[FOM] 777: Goedel's Second: Proofs/4
Noah Schweber
schweber at berkeley.edu
Thu Dec 28 20:02:01 EST 2017
I may be misunderstanding something - apologies if so - but what is the
difference between "agrees somewhere with" and "is not the complement of"?
It seems to me that as stated, A agrees somewhere with B iff A is not
exactly the complement of B. If so, of course, the r.e. sets which agree
somewhere with every r.e. sets are exactly the non-recursive r.e. sets.
On Thu, Dec 28, 2017 at 10:52 AM, Harvey Friedman <hmflogic at gmail.com>
wrote:
> RADICALLY (?) SIMPLIFIED(?) PROOF OF GOEDEL'S SECOND INCOMPLETENESS THEOREM
>
> This is a sequel to https://cs.nyu.edu/pipermail/
> fom/2017-December/020729.html
>
> 1. {e: T proves (e not in W_e)}
> 2. r.e. agreement theorems
> 3. proving GSIT
> 4. For recursion theorists
>
> I feel more comfortable with GSIT as the abbreviation for Goedel's
> Second Incompleteness Theorem.
>
> 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.
>
> 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}.
>
> QED
>
> We don't need the following Theorem 2.3 for GSIT.
>
> LEMMA 2.2. Suppose A agrees somewhere with every r.e. set. Let f:N
> into N be a recursive bijection. Then f[A] agrees somewhere with every
> r.e. set. I.e., the property "agreeing somewhere with every r.e. set"
> is preserved under recursive isomorphism.
>
> Proof: Let A,f be as given. Let B be an r.e. set. Then A and f^-1[B]
> agree somewhere, say at n. Hence f[A] and B agree at f(n). QED
>
> THEOREM 2.3. Every complete r.e. set agrees somewhere with every r.e. set.
>
> Proof: Let A be complete r.e. By classical recursion theory, all
> complete r.e. sets are recursively isomorphic, and {e: e in W_e} is
> complete r.e.. Hence A and {e: e in W_e} are recursively isomorphic.By
> Theorem 2.1, {e: e in W_e} has "somewhere agreement with every r.e.
> set", and so by Lemma 2.2, A has "somewhere agreement with every r.e.
> set". QED
>
> We do need the following very explicit form of Theorem 2.1 for GSIT.
> This is obvious from the proof of Theorem 2.1.
>
> THEOREM 2.4. There is an r.e. set A and a very weak system W of
> arithmetic such that the following holds. For any r.e. set B, there
> exists n such that W proves A,B agree at n.
>
> NOTE: We can contemplate Theorem 2.4 nicely without having to look at
> the blatantly "technical" construction {e: T proves (e not in W_e)}.
>
> 3. PROVING GSIT
>
> 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: By Theorem 2.4, let A be an r.e. set such that the following
> holds. For any r.e. set B, there exists n such that K proves A,B agree
> at n.
>
> 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
>
> Analyze the property of an r.e. set A that: A agrees somewhere with
> every r.e. set.
>
> Also consider various effective forms of the property "A agrees
> somewhere with every r.e. set".
>
> ************************************************************************
> 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 777th 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
>
> Harvey Friedman
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20171228/f67abb19/attachment.html>
More information about the FOM
mailing list