🚀 go-pugleaf

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