[FOM] RE Formal Proof

[Alan Weir]

Jay Sulzberger wrote:
> Surely no serious student of logic after the publication of the
> completeness theorem for the lower order predicate calculus ever thought
> that formalization was impossible, in any serious sense. If one thought
> this, then the completeness theorem must seem to lack force.

and Timothy Chow replied:

>Maybe no "serious student of logic" thought so, but for a long time, I
> believe that it was the conventional wisdom that complete formalization of
> nontrivial mathematics was impossible in practice.



I'd add that completeness and soundness theorems apply to formalised languages but there are a prior questions about the relationship between these languages and the languages in which most maths is carried out which need to be addressed before we can appreciate the full force of the theorems. Can all of the informal mathematical proofs which still form the vast bulk of published mathematics be adequately formalised in formal languages? What does 'adequacy' here amount to? And even if so, can all the proofs of the theorems thus formalised be appropriately transformed into formal proofs? What does 'appropriately' amount to here (would it require that formal proofs be finite, for example)? Many philosophers and mathematicians have challenged the claim that formalisation is always possible, for example Yehuda Rav in a well known series of articles including 'Why Do We Prove Theorems?’, Philosophia Mathematica, 1999. These people are not ignorant of the completeness theorem.



With respect to those parts of mathematics which can be formalised (in some interesting useful sense), whether that is all or not, there then arises the question whether this can be done in some reasonable, feasible sense. Whether, for example, it will soon be appropriate to ask anyone submitting a proof in these areas to submit in addition a mechanically checkable, computer-verifiable perhaps,  formalisation. That's clearly a very important question, but the more philosophically fundamental questions are those which arise with respect to the relationship between informal proofs and formal proofs, proofs for which there is a purely syntactic criterion of correctness.



Alan Weir



Professor Alan Weir

Roinn na Feallsanachd/Philosophy
Sgoil nan Daonnachdan/School of Humanities

Oilthigh Ghlaschu/University of Glasgow

GLASGOW G12 8Q

SCOTLAND
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20141028/26a23186/attachment.html>