[FOM] 306:Godel's Second/more

Sat Dec 23 19:02:39 EST 2006

1. A SEMANTIC FORM OF GODEL'S SECOND.

THEOREM 1.1. No consistent many sorted finitely axiomatized extension of PA
can be self interpreted using arithmetic formulas only.

INFORMAL COROLLARY 1. No consistent many sorted finitely axiomatized
extension of PA can prove its own consistency.

Proof: If so, then it has an interpretation of itself using arithmetic
formulas only, via the completeness theorem, which obviously uses only the
most basic properties of a proof predicate. QED

INFORMAL COROLLARY 2. PA does not prove its own consistency.

Proof: First prove in PA that Con(PA) implies Con(ACA0), using cut
elimination. If PA proves its own consistency then PA proves Con(ACA0). Now
apply Theorem 1.1. QED

INFORMAL COROLLARY 3. No consistent many sorted recursively axiomatized
extension of PA can prove its own consistency.

Proof: One can adapt the proof of Informal Corollary 2. QED

Other semantic forms, with stronger informal Corollaries, were discussed
earlier on FOM. See the references in #305.

2. PROOFS OF GODEL'S SECOND.

Here are two reviews from SciNet of existing proofs. I am still looking for
a new kind of proof. The bizarre thing about Godel's second is that proofs
use some sort of mysterious diagonalization or self reference, which is
usually thought to be good for proving existence statements - e.g., in
Cantor - not universal statements such as Godel's second.

MR2060929 (2005d:03100) 03F03
Kotlarski, Henryk
The incompleteness theorems after 70 years. (English summary)
Provinces of logic determined.
Ann. Pure Appl. Logic 126 (2004), no. 1-3, 125?138.
The author gives a survey on alternative methods to prove G¨odel?s
incompleteness theorems (and related results), in particular without use of
the diagonal lemma. The following results are addressed:
?1. A proof of Tarski?s theorem on undefinability of truth using the
existence of nonrecursively saturated models instead of the diagonal lemma.
2. Kikuchi?s proof from [M. Kikuchi, Math. Logic Quart. 40 (1994), no. 4,
528?532; MR1301944 (95j:03095)] (it is based on Berry?s paradox; Kikuchi?s
work extends earlier work of G. S. Boolos [Gac. R. Soc. Mat. Esp. 4 (2001),
no. 3, 521?527; MR1885109 (2002k:03100)]).
3. My proof from [H. Kotlarski, J. Symbolic Logic 59 (1994), no. 4,
1414?1419; MR1312319 (96c:03111)] (it turned out that it is based on the
socalled busy beaver problem).
4. Adamowicz?s idea from [Z. Adamowicz and T. Bigorajska, J.
Symbolic Logic 66 (2001), no. 1, 349?356; MR1825189 (2002b:03122)] (it is a
link between the incompleteness phenomena and the idea of existentially
closed models)? (p. 126).
Reviewed by Reinhard Kahle

MR1191869 (94g:03018) 03B10 (03C62 03F25)
Jech, Thomas (1-PAS)
On G¨odel?s second incompleteness theorem. (English summary)
Proc. Amer. Math. Soc. 121 (1994), no. 1, 311?313.
A special case of Godel?s second incompleteness theorem (that no
sufficiently strong consistent theory can prove its own consistency) is
stated as the following theorem: It is unprovable in set theory (unless set
theory is inconsistent) that there exists a model of set theory. A short
model theoretic proof of this theorem (using the completeness theorem) is
provided. It is also shown how the argument can be modified to apply to
weaker theories such as Peano arithmetic.
Reviewed by Stanisław J. Surma

**********************************

I use http://www.math.ohio-state.edu/%7Efriedman/ for downloadable
manuscripts. This is the 306th 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
305: Proofs of Godel's Second  12/21/06  11:31AM

Harvey Friedman