[Date Index] [Thread Index] [FOM Postings] [FOM Home]

*To*: fom@math.psu.edu*Subject*: FOM: certainty*From*: Randy Pollack <pollack@dcs.gla.ac.uk>*Date*: Tue, 15 Dec 1998 17:46:38 GMT*Sender*: owner-fom@math.psu.edu

First, a recent example of another long-open problem verified using computer calculation of many and large cases: Thomas Hales announced a proof of Kepler's conjecture about maximum density packing of speheres (http://www.math.lsa.umich.edu/~hales/countdown). See Nature (1 Oct 1998) for an informal overview. Vladimir Sazonov said he is "a permanent opponent of those who assert existence of absolute mathematical truth." I don't know what "absolute truth" means. Issues of evidence and belief are more interesting. What follows is not a final answer to mathematical meaning, but some sample thoughts meant to widen the FOM discussion. I suggest seperating belief in a formal system from belief in proofs in that formal system. Belief in ZFC is informal in the sense that if we disagree (say Steve Cook believes ZFC but I do not) there is no formal argument to attain agreement. We must talk about mathematical principles and other philosophical stuff. Belief in a formal proof in a given formal system, S, (here I'm vague about what is a formal system; I'll return to that later) is attained formally, not philosophically. If A doesn't accept a proof in S, s/he must say which step s/he doesn't accept. Then B, who believes the proof in S, can add more detail to the explanation of why the side conditions and premises of Rule xxx are satisfied; or possibly A can convince B the formal rule does not actually apply. Under reasonable meanings of "formal system", A and B can resolve the point purely formally. The distinction is not quite as simple as I just suggested. We need some base notion of representation of a formal system; i.e. we somehow have to bridge the informal-formal gap. We cannot have a formal presentation of a formal system until we have, at bottom, some informally presented formal system. This is usually where we appeal to PRA (informally presented), or to Fefermans FS0, or to some weak dependent types system (Martin-Lof's or Plotkin's Logical Frameworks). So it is possible to find disagreement about the encoding of our object formal system in the meta-system PRA or FS0 or .... The "informal" framework may actually be a computer program in a completely formal notation, but it ultimately is executed on a physical device. We haven't yet addressed the formal system itself; we must look, not at extension (the judgements derived), but at presentation. Cut-free FOL is different from FOL with cut in terms of both feasible checking and mathematical principles. The admissibility of cut is meta-theoretic, outside of FOL, depending on induction in the meta-theory. So if we want to use cut, and other admissible rules, they should be explicitly part of the formal system. In this way, we might have a formal proof of the 4CT in a formal system that has rules explaining the computational behavior of the computer programs that check the cases. Those rules are shown to be admissible by meta-theoretic proof, just as the cut rule is for FOL. Accepting the meta-theoretic program correctness proof as a mathematical principle is the main difficulty to calling this a proof, but how is it different from accepting cut? We can internalize this approach in a logic with internal computation, such as Martin-Lof type theory or the Calculus of Constructions. The 4CT programs can be written as typed lambda-terms that are proved correct internal to the logic. (Now there is no new mathematical principle being accepted specifically for the 4CT, and Martin-Lof type theory is based on weak principles for those who accept ZFC!) However, we must execute the typed lambda-terms (i.e. check definitional equality in the formal system) to have a truly formal proof. This is totally infeasible! But we can play the same trick again. Work on "program extraction" from constructive proofs (e.g. Nakano and Hayashi, Paulin-Mohring, Berardi, ...) suggests that we can make these internal proofs of the 4CT in Martin-Lof type theory into feasible programs. (E.g. using Paulin-Mohring's extraction, implemented in Coq, there is a running proofchecker actually extracted from a proof that proof-checking is decidable in the Calculus of Constructions.) However, we will need a new mathematical principle to accept these feasible programs as internal proofs in the logic. This has not been studied to my knowledge. Again, this principle is seen meta-theoretically to be admissible, and is not a special principle adopted to prove a particular theorem. Thus it is conceivable we can have a completely formal (feasible) proof of the 4CT in a constructive and predicative logic. Still, I guess no mathematician will "read and understand it" in the ordinary sense. What should we make of that? -- Randy Pollack <http://www.dcs.gla.ac.uk/~pollack/> Computing Science Dept. <pollack@dcs.gla.ac.uk> University of Glasgow, G12 8QQ, SCOTLAND Tel: +44 141 330-6055

**Follow-Ups**:**Vladimir Sazonov**- Re: FOM: certainty

[Date Prev] [Date Next] [Thread Prev] [Thread Next]

[Date Index] [Thread Index] [FOM Postings] [FOM Home]