# Proofs of Gödel's theorem

I am interested in different contexts in which Gödel's incompleteness theorems arise. Besides traditional Gödelian proof via arithmetization and formalization of liar paradox it may also be obtained from undecidability results of Turing and Church. In the context of complexity theory, it is not hard to see that Gödel's theorem (as well as Turing's result) follows from the following Chaitin's result: there exists some natural number N such that for any program P of size more than N it is impossible to prove (say, in ZFC) that it is the smallest (in the sense of size, i. e. number of bits) of those programs which have the same inputs-outputs as P has. The number N depends on particular axiomatic system (say, ZFC) and is not very large so that it actually can be calculated.

If You know other ways towards Gödel's incompleteness theorems, please, present them. Particularly, can Goedel's theorem be obtained without use of self-referential ideas?

-
You might be interested in the answers to this question: mathoverflow.net/questions/39626/… –  Peter Arndt Mar 22 '11 at 1:17
There is a categorical proof by Joyal, though it does use self-referential ideas. It makes use of arithmetic universes, which he introduced in the 70's. Their categorical structure supports the construction of internal categories providing internal copies of themselves, just the amount of self-reference needed to perform Cantor's diagonal argument. An abstract can be found at A. Joyal., The Gödel incompleteness theorem, a categorical approach. Cahiers de topologie et géometrie différentielle categoriques, 16(3), 2005. For a related work, see tac.mta.ca/tac/volumes/24/3/24-03abs.html –  godelian Mar 25 '11 at 20:31

Apart from usual proofs with diagonalization, have a look at model-theoretic proofs (Kotlarski's proof, Kreisel's left-branch proof, etc..), then there are some other proofs that formalize paradoxes (Kikuchi's, Boolos's, etc... there are about a dozen, most of them mentioned in Kotlarski's book).

If you don't want full generality ("for every rec. ax. theory T") then of course almost every proof in modern Unprovability Theory does not use any self-reference (you build a model of your theory by hands, using some unprovable combinatorial principle). Have a look at some easy recent accessible model-theoretic proofs of the Paris-Harrington Principle.

At the low end of the consistency strength spectrum (ISigma_n, PA, ATR_0), for theories that already have good classifications of their provably recursive functions, PH and other unprovable statements can also be proved unprovable using ordinal analysis (e.g. Ketonen-Solovay style), without using diagonalization tricks.

For higher ends of the strength spectrum (SMAH, SRP, etc), H. Friedman's highly technical results also don't use any diagonalization. This is a huge powerful machinery, and much new research is happening there.

MDRP theory gives interesting examples: have a look at the Jones polynomial expression: you can indeed substitute numbers into it and hit every consistency statement by its instances. There are similar ones for n-consistency for each n.

There is much more to say: this is a big subject, with huge bibliography. And, yes, much of the body of results in the subject is unpublished. I can give more pointers if necessary.

-
This is extremely interesting and, yes, please give more pointers. I'd like to know where to read about the Jones polynomial result. –  John Stillwell Mar 26 '11 at 0:18
Hi Andrey, welcome to MO! –  Andres Caicedo Mar 26 '11 at 5:51
Andrey, thank You very much for this detailed answer! Any more pointers, references and details from You would be very appreciated! –  Sergei Tropanets Mar 27 '11 at 9:49

Saul Kripke gave a proof of incompleteness using nonstandard models and a notion of "fulfillability". Roughly speaking, a sequence fulfills a (prenex) formula if the formula is true when its successive quantifiers are bounded by the terms of the sequence. Kripke apparently never published this, but Hilary Putnam presented in a lecture, subsequently published as "Nonstandard models and Kripke's proof of the Gödel theorem" [Notre Dame Journal of Formal Logic 41 (2000) pp. 53-58]. The MathSciNet review by Alex Wilkie reads:

"This paper was developed from a lecture given by the author at Beijing University in 1984 which described Kripke's notion of fulfillability and how it may be used to give a proof of the incompleteness of Peano arithmetic. Putnam has decided to publish it now because Kripke has still not published it himself. The point of this proof is that it is semantic and avoids self-reference, but is much simpler than the Paris-Harrington argument. It achieves this simplicity by considering a sentence that directly expresses the existence of long (finite) sequences of natural numbers that verify all the bounded approximations of the Peano Axioms, rather than deducing this existence, as Paris and Harrington had to, from a version of Ramsey's Theorem. Thus the simplicity comes at the cost of mathematical naturality. Also, although it is not made explicit in this paper, one still has to go through the process of Gödel numbering and the construction of a uniform satisfaction predicate for bounded quantifier formulas."

-
This is great! I'd heard of Kripke's proof but not about Putnam's paper. It's available for free at projecteuclid.org/euclid.ndjfl/1027953483. Incidentally, do you know what is up with the publication date? Volume 41 is clearly listed as "Publication Date: 2000" on the web site and in the PDF files, but Putnam's paper wasn't even received until 2001 and was printed in 2002. I figured one or the other must be a typo, but 2000 is repeated frequently, as is the bit about being printed in 2002, and Putnam's paper isn't the only one received in 2001. Does this make any sense? –  Henry Cohn Mar 21 '11 at 21:53
Warren Goldfarb also has a paper presenting Kripke's fulfillability proof: "Herbrand's theorem and the incompleteness of arithmetic," Iyyun vol. 39, pp. 45-64. –  Ed Dean Mar 21 '11 at 22:10
Henry, I believe the official publication dates of journals are sometimes fictitious. A journal wants to publish (and subscribers expect) a fixed number of issues per year, so, if they get behind on the publication schedule, some issues published in a later year may be assigned an earlier official publication date (and sent to whoever subscribed for that earlier year). –  Andreas Blass Mar 22 '11 at 12:41

In a recent AMS notices article, Shira Kritchman and Ran Raz give a proof of Godel's Second Incompleteness Theorem based on the Surprise Examination Paradox.

-

Possibly the least "self-referential" argument for Gödel's incompleteness theorem is the one due to Gentzen. His ordinal analysis of proofs in PA shows that any ordering that PA can prove to be a well-ordering has ordinal less than $\varepsilon_0$. Hence any ordering, definable in PA, that happens to be a well-ordering of length at least $\varepsilon_0$ cannot be proved to be a well-ordering in PA.

-
I see. But Gödel's incompleteness theorem talks not only about PA but any recursive extension of a system much weaker that PA. –  Sergei Tropanets Mar 21 '11 at 21:39

For Goedel's first incompleteness theorem, you can appeal to the existence of any computably (recursively) enumerable set $A$ that's not computable (recursive). Specifically, suppose $T$ is an $\omega$-consistent, computable theory powerful enough to represent all computable functions. Let $f$ be a total computable function listing all Natural numbers in $A$, and let $F$ represent $f$ in the theory $T$. Then there must exist $n \in \mathbb{N}$ for which:

(1) $T \nvdash \exists m F(m, n)$ nor (2) $T \nvdash \lnot\exists m F(m, n)$

Otherwise we could determine whether or not any given $n$ is in $A$ by effectively listing all theorems of $T$ until we received one of these statements, contradicting the fact that $A$ is not computable. Specifically, (1) would tell us that $n \in A$ by the $\omega$-consistency of $T$ (i.e., there exists a true Natural number $m$ so $f(m) = n$) while (2) would tell us that $n \notin A$ because it is never listed by $f$.

If I recall correctly, a proof along these lines is mentioned in An Introduction to Kolmogorov Complexity and Its Applications by Ming Li and Paul Vitányi.

-
You can't prove Godel from Turing. In fact Turing's Incompleteness Theorem is still open (the proof contains a hidden assumption of Euclidean space) due to the reappearance of negative energy in QM. If the Alcubierre drive works, Turing's fall is within reach. The resulting change is ω is directly computable. –  Joshua Dec 15 at 18:50

Gregor Lafitte's short paper: "G\"odel incompleteness revisited" is is a freely downloadable nice and concise overview of different kinds of proofs with a long list of references:

hal.archives-ouvertes.fr/docs/00/27/45/64/PDF/74-89.pdf

Supplement of 11th October 2011:

In a recent paper `The Surprise Examination Paradox and the Second Incompleteness Theorem', Notices of the AMS Volume 57, Number 11 (it can be downloaded from http://www.ams.org/notices/201011/rtx101101454p.pdf), the authors give a new proof for Godel’s second incompleteness theorem, based on Kolmogorov complexity, Chaitin’s incompleteness theorem, and an argument that resembles the surprise examination paradox.

-
Nice paper! Thank you. –  Sergei Tropanets May 27 '11 at 18:14
The Kritchman–Raz paper is already noted above in Jason Rute’s answer. –  Emil Jeřábek Oct 12 '11 at 9:50
Emil Jeřábek. The paper is worth to be noticed twice though. –  Sergei Tropanets Oct 21 '11 at 17:27

This is a comment on a post by Andreas Blass here.

I have not read Kripke's statement, apart from Andreas's sketch above, but it sounds familiar from elsewhere, so let me comment a bit on the family of results and the many discussions about a family of unprovable statements of the form "for every n there is a finite set that approximates a model of your theory T to the degree n" (where "to the degree n" is specified separately each time).

The first such statement found in print belongs to Paris and Harrington (see the original article in the Handbook for Mathematical Logic), and is sometimes referred to as "half-baked Paris-Harrington Principle". It says "for every n there exists a finite sequence of points that acts as diagonal indiscernibles for the first n Delta_0 formulas", where "diagonal indiscernibility" or "Paris indiscernibility" is the condition that for any c_i_0 < c_i_1< ... < c_i_k < c_j_1 < ... < c_j_k in the sequence, we have: for every parameter a < c_i_0, the following holds:

\forall x_1 < c_i_1 \exists x_2 < c_i_2.... \phi(a, x_1, x_2... x_k) < -- > \forall x_1 < c_j_1 \exists x_2 < c_j_2... \phi(a, x_1, x_2, ...x_k).

Since that time statements of this form became routine intermediate steps in unprovability proofs. For example Shelah tried to modify this statement and came up with something that should be of strength Pi_1^1-CA_0 (see "On logical sentences in PA").

The same idea is the core of most of Harvey Friedman's proofs in the last 25 years, but at higher levels of sophistication. For example for Proposition C, Friedman has 9 intermediate statements of this shape ("the Transmutations"), where the notion of indiscernibility changes at each step. And for Proposition B you need perhaps only 6 transmutations.

When I was entering the subject in 2002 -- 2003, I wrote a naive article draft on half-baked PH and beyond, tinkering and trying to generalize. But then I realized that this topic is widely developed and discussed in the unprovability community, so since this piece already entered the unprovability community's knowledge pot long before me, perhaps none of it is publishable.

One more thought: there are two or three ways of dressing unprovability proofs. Paris's original dressing was via cuts in models of arithmetic, but after Harrington's simplification of n-densities, they wrote the proof for the Handbook in the finitistic way, via half-baked Paris-Harrington + compactness as I sketched above. After that Paris and his co-workers returned to thinking in terms of cuts in models of arithmetic. Both ways of dressing the proof are equally good, but each person usually chooses one.

-

Dear Sergei and John. There is just too much to say. If I give you 3 pointers - it will not mean that these are good starting points or that these are the most important developments.

The Jones polynomial is from JSL 43 (1978), no 2. but me and De Smet recently enhanced the polynomial a bit (shortened it by 7 symbols)... :)

Friedman's book is on his homepage. The introduction is quite readable, and contains a long list of unprovable statements.

You can also have a look at my "Brief introduction" on my homepage, although I am a bit ashamed of that naive paper of mine written 6 years ago. I am now writing a long better piece, with all motivations and explanations, and the Arithmetical Splitting story.... but it will take some time.

-
Smorynski's article in the Handbook for Mathematical Logic is still relevant (at least you can read Kreisel's left-branch proof in there)... Kotlarski's book is still unpublished. As far as I know, Konrad Zdanowski and Zosia Adamowicz are working to have it published asap. –  andrey bovykin Mar 29 '11 at 11:25
Andrey, thanks for the clarification. At first I thought you meant the Jones polynomial from knot theory. –  John Stillwell Mar 29 '11 at 21:19