[FOM] 773: Goedel's Second: Proofs/1
Harvey Friedman
hmflogic at gmail.com
Mon Dec 18 20:31:25 EST 2017
We present what seems to be a new(?) proof of Goedel's Second
Incompleteness Theorem. It has the advantage that the only self
reference is buried in the trivial proof of an interesting and
fundamental recursion theoretic fact: that the set {e: e in W_e}
agrees somewhere with every r.e. set. The full fact, not needed here,
is of course: any complete r.e. set agrees somewhere with every r.e.
set. Here W_e is the e-th r.e. set, and two sets agree at n if and
only if (n is in the first set if and only if n is in the second set).
NOTE: What we actually need is the we can point to a specific place
where they can be proved to agree within a very weak fragment of
arithmetic.
Because the self reference is buried nicely as a triviality within a
mathematically interesting fact about r.e. sets, we think that this
proof is considerably more friendly than other proofs of GSC. It would
be interesting to see what readers have to say about this.
Here we present the proof with the level of rigor that one
typically exposits. This does not go into various details, e.g., like
the Hilbert/Bernays derivability conditions. See my particularly
careful and thorough version of Hilbert/Bernays/Jerosolow in
57. My Forty Years On His Shoulders, October 31, 2009, to appear in
the proceddings of the Goedel Centenary meeting in Vienna, held in
April 2006, Horizons of Truth, 69 pages. Supercedes earlier versions.
Fortyyears111909
http://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
section 4, Second Incompleteness Theorem.
I have written extensively on FOM concerning a totally different issue
surrounding GSC. That is, what is the best formal statement of it that
avoids any specific formalization of Con and singles out the essential
features of formalizations of Con that can be used. I expect to write
about that again soon.
In fact, there are many interlocking issues surrounding statements and
proofs of GSC that are still in a very unsettled state. The entire
complex of issues needs to be organized and fleshed out. This posting
concerns, as I said, only one issue. Trying to give a particularly
simple transparent semiformal proof.
The basic idea is to push as much of the proof of Goedel's Second
Incompleteness Theorem as we can, away from details about proof
systems, and proofs and towards recursion theory. It is well known
that this has been extremely successful with Goedel's First
Incompleteness Theorem.
OVERVIEW OF PROOF
black boxing very general easy manipulations concerning {e: e in W_e},
which are treated below
Assume T is adequate, T is consistent, and T proves Con(T). We want to
obtain a contradiction.
We compare the properties of n,
1) n in W_n
2) T proves (n not in W_n)
By very general easy manipulations, there is a particular number
(numeral) t* such that
3) t* in W_t* if and only if T proves (t* not in W_t*)
4) T proves 3)
REASON: Recursion theoretically, a complete r.e. set must agree with
any other r.e. set somewhere; and in fact provably, at a specific
number. See below.
Obviously
5) if (t* in W_t*) then T proves (t* in W_t*)
6) T proves 5)
Hence
7) if both statements in 3) are true then T is inconsistent
8) both statements in 3) are false
9) T proves 7)
10) T proves that both statements in 3) are false
7) is from 3), 5).
8) is from 5), 7), and T is consistent.
9) is from 4), 6).
10) is from 9), and T proves Con(T).
11) T does not prove (t* not in W_t*)
12) T proves t* not in W_t*.
11) is from 8), second statement.
12) is from 10), first statement.
QED
A COMPLETE R.E. SET MUST AGREE WITH ANY OTHER R.E. SET SOMEWHERE, AND
IN FACT PROVABLY, AT A SPECIFIC NUMBER
We need this only for the complete r.e. set {e: e in W_e}. It follows
for all complete r.e. sets since any two have a specific recursive
isomorphism that provably works within a fixed weak fragment T_0 of
arithmetic.
THEOREM 1. (Well known) For all r.e. sets S, [e: e in W_e} and S
agree somewhere.
Proof: Set S = W_t. Then the two sets agree at t because t in W_t if
and only if t in W_t. QED
COROLLARY 2. There is a very weak fragment T_0 of arithmetic,
independent of phi, such that given any r.e. set S, there exists t
such that
i. t in W_t if and only if t in S
ii. T_0 proves (t* in W_t* if and only if t* in S).
Proof: By Theorem 1. The proof there goes through in any T_0 that
treats the notions sensibly. QED
************************************************************************
My website is at https://u.osu.edu/friedman.8/ and my youtube site is at
https://www.youtube.com/channel/UCdRdeExwKiWndBl4YOxBTEQ
This is the 773rd 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-699 can be found at
http://u.osu.edu/friedman.8/foundational-adventures/fom-email-list/
700: Large Cardinals and Continuations/14 8/1/16 11:01AM
701: Extending Functions/1 8/10/16 10:02AM
702: Large Cardinals and Continuations/15 8/22/16 9:22PM
703: Large Cardinals and Continuations/16 8/26/16 12:03AM
704: Large Cardinals and Continuations/17 8/31/16 12:55AM
705: Large Cardinals and Continuations/18 8/31/16 11:47PM
706: Second Incompleteness/1 7/5/16 2:03AM
707: Second Incompleteness/2 9/8/16 3:37PM
708: Second Incompleteness/3 9/11/16 10:33PM
709: Large Cardinals and Continuations/19 9/13/16 4:17AM
710: Large Cardinals and Continuations/20 9/14/16 1:27AM
700: Large Cardinals and Continuations/14 8/1/16 11:01AM
701: Extending Functions/1 8/10/16 10:02AM
702: Large Cardinals and Continuations/15 8/22/16 9:22PM
703: Large Cardinals and Continuations/16 8/26/16 12:03AM
704: Large Cardinals and Continuations/17 8/31/16 12:55AM
705: Large Cardinals and Continuations/18 8/31/16 11:47PM
706: Second Incompleteness/1 7/5/16 2:03AM
707: Second Incompleteness/2 9/8/16 3:37PM
708: Second Incompleteness/3 9/11/16 10:33PM
709: Large Cardinals and Continuations/19 9/13/16 4:17AM
710: Large Cardinals and Continuations/20 9/14/16 1:27AM
711: Large Cardinals and Continuations/21 9/18/16 10:42AM
712: PA Incompleteness/1 9/23/16 1:20AM
713: Foundations of Geometry/1 9/24/16 2:09PM
714: Foundations of Geometry/2 9/25/16 10:26PM
715: Foundations of Geometry/3 9/27/16 1:08AM
716: Foundations of Geometry/4 9/27/16 10:25PM
717: Foundations of Geometry/5 9/30/16 12:16AM
718: Foundations of Geometry/6 101/16 12:19PM
719: Large Cardinals and Emulations/22
720: Foundations of Geometry/7 10/2/16 1:59PM
721: Large Cardinals and Emulations//23 10/4/16 2:35AM
722: Large Cardinals and Emulations/24 10/616 1:59AM
723: Philosophical Geometry/8 10/816 1:47AM
724: Philosophical Geometry/9 10/10/16 9:36AM
725: Philosophical Geometry/10 10/14/16 10:16PM
726: Philosophical Geometry/11 Oct 17 16:04:26 EDT 2016
727: Large Cardinals and Emulations/25 10/20/16 1:37PM
728: Philosophical Geometry/12 10/24/16 3:35PM
729: Consistency of Mathematics/1 10/25/16 1:25PM
730: Consistency of Mathematics/2 11/17/16 9:50PM
731: Large Cardinals and Emulations/26 11/21/16 5:40PM
732: Large Cardinals and Emulations/27 11/28/16 1:31AM
733: Large Cardinals and Emulations/28 12/6/16 1AM
734: Large Cardinals and Emulations/29 12/8/16 2:53PM
735: Philosophical Geometry/13 12/19/16 4:24PM
736: Philosophical Geometry/14 12/20/16 12:43PM
737: Philosophical Geometry/15 12/22/16 3:24PM
738: Philosophical Geometry/16 12/27/16 6:54PM
739: Philosophical Geometry/17 1/2/17 11:50PM
740: Philosophy of Incompleteness/2 1/7/16 8:33AM
741: Philosophy of Incompleteness/3 1/7/16 1:18PM
742: Philosophy of Incompleteness/4 1/8/16 3:45AM
743: Philosophy of Incompleteness/5 1/9/16 2:32PM
744: Philosophy of Incompleteness/6 1/10/16 1/10/16 12:15AM
745: Philosophy of Incompleteness/7 1/11/16 12:40AM
746: Philosophy of Incompleteness/8 1/12/17 3:54PM
747: PA Incompleteness/2 2/3/17 12:07PM
748: Large Cardinals and Emulations/30 2/15/17 2:19AM
749: Large Cardinals and Emulations/31 2/15/17 2:19AM
750: Large Cardinals and Emulations/32 2/15/17 2:20AM
751: Large Cardinals and Emulations/33 2/17/17 12:52AM
752: Emulation Theory for Pure Math/1 3/14/17 12:57AM
753: Emulation Theory for Math Logic 3/10/17 2:17AM
754: Large Cardinals and Emulations/34 3/12/17 12:34AM
755: Large Cardinals and Emulations/35 3/12/17 12:33AM
756: Large Cardinals and Emulations/36 3/24/17 8:03AM
757: Large Cardinals and Emulations/37 3/27/17 2:39AM
758: Large Cardinals and Emulations/38 4/10/17 1:11AM
759: Large Cardinals and Emulations/39 4/10/17 1:11AM
760: Large Cardinals and Emulations/40 4/13/17 11:53PM
761: Large Cardinals and Emulations/41 4/15/17 4:54PM
762: Baby Emulation Theory/Expositional 4/17/17 1:23AM
763: Large Cardinals and Emulations/42 5/817 2:18AM
764: Large Cardinals and Emulations/43 5/11/17 12:26AM
765: Large Cardinals and Emulations/44 5/14/17 6:03PM
766: Large Cardinals and Emulations/45 7/2/17 1:22PM
767: Impossible Counting 1 9/2/17 8:28AM
768: Theory Completions 9/4/17 9:13PM
769: Complexity of Integers 1 9/7/17 12:30AM
770: Algorithmic Unsolvability 1 10/13/17 1:55PM
771: Algorithmic Unsolvability 2 10/18/17 10/15/17 10:14PM
772: Algorithmic Unsolvability 3 Oct 19 02:41:32 EDT 2017
Harvey Friedman
More information about the FOM
mailing list