mps@duke.UUCP (06/08/87)
In his valuable contribution to a continuing discussion on Godel's incompleteness results, Rick Moll asks: >I believe there is a theorem that states that the consistency of a >consistent theory cannot be formally proved from those axioms >themselves. ... We can use one set of axioms to prove the >consistency of another, but our first axiom (at least) we must simply >assume to be consistent... If anyone out there can state this >theorem succinctly (and is still awake after reading this article), >please post or e-mail it to me. This certainly sounds like Godel's second incompleteness theorem, although after reading Moll's article I should think that he would be familiar with it. Anyway, to summarize: Godel's first incompleteness theorem, as generalized by Rosser, states that any consistent first-order axiomatization of arithmetic will be incomplete -- i.e., some formulable statements will be neither provable nor disprovable. These unprovable statements may of course be added as axioms, but the incompleteness will persist for any effective extension. Godel's second incompleteness theorem, as generalized by Hilbert-Bernays, says that a system rich enough to express its own consistency, if consistent, will be unable to prove its own consistency. A system is rich enough to express its own consistency in the relevant sense if it contains a function effectively representing the substitution operation and a predicate effectively representing provability within the system. Almost any logic text other than the most elementary covers these theorems. I am looking at Richard E. Grandy's ADVANCED LOGIC FOR APPLICATIONS (Reidel, 1977). I might also mention GODEL'S PROOF, by Nagel & Newman, for those unfamiliar with this respectable popular work. The more serious should read Godel's papers, translated in J. van Heijenoort's FROM FREGE TO GODEL (Harvard, 1967). Also worthwhile is Solomon Feferman's "Arithmetization of Metamathematics," FUNDAMENTA MATHEMATICA, 1960. Michael P. Smith