Re: rigorous and formal proof

[John Harrison <John.Harrison@cl.cam.ac.uk>]

I would say that:

 * A proof is formal if it is constructed in conformance with a set of
   precisely defined and algorithmically checkable rules.

 * A proof is rigorous if the reasoning process it involves is considered
   correct beyond reasonable doubt.

On these definitions, a correct proof in an unsound formal system is formal
but not rigorous (no doubt there have been plenty of these).

It so happens that current mathemticians tend to identify "rigorous" with
"could in principle be formalized in an appropriate widely accepted formal
system", but I think this is a convenience rather than an expression of a
philosophical position. That is, I don't see that a proof obviously needs
to be formalizable in order to be rigorous.

Nevertheless, formalizability in something like ZF or TG would be accepted
by most mathematicians as a sufficient condition for rigour. And actually
formalizing proofs removes the questions about "what can be done in
principle".  This, I guess, is why so many people are interested in
projects like Mizar.

In practice, Mizar's formal system is a bit different from the ones
given in textbooks, but it's still perfectly formal (since it can be
checked by an autonomous program). It would not be difficult to expand
out Mizar proofs into a more traditional and simple formal system ---
the HOL prover already expands all its proofs to such a system.

John.