[mizar] proof objects for mizar: already available?

[Jesse Alama <jesse.alama@gmail.com>]

There are two senses in which mizar already has proof objects, despite
appearances to the contrary.  However, both senses are unsatisfactory.

(a) One could argue that there's no difference between "proof object"
    and "mizar article", because the proof is contained right there in
    a mizar text.  That is, of course, correct.  But this is
    unsatisfactory because one must have the mizar infrastructure to
    work with the proof object.  Of course, with some mathematical and
    logical background one can read a mizar text in the same sense
    that one reads a book, but doing anything interesting requires the
    mizar tools.  (Moreover, as we all know, in general, owing to the
    evolving syntax and library, an article might even require a
    specific *version* of the mizar toolset.)  But proof objects
    shouldn't really depend on the version of mizar that was used to
    generate them.  They shouldn't even depend on mizar itself.  One
    should be able to inspect and work with a mizar object, in
    principle, independently of mizar.

(b) Proofs objects are already available, in some sense, for mizar
    proofs.  They do not give precisely what is wanted from the
    concept of proof object, though:

    * They are not always available.  With the current transformation
      into a vanilla first-order format, and with current ATPs, for
      less than half of mizar theorems from the library do we have
      deductions.  This is clearly an important result for the
      community, but not having deductions is a serious shortcoming.
      We want proof objects for all mizar proofs.

    * The calculi of the proofs that are found this way depend on the
      theorem prover employed.  One finds proofs in the superposition
      calculi, resolution calculi... The plurality of proof calculi is
      welcome -- we want to view mizar proof objects through various
      formal lenses -- but none of these is satisfactory because none
      is a natural deduction proof in the style of mizar.  (To some
      extent this problem can be overcome: an ATP could either do
      search in a natural deduction setting, or emit natural
      deductions by translating whatever calculus it uses into natural
      deduction.  But proof search in natural deduction is generally
      not as efficient as search in other calculi.  And the
      translation from other calculi to a natural deduction is not
      always clear.)  What is wanted from proof objects for mizar is a
      sort of natural deduction proof that adheres more or less to the
      mizar format, but which brings out all logical details.  It is
      unpleasant and awkward to switch from natural deduction-style
      mizar proofs to unnatural resolution deductions.

    * There is no assurance that the proofs discovered by an ATP
      thanks to Josef's translations are the same as the mizar proofs
      with which one started.  Genuinely new proofs can be (and are)
      discovered.  An ATP might exploit a premise or combination of
      premises in an unusual way that diverges from the input mizar
      proof.  An even when the ATP-discovered proof is more or less
      congruent to the mizar proof from which it came, because it is
      expressed in a different formal calculus there might be some
      uncertainty about whether we are looking at the same proof.

    * By diverging from mizar's natural deduction format, one loses
      the ability to carry out experiments and investigations that
      require that one works with natural deductions.  Thus, one might
      wish to investigate the notion of obviousness.  One might ask,
      for example, what instances of which universal formulas were
      used to carry out a particular by step.  One might wish to carry
      out certain transformations of the the deduction (e.g., rewrite
      a natural deduction by represent applications of definitions as
      rules of inference, rather than as applications of the rule of
      modus ponens).

--
Jesse Alama
http://centria.di.fct.unl.pt/~alama/