The nature of proofs

A proof may hope to be correct only when it can be verified independent of intuition. The prover and the verifier may agree on a common language to write and analyse the proof, but that language must be bred outside the domain of the proof itself (and I assume that a proof subsumes the theorem it seeks to prove). To analyse a written proof is then to mechanically establish that it has a valid structure.

This necessity, however, abstracts away some burdens off the proof, viz. the denotational meaning of the terms of writing and analysis. One might, of course, prefer to call a proof a proof only when it answers the denotation as well; I would be a bit skeptical, in that case, on what decides the denotation of the in-the-limit denotation language itself. At some point, one would need to rely on intuition to write a theorem to be proved, and write the proof-writing-and-analysis structure, without analysing the soundness of these "translations" formally; it would be futile to seek to avoid this leap.

One now needs to focus on getting the proof right, after such other burdens are hidden. A good principle: strip the proof of any essential intuition. An intuition would reflect a denotation of structure to some in-the-limit informal domain. There is no guarantee that the translation preserves structures, because the structure itself is not formalized in the domain speaking the intuition.

It can thus be thought prudent to delegate writing and analysing proofs to a mind that has never seen the denotational translations as well.

(Note added on 12/16/2005: Maybe I'm repeating an idea that Dijkstra talked about in 1988.)