[FOM] 305:Proofs of Godel's Second
Harvey Friedman
friedman at math.ohio-state.edu
Thu Dec 21 11:31:49 EST 2006
We present two proofs of Godel's second incompleteness theorem. In both
cases, we work solely with PA, because of its great familiarity. The proofs
can be easily adapted to give general forms of Godel's second incompleteness
theorem. This will be taken up in a publication.
The first proof is the earlier proof that I put on the FOM recently. It
presents an intriguing, diabolical Turing Machine involving running Turing
Machines at themselves, and then asks what happens when it is run at itself.
The rest follows inexorably. Since there was no indication that the proof
was known by readers, I decided to move it to my numbered postings.
The second proof is the same as the first proof, except that simplifications
are made by using the recursion theorem freely.
The third proof eliminates the need for the recursion theorem and introduces
a further simplification, by using a well known modification of the Turing
machine model. We hide all use of diagonalization into this standard
modified Turing machine model.
CERTAINLY there is a real question of just how new and/or important these
proofs are. So one is clearly led to questions of pedagogy. I would like to
hear opinions on that.
ALSO, none of this addresses the crucial issue of just what a standard proof
predicate is. All treatments of this, at the moment, are uncomfortably
complicated. Also the problem with the derivability conditions going back to
Hilbert/Bernays is that one still has to prove the existence of proof
predicates obeying those conditions. The derivability conditions themselves
should be derived from more fundamental principles.
I discussed a purely semantic approach on the FOM which avoids any use of
proof predicates. This has enormous advantages, but still one can object
that one still wants the proof theoretic theorem.
The prior FOM discussion is at
http://www.cs.nyu.edu/pipermail/fom/2006-March/010207.html 3/18/06
http://www.cs.nyu.edu/pipermail/fom/2006-March/010258.html 3/23/06
http://www.cs.nyu.edu/pipermail/fom/2006-April/010324.html 4/3/06
http://www.cs.nyu.edu/pipermail/fom/2006-May/010524.html 5/9/06
http://www.cs.nyu.edu/pipermail/fom/2006-May/010525.html 5/9/06
http://www.cs.nyu.edu/pipermail/fom/2006-May/010529.html 5/10/06
http://www.cs.nyu.edu/pipermail/fom/2006-May/010532.html 5/11/06
http://www.cs.nyu.edu/pipermail/fom/2006-December/011194.html 12/17/06
HOWEVER, I still don't have the proof of Godel's 2nd that I would like to
have. Although these proofs are simple, they are still too close to what is
normally done.
IN FACT, all of these proofs are merely failed proofs of the kind I am
looking for. I am looking for a truly quantitative proof.
FIRST PROOF
To make things as familiar as possible, we treat PA. We assume familiarity
with Turing machines and their formalization in PA.
In particular, we will assume that every n >= 0 is the Godel number of a
Turing machine. We write TM[n] for the n-th Turing machine.
We begin with the description of a particularly simple, fascinating(!) and
diabolical(!) Turing machine TM.
At input n, TM searches for a proof in PA that "TM[n] does not halt at n".
When it finds one, it immediately halts (and returns 0). Otherwise, TM will
not halt.
Let TM be TM[k]. What if we run TM[k] at k?
case 1. There is a proof in PA that "TM[k] does not halt at k". Then TM[k]
halts at k (by the action of TM = TM[k]). But then PA proves "TM[k] halts at
k". Since PA is CONSISTENT, this case is impossible.
case 2. There is no proof in PA that "TM[k] does not halt at k". Then TM[k]
does not halt at k (by the action of TM = TM[k]).
Note that we have proved
there is no proof in PA that "TM[k] does not halt at k".
TM[k] does not halt at k.
within PA + Con(PA).
{These two lines alone, independently of their provability in PA + Con(PA),
give us a form of Godel's 1st for PA}.
If PA were to prove Con(PA), then PA would prove
there is no proof in PA that "TM[k] does not halt at k".
TM[k] does not halt at k.
>From this, we see that PA would prove
there is no proof in PA that "TM[k] does not halt at k".
PA proves "TM[k] does not halt at k".
Hence PA would be INCONSISTENT. QED
Furthermore, the entire argument takes place in a weak fragment of PA.
SECOND PROOF USING RECURSION THEOREM
We first present the second proof using the recursion theorem freely.
NOTE: Of course, this is starting to look more like the standard proofs.
END.
We let n be such that we can prove in PA,
TM[n] halts at 0 when and ony when we find a proof in PA that TM[n] does not
halt at 0.
case 1. There is a proof in PA that "TM[n] does not halt at 0". Then, using
the consistency of PA, it is the case that TM[n] does not halt at 0. Hence
there is no proof in PA that "TM[n] does not halt at 0". This is a
contradiction.
case 2. There is no proof in PA that "TM[n] does not halt at 0". Then TM[n]
does not halt at 0 (by the action of TM[n]).
Note that we have proved
there is no proof in PA that "TM[n] does not halt at 0".
TM[n] does not halt at 0.
within PA + Con(PA).
{These two lines alone, independently of their provability in PA + Con(PA),
give us a form of Godel's 1st for PA}.
If PA were to prove Con(PA), then PA would prove
there is no proof in PA that "TM[n] does not halt at 0".
TM[n] does not halt at 0.
>From this, we see that PA would prove
there is no proof in PA that "TM[n] does not halt at 0".
PA proves "TM[n] does not halt at 0".
Hence PA would be INCONSISTENT. QED
Furthermore, the entire argument takes place in a weak fragment of PA.
THIRD PROOF BASED ON MODEL OF COMPUTATION
We use the Turing machine model of computation, both simplified and
amplified.
Simplified in that these Turing machines have no input. They just initialize
and then compute, either halting or not halting. They don't even have
outputs.
Amplified in that upon initialization, their program, which is a set of
quadruples, is inscribed on the tape starting at square 0. These
inscriptions are always made using three symbols 0,1,2,3. The Turing
machines themselves can use any natural numbers as symbols.
So this is a stored program model, with no inputs and no outputs, where the
program can be accessed and overwritten just like any other location in
memory.
NOW, we can, without arguably looking like diagonalization, program a Turing
machine TM, which does the following:
it searches for a proof in PA that "the Turing machine itself, as read from
the tape, does not halt". It halts when and only when it finds this proof.
Let TM[k] be this Turing machine.
case 1. There is a proof in PA that "TM[k] does not halt". Then, using the
consistency of PA, it is the case that TM[k] does not halt. Hence there is
no proof in PA that "TM[k] does not halt" (by the action of TM[k]). This is
a contradiction.
case 2. There is no proof in PA that "TM[k] does not halt". Then TM[k] does
not halt (by the action of TM[k]).
Note that we have proved
there is no proof in PA that "TM[k] does not halt".
TM[k] does not halt.
within PA + Con(PA).
{These two lines alone, independently of their provability in PA + Con(PA),
give us a form of Godel's 1st for PA}.
If PA were to prove Con(PA), then PA would prove
there is no proof in PA that "TM[k] does not halt".
TM[k] does not halt.
>From this, we see that PA would prove
there is no proof in PA that "TM[k] does not halt".
PA proves "TM[k] does not halt".
Hence PA would be INCONSISTENT. QED
Furthermore, the entire argument takes place in a weak fragment of PA.
**********************************
I use http://www.math.ohio-state.edu/%7Efriedman/ for downloadable
manuscripts. This is the 305th in a series of self contained numbered
postings to FOM covering a wide range of topics in f.o.m. The list of
previous numbered postings #1-249 can be found at
http://www.cs.nyu.edu/pipermail/fom/2005-June/008999.html in the FOM
archives, 6/15/05, 9:18PM. NOTE: The title of #269 has been corrected from
the original.
250. Extreme Cardinals/Pi01 7/31/05 8:34PM
251. Embedding Axioms 8/1/05 10:40AM
252. Pi01 Revisited 10/25/05 10:35PM
253. Pi01 Progress 10/26/05 6:32AM
254. Pi01 Progress/more 11/10/05 4:37AM
255. Controlling Pi01 11/12 5:10PM
256. NAME:finite inclusion theory 11/21/05 2:34AM
257. FIT/more 11/22/05 5:34AM
258. Pi01/Simplification/Restatement 11/27/05 2:12AM
259. Pi01 pointer 11/30/05 10:36AM
260. Pi01/simplification 12/3/05 3:11PM
261. Pi01/nicer 12/5/05 2:26AM
262. Correction/Restatement 12/9/05 10:13AM
263. Pi01/digraphs 1 1/13/06 1:11AM
264. Pi01/digraphs 2 1/27/06 11:34AM
265. Pi01/digraphs 2/more 1/28/06 2:46PM
266. Pi01/digraphs/unifying 2/4/06 5:27AM
267. Pi01/digraphs/progress 2/8/06 2:44AM
268. Finite to Infinite 1 2/22/06 9:01AM
269. Pi01,Pi00/digraphs 2/25/06 3:09AM
270. Finite to Infinite/Restatement 2/25/06 8:25PM
271. Clarification of Smith Article 3/22/06 5:58PM
272. Sigma01/optimal 3/24/06 1:45PM
273: Sigma01/optimal/size 3/28/06 12:57PM
274: Subcubic Graph Numbers 4/1/06 11:23AM
275: Kruskal Theorem/Impredicativity 4/2/06 12:16PM
276: Higman/Kruskal/impredicativity 4/4/06 6:31AM
277: Strict Predicativity 4/5/06 1:58PM
278: Ultra/Strict/Predicativity/Higman 4/8/06 1:33AM
279: Subcubic graph numbers/restated 4/8/06 3:14AN
280: Generating large caridnals/self embedding axioms 5/2/06 4:55AM
281: Linear Self Embedding Axioms 5/5/06 2:32AM
282: Adventures in Pi01 Independence 5/7/06
283: A theory of indiscernibles 5/7/06 6:42PM
284: Godel's Second 5/9/06 10:02AM
285: Godel's Second/more 5/10/06 5:55PM
286: Godel's Second/still more 5/11/06 2:05PM
287: More Pi01 adventures 5/18/06 9:19AM
288: Discrete ordered rings and large cardinals 6/1/06 11:28AM
289: Integer Thresholds in FFF 6/6/06 10:23PM
290: Independently Free Minds/Collectively Random Agents 6/12/06 11:01AM
291: Independently Free Minds/Collectively Random Agents (more) 6/13/06
5:01PM
292: Concept Calculus 1 6/17/06 5:26PM
293: Concept Calculus 2 6/20/06 6:27PM
294: Concept Calculus 3 6/25/06 5:15PM
295: Concept Calculus 4 7/3/06 2:34AM
296: Order Calculus 7/7/06 12:13PM
297: Order Calculus/restatement 7/11/06 12:16PM
298: Concept Calculus 5 7/14/06 5:40AM
299: Order Calculus/simplification 7/23/06 7:38PM
300: Exotic Prefix Theory 9/14/06 7:11AM
301: Exotic Prefix Theory (correction) 9/14/06 6:09PM
302: PA Completeness 10/29/06 2:38AM
303: PA Completeness (restatement) 10/30/06 11:53AM
304: PA Completeness/strategy 11/4/06 10:57AM
Harvey Friedman
More information about the FOM
mailing list