[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