[FOM] Certificates are Fully Practical

[Alan Weir]

Thanks to Prof. Friedman (FOM Digest, Vol 129, Issue 20) for the thoughtful comments on the issue of finiteness of proofs and certificates.

Regarding 'certificates', I had the idea that there is an abstract theoretical notion of 'certificate' in computer science in which there is no finite bound on a certificate. But no matter, I agree that the emergence of proof assistants such as Coq, Isabelle, Mizar and the like has altered the landscape considerably.

I'd be interested to hear views on the likely consequences though: do list members think that we will move to a situation when for every theorem of interest- in any area of mathematics whatever- whenever an informal proof emerges we will be able, if it conforms to standards which are emerging in conjunction with the development of proof assistants, to plug it in to such an assistant and get a fully rigorous proof. That's not the case for current maths. Is it reasonable to suppose it likely for future mathematics however it develops by 2150 or beyond. Yehuda Rav and others have expressed strong scepticism about this.

However even if that is how things turns out (and there are humans still around and with the time and ability to do mathematics in later centuries!) , it will still be the case that there will be theses, even if boring uninteresting ones,  small enough for us to grasp but whose shortest rigorous proof (if they are provable) will be far too long for any human or computer to churn out. This has implications for philosophy of maths, if not mathematical practice. Certainly for formalists such as myself: if there can be concrete tokens of mathematical sentences which cannot  have concrete proofs or disproofs does that not block any equation of truth with proof, unless one allows in abstract proofs. But then if so, why not other abstracta?

But even for non-formalist logicians  the limited extent of concrete, feasible provability surely has implications. We declare first-order logic complete with respect to a particular semantics, but this whole claim is senseless unless we idealise beyond feasible, concretely realisable proof. Given that we do so, why not declare PA negation-complete, since it is so in omega-logic, and read Godel's beautiful results, the first theorem in particular, as telling us not that truth and proof come apart but that finitary proof is too weak? The gap arises, putting it crudely, because we are infinitistic in model theory but finitistic in proof theory. Is there a rationale for this, or is it an accidental product of Godel's prestige and the fact that when he discovered the incompleteness theorems he was much more strongly influenced by finitism than later?

Note also that though we cannot produce unabbreviated infinitary proofs, we can often produce detailed proof sketches which in a clear sense leave no room for doubt as to the structure of the final proof. Indeed we can even computerise this to an extent, in such things as recursive omega rules. So it is not clear that infinitary logic has no implications for mathematical inferential practice (as well as applications as a tool in e.g. study of large cardinals).

Alan Weir

Professor Alan Weir
Roinn na Feallsanachd/Philosophy
Sgoil nan Daonnachdan/School of Humanities
Oilthigh Ghlaschu/University of Glasgow
GLASGOW G12 8QQ

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20130918/a38e561f/attachment.html>