[FOM] 778: Goedel's Second: Proofs/5
Harvey Friedman
hmflogic at gmail.com
Sat Dec 30 02:40:16 EST 2017
RADICALLY (?) SIMPLIFIED(?) PROOF OF GOEDEL'S SECOND INCOMPLETENESS THEOREM
Noah Schweber https://cs.nyu.edu/pipermail/fom/2017-December/020741.html
has quite correctly pointed out that my condition
being an r.e. set that agrees somewhere with every r.e. set
is the same as
being an r.e. set that is not the complement of any r.e. set
is the same as
being an r.e. set that is not recursive.
So why did I have this blind spot? The answer is that I was led to the
notion by pondering GSIT and my argument for GSIT, and automatically
assumed that something powerfully mysterious must be going on with the
essence of the proof - and hence or "hence" with this property above
of r.e. sets that I isolated!
So what should I learn from my idiocy (that I already don't know
about)? That seems to be a difficult open question.
Now let's go back and upgrade
https://cs.nyu.edu/pipermail/fom/2017-December/020741.html
RADICALLY (?) SIMPLIFIED(?) PROOF OF GOEDEL'S SECOND INCOMPLETENESS THEOREM
1. {e: T proves (e not in W_e)}
2. r.e. agreement theorems
3. proving GSIT
1. {e: T proves (e not in W_e)}
Here we simply copy the proof given in
https://cs.nyu.edu/pipermail/fom/2017-December/020729.html
GSIT. Let T be a consistent r.e., axiomatized theory containing a
weak fragment K of arithmetic. Then T does not prove Con(T).
Proof: Let n* be natural so that W_n* = {e: T proves (e not in W_e)}. Then
1) n* in W_n* if and only if T proves (n* not in W_n*).
2) n* in W_n* implies T proves (n* in W_n*).
3) n* not in W_n* and T does not prove (n* not in W_n*).
Note that 3) follows from 1),2), and that T is consistent. The above
argument has been carried out external to T.
Note also that the above argument can be carried out in T + Con(T). In
particular, the first conjunct of 3) gets modified to: T + Con(T)
proves n* not in W_n*. So if T proves Con(T) then T proves n* not in
W_n*, contradicting the unmodified second conjunct of 3). Therefore T
does not prove Con(T). QED
2. r.e. agreement theorems
Two sets A,B agree at x if and only if (x in A iff x in B).
THEOREM 2.1*. There is an r.e. set which agrees somewhere with every
r.e. set. In fact, this property of r.e. sets is equivalent to being
an r.e. set that is not recursive.
Proof: {e: e in W_e} agrees with any W_n at n, because
n in W_n if and only if n in {e: e in W_e}.
For the second claim, let A be r.e. Note that
A agrees somewhere with every r.e. set
if and only if
A is not the complement of any r.e. set
if and only if
A is not both r.e. and co r.e.
if and only if
A is not recursive.
QED
*Pointed out to me in https://cs.nyu.edu/pipermail/fom/2017-December/020741.html
We now need a sharper version of the property "A is an r.e. set that
agrees somewhere with every r.e. set".
DEFINITION 2.1. A is a remarkable r.e. set if and only if A is an r.e.
set, where for every r.e. set B there exists e such that ISigma_0
proves A.B agree at e.
THEOREM 2.2. There is a remarkable r.e. set.
Proof: Same as for Theorem 2.1. QED
3. PROVING GSIT
GSIT. Let T be a consistent r.e., axiomatized theory containing
ISigma_0. Then T does not prove Con(T).
Proof: By Theorem 2.2, let A be a remarkable r.e. set. Let B be the
r.e. set {e: T proves (e not in A)}.
Fix n* such that
K proves (n* in A if and only if T proves (n not in A)).
Then
1) n* in A if and only if T proves (n* not in A).
2) n* in A implies T proves (n* in A).
3) n* not in A and T does not prove (n* not in A).
Note that 3) follows from 1),2), and that T is consistent. The above
argument has been carried out external to T.
Note also that the above argument can be carried out in T + Con(T). In
particular, the first conjunct of 3) gets modified to: T + Con(T)
proves n* not in A. So if T proves Con(T) then T proves n* not in
A, contradicting the unmodified second conjunct of 3). Therefore T
does not prove Con(T). QED
4. FOR RECURSION THEORISTS
What are the remarkable r.e. sets?
Can an understanding of the remarkable r.e. sets give an even simpler
proof of GSIT? Maybe one that is yet farther away from diagonalization
than ours in 1 above?
************************************************************************
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 778th 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/15/17 10:14PM
772: Algorithmic Unsolvability 3 10/19/17 2:41AM
773: Goedel's Second: Proofs/1 12/18/17 8:31PM
774: Goedel's Second: Proofs/2 12/18/17 8:36PM
775: Goedel's Second: Proofs/3 12/19/17 12:48AM
776: Logically Natural Examples 1 12/21/17 8:45AM
777: Goedel's Second: Proofs/4 12/28/17 8:02PM
Harvey Friedman
More information about the FOM
mailing list