What are some proofs of Godel's Theorem which are *essentially different* from the original proof?

Question

I am looking for examples of proofs of Godel's (First) Incompleteness Theorem which are essentially different from (Rosser's improvement of) Godel's original proof.

This is partly inspired by questions two previously asked questions:

(Proofs of Gödel's theorem)

(When are two proofs of the same theorem really different proofs)

To give an example of what I mean: The Godel/Rosser proof (see http://www.jstor.org/pss/2269059 for an exposition) shows that any consistent sufficiently strong axiomatizable theory is incomplete. The proof uses a substantial amount of recursion theory: the representability of primitive recursive functions and the diagonal lemma (roughly the same as Kleene's Recursion Theorem) are essential ingredients. The second incompleteness theorem - that no consistent sufficiently strong axiomatizable theory can prove its own consistency - is essentially a corollary to this proof, and a rather natural one at that. On the other hand, in 2000 Hilary Putnam published (https://doi.org/10.1305/ndjfl/1027953483) an alternate proof of Godel's first incompleteness theorem, due to Saul Kripke around 1984. This proof uses much less recursion theory, instead relying on some elementary model theory of nonstandard models of arithmetic. The theorem proven is slightly weaker, since Kripke's proof requires $\Sigma^0_2$-soundness, which is stronger than mere consistency (although still weaker than Godel's original assumption of $\omega$-consistency).

Kripke's proof is clearly sufficiently different from the Godel/Rosser proof that it deserves to be considered a genuinely separate object. What makes the difference seem really impressive, at least to me, is that Kripke's proof yields a different corollary than that of Godel/Rosser. In a short paragraph, Putnam shows (and I do not know whether this part of his paper is due to Kripke) that Kripke's argument proves that there is no consistent finitely axiomatizable extension of $PA$. This is not a result which I know to follow from the Godel/Rosser proof; moreover, the Second Incompleteness Theorem, which is a corollary to Godel/Rosser's proof, does not seem easily derivable from Kripke's proof.

Motivated by this, say that two proofs of (roughly) the same theorem are essentially different if they yield different natural corollaries. Clearly this is a totally subjective notion, but I think it has enough shared meaning to be worthwhile.

My main question, then, is:

1. What other essentially different proofs of something resembling Godel's First Incompleteness Theorem are known? In other words, is there some other proof of something close to "every consistent axiomatizable extension of $PA$ is incomplete" which does not yield Godel's Second Incompleteness Theorem as a natural corollary?

I am especially interested in proofs which don't yield the nonexistence of consistent finitely axiomatizable extensions of $PA$, either, and in proofs which do yield some natural corollary. I don't particularly care about the precise version of the First Incompleteness Theorem proved: if it applies to systems in the language of second-order arithmetic, if it assumes $\omega$-consistency, or if it only applies to systems stronger than $ATR_0$, say, that's all the same to me. However, I do require that the version of the incompleteness theorem proved apply to all sufficiently strong systems with whatever consistency property is needed; so, for example, I would not consider the work of Paris and Harrington to be a good example of this.

The only other potential example of such an essentially different proof that I know of is the proof(s) by Jech and Woodin (see https://andrescaicedo.files.wordpress.com/2010/11/2ndincompleteness1.pdf), but I don't understand that proof at a level such that I would be comfortable saying that it is in fact an essentially different proof. It seems to me to be rather similar to the original proof. Perhaps someone can enlighten me?

Of course, entirely separate from my main question, my characterization of the difference between the specific two proofs of the incompleteness theorem mentioned above may be incorrect. So I'm also interested in the following question:

2. Is it in fact the case that Kripke's proof does not yield Second Incompleteness as an natural corollary, and that Godel/Rosser's proof does not easily yield the nonexistence of a consistent finitely axiomatizable extension of PA as a natural corollary?

Answer 1

The question hinges on the best answer to a previous question, when are two proofs the same? I believe that the only satisfactory answer to this earlier question is by considering the construction implicit in the proof. Two proofs are the same when they give the same construction.

To isolate a construction, one must carefully distinguish between a proof of statements of the form "There exists..." and "For all...", and one must also distinguish between a statement and its double negation. For the purposes of practically distinguishing proofs, one does not need to be so pedantic most of the time. For example, the "topological proof" of the infinity of primes is essentially the same as Euclid's proof, because given a collection of primes, when unpacked to its construction, it builds the same number.

One must note here that the problem of deciding when two programs produce the same answers is undecidable, even more so when the programs have access to oracles, which is necessary sometimes. Further complicating matters is the fact that certain programs are only superficially different to the eye, but are essentially the same. Nevertheless, I think this is a useful heuristic, which has a chance of having a precise counterpart.

The construction in Godel's theorem is often obscured by the heavy coding involved. Since today, coding is standardized in computer science, I prefer to state the construction explicitly as a computer program, instead of as a coded statement of first-order logic. Two proofs are the same when they construct the same computer program.

There are exactly three types of unpacked proofs of Godel's theorem and related results, as far as I know. To save typing, a program P "runs" iff it does not halt.

---

TYPE I: self referential pi-0-1 statements (statements about the non-halting of a certain computer program)

GODEL_1: To prove Godel's theorem Godel's way (as clarified by Turing and Kleene), given an axiomatic system S whose deduction system is computable, you construct the program GODEL which does the following:

1. It prints its own code into a variable R. (This is possible since you can write quines, and make quining into a subroutine)
2. It deduces all consequences of S, looking for a proof in S of the statement "R does not halt" ("R runs").(This is a statement of arithmetic of the form "forall n F^n(R) is non-halting", where F is a primitive recursive instruction set for any computer you care to code up).
3. If it finds this statement, it halts.

The statement G--- "GODEL runs" is true precisely when S does not prove it. So G states "S does not prove G". The self reference is obvious in the first step of the program. This is equivalent to Godel's original construction.

From the construction, you can read off the requirements on the axiom system. In order to be sure that GODEL halting leads a contradiction, the axiom system has to be able to prove every statement of the form "program P leads to memory state M after time t" for all integer times t, and for all programs P. Each of these statements is a finite computation, a sigma-0-1 statement, so the axiom system must be able to prove all true sigma-0-1 statements (or even just a subset of these rich enough to allow a computer to be embedded in the language).

GODEL_2: Note that if S is inconsistent, it proves every statement, including "GODEL runs", so "S is inconsistent" implies "GODEL halts". "GODEL halts" also implies "S is consistent", if S can prove that it is sigma-0-1 complete. So the unprovability of "GODEL halts" is tantamount to the unprovability of consis(S).

But S can (falsely) prove "GODEL halts", without any contradiction, so long as GODEL never actually halts. This is saying that it is possible for an axiom system to prove its own inconsistency without actually being inconsistent, just by telling lies about computer programs. The assumption that S is omega consistent (or even just sigma-0-1 sound), means that it does not prove "P halts" unless P actually halts. So the same construction of GODEL proves the second incompleteness theorem as stated by GODEL, an omega-consistent system (or a sigma-0-1 sound system) cannot prove its own consistency.

The proofs of Godel's theorem which go through the halting problem all give this construction.

ROSSER: The program ROSSER is just a slight modification of GODEL. ROSSER does this:

1. prints its code into a variable R
2. looks in S for a proof of 1. "R prints to the screen" or 2. "R does not print to the screen".
3. If it finds 1. It halts without printing, if 2, it halts after printing "hello".

Now note that a consistent S cannot prove 1 nor 2, because either way, there is a halting computation that contradicts the statement. So a consistent S is incomplete. If we call the statement "ROSSER prints to the screen" by the name R, and its negation 2 by the name "notR", then "ROSSER does not print" is iff equivalent to "S proves R before notR", which is the standard gloss for ROSSER's construction.

ROSSER's statement is different than GODEL statement, because the statement "ROSSER does not print" is not equivalent to the statement "S is consistent". But since the slightly different statement "ROSSER does not halt" actually is equivalent to "S is consistent", ROSSER's construction includes GODEL's construction in a simple way.

Here are some simple modifications which also prove Godel's theorem:

PROOF_LENGTH: Given a provable statement of length L bytes in an axiomatic system S, there is no computable function of L, f(L), which bounds the length of the proof of L (relatively short theorems can have enormously long proofs).

construct PROOF_LENGTH to do the following:

1. Print its own code into a variable R
2. look through all deductions of S of length up to f(|R|) bytes for a proof of "R prints ok"
3. If you finds it, halt without printing
4. If not, print "ok" and halt.

In this case, the construction is clarified with a gloss: suppose f(L) exists, then you can decide the halting problem by running through all proofs of length f(|"P halts"|) for a proof of "P halts". If you don't find it, then P doesn't halt.

This is also a proof of Godel's theorem, since if S is complete, then it will decide all statements of the form "P halts", and then you can compute the function f which is the length of the proof of the statement. But the program constructed is essentially the same as GODEL (actually ROSSER, in the version I gave here).

But the explicit construction does give you an important corollary: if you assume S is consistent, then just by the form of PROOF_LENGTH, you can see that PROOF_LENGTH has to print "ok" independent of the function f, since if it does not, this means it has found a proof that it didn't. So the assumption of consis(S) will collapse this f dependent enormously long proof to a short f-independent proof of the same statement.

This construction is just a finitary version of the original GODEL program, and this theorem is called the GODEL speedup theorem. The assumption of consis(S) reduces the length of proofs of certain statements by an amount greater than any computable function of the length.

LOB: Given an axiomatic system S, consider the program LOB which, given statement A, does the following:

1. Prints its code into R
2. Deduces consequences of S, looking for "R halts implies A"
3. if it finds this theorem, it halts.

"LOB halts" only if S proves "LOB halts implies A", and then S also proves "LOB halts", so it proves A by modus ponens, so LOB halts iff A. But "LOB halts" is equivalent to "(S proves LOB halts) implies A", and therefore to "(S proves (S proves A) implies A)". Therefore, S proves "S proves ((S proves A) implies A) iff (S proves A)". This theorem can be repackaged into an infinite sequence of ever more obscure statements, by replacing "LOB halts" with its different equivalent forms (some of which contain itself), and eventually closing the recursion. The full set of Lob statements is generated by a simple recursive grammar.

LOB's theorem does not prove Godel's theorem, but it extends it. The proof is of a similar kind.

TWEEDLEDEE and TWEEDEDUM: consider two programs as follows:

TWEEDLEDEE:

1. prints TWEEDLEDEE's code into ME, and TWEEDLEDUM's code into HE
2. looks for 1. ME runs 2. HE runs
3. if it finds 1. it halts, if it finds 2. it prints "tweedle-dee-dee!" and goes into an infinite loop.

TWEEDLEDUM:

1. prints TWEEDLEDUM's code into ME, and TWEEDLEDEE's code into HE
2. looks for 1. ME runs 2. HE runs
3. If it finds 1. it halts, if it finds 2. it prints "tweedle-dee-dum!" and goes into an infinite loop.

These give a kind of splitting theorem for axiomatic systems which satisfy the hypotheses of GODEL's theorem. "DEE runs" and "DUM runs" are both unprovable in S, since proving either one leads to a contradiction. "consis(S)" implies "DEE runs & DUM runs", and conversely "DEE runs & DUM runs" implies consis(S).

So if S is inconsistent, then one of TWEEDLEDEE or TWEEDLEDUM has to halt But which one? This is not decidable in S. That is, S+"DEE runs" is a theory which is strictly stronger than S, since it proves "DEE runs", but is weaker than S+"consis(S)" because it cannot prove "DUM runs".

To prove this, note that S proves "DEE runs or DUM runs", i.e. "DEE halts implies DUM runs". So if S also proved "DEE runs implies DUM runs", it would prove plain old "DUM runs", which is impossible.

The reason for the spurious print statement is just to make absolutely sure that the programs DEE and DUM, which are so similar, don't end up identical, which would wreck the proof (this subtlety is hard to see if you don't unpack the construction into an explicit program, but it is also easy to avoid by using different variable names, or extra spaces, or whatever).

This construction is strictly stronger than GODEL's. It shows that for any sound system S, the implication "DEE runs implies DUM runs" is unprovable. The construction provides a proof of Godel's theorem, although it is similar to ROSSER (The statement DEE halts is provably NOT the negation of "DUM halts", that's the whole point)

I wondered if this construction was in the literature for a long time. I recently ran across it in "The Realm of Ordinal Analysis" by Michael Rathjen (proposition 2.17 on page 14). He couldn't find it in the rest of the literature, but the methods are sufficiently well known (and sufficiently close to Rosser's) to make it folklore. But, as emphasized by Rathjen, the result is significantly stronger than the usual theorems.

TWEEDLE_N: To push this further into uncharted territory, consider the infinite sequence of programs TWEEDLE_N (where N is an integer)

TWEEDLE_N:

1. loops over M, printing the code of TWEEDLE_M into a variable R(M)
2. Deduces consequences of S, looking for a theorem of the form "TWEEDLE_M runs" for some M
3. If it finds this theorem, and M=N, it halts. If M != N, it goes into an infinite loop.

It is easy to see that either all TWEEDLE-N's run, or exactly one of them halts, something which S can prove, because steps 1+2 (which must be run simultaneously in two threads) are the same for all the programs. But S cannot prove that any single one of them runs.

To prove this, note that if there is an effective list of programs A_N (like the TWEEDLE's), you can make a program MERGE(A_N) which generates and runs all of the programs on parallel threads and halts exactly when any one of them does. Then S proves that either TWEEDLE_k runs or MERGE(A_r (r!=k)) runs. That is, TWEEDLE_k and MERGE(all the others) form a TWEEDLEDEE/TWEEDLEDUM pair. This means that it cannot prove that one runs implies the other runs.

The result is that for any computable partition of the TWEEDLE's into two disjoint subsets A and B, S cannot prove that the TWEEDLE_A's run implies the TWEEDLE_B's run, although consis(S) proves that all the TWEEDLE's run. The theories "S+all the TWEEDLE_A's run" are sound theories strictly between S and S+consis(S) in terms of Pi-0-1 content--- they prove new correct theorems about the non-halting of computer programs, but they are weaker than S+consis(S) (and weaker than each other in a way described by the partial order of set containment).

I like this theorem, because it is a proof which is very dastardly to translate to more traditional logic language. I think that computational language is more natural for these results.

I could go on making more complicated self-referential proofs (and I think this is an interesting thing to do, they all prove somewhat different things), but I will stop here to consider non self-referential proofs, which work at a higher level of the arithmetic hierarchy.

---

TYPE II: these prove that there exist total functions which are not provably total. The statements in this case are pi-0-2, statements about the totality of some computable function.

FASTER_GROWTH: Given axiomatic system S, consider all computable functions f from the integers to the integers that are proven to be total (that is, which halt for all arguments). Now construct the program FASTER_GROWTH(n) which does the following:

1. Lists the first n functions which are provably total, and computes their value at position n.
2. returns the biggest value at n, plus 1.

If S is sound for pi-0-2 statements, then there are infinitely many provably total functions, and FASTER_GROWTH halts at every input. Further, FASTER_GROWTH is eventually bigger than any function provably total in S. So "FASTER_GROWTH is total" is an unprovable true theorem.

The function FASTER_GROWTH is constructed entirely from other functions which are not equal to itself. The requirement on the theory is that when it proves a function is total, it is telling the truth, otherwise FASTER_GROWTH will get stuck in an infinite loop at some point. This is the pi-0-2 soundness. The pi-0-2 soundness proofs generally construct this type of thing, when unpacked.

The most common abbreviated form of this argument runs as follows: given an axiomatic system S, diagonalizing against all provably total recursive functions in the theory gives a total recursive function which the theory cannot prove is total. This argument is folklore.

Type II Godel theorems provide a different way to strengthen the axiom system, by adding the statement of the totality of FASTER_GROWTH. This statement implies consistency of S, but is strictly stronger, since consistency is not enough to ensure FASTER_GROWTH is total (you need some soundness).

---

TYPE III: nonconstructive theorem about a large class of statements, which do not provide an explicit unprovable statement, and so cannot be used to step up the heirarchy of systems.

BOOLOS: There is no computer program which will output the true answer to statements of the form "Integer N can be named using k bytes or less worth of symbols of Peano Arithmetic"

write program BOOLOS: 1. loops over all integers N, looking for the first N which requires more than M symbols to name, where M is the length of the symbols describing the output of BOOLOS, translated to arithmetic. 2. prints out N.

The contradiction means that BOOLOS does not work. Boolos is not so great, because it isn't focused on a particular system, but it's the same basic idea as...

CHAITIN: Which replaces the notion of definability with Kolmogorov complexity, which is definability by an algorithm. Write the program CHAITIN to do the following:

1. List all proofs of S, looking for "the Kolmogorov complexity of string Q is greater than N" (where N is the length of CHAITIN)
2. Print string Q

Now if S ever proves that the Kolmogorov complexity of any string is greater than the length of CHAITIN, then CHAITIN will make S into a sigma-0-1 liar (inconsistent). This proves that there is a completely effective bound on the maximum provable Kolmogorov complexity of any string. (this was given previously as an answer).

There is an infinite list of true sentences of the form "The Kolmogorov complexity of Q is N", since there are infinitely many strings and only finitely many programs of length less than N. But only a finite number of these theorems get decided by any given axiom system S. This is a less explicit proof, because you can't be sure which strings are unprovably complex, so there isn't a natural axiom to add on to strengthen the system.

The statement "the Kolmogorov complexity of Q is N", translated to Arithmetic, is forall P, there exists N, ((F^N(P) is a halted state with output Q) implies |P|>n), so that it's Pi-0-2.

---

Now to identify which proofs is what type:

• Self-referential sentence proofs--- type I (Godel, Rosser, Kleene, Post, Church, Turing, Smullyan, popular works)
• Epsilon-naught induction proofs--- these are type II, but specific to Peano Arithmetic. The general version is the one presented above (Kripke's proof, and Paris-Harrington, Goodstein, Hydra). The version they give is that the limit ordinal of all recursive provable ordinals is recursive but not provably recursive, but this is a type II argument.
• Jech/Woodin Set theory model proof--- despite all its elegance and generality, the proof is type 1 when formulated computationally. I will elaborate below
• Chaitin/Boolos--- type III. I don't know any other type IIIs.

By the way, I agree with Sergei that finite axiomatizability (although emphasized by Putnam for some reason) is not so important. That property depends on exactly how you choose your axioms. The completeness theorem is strong enough to get a general computation from only finitely many axioms. The proof of impossibility of finite axiomatization (when it holds) is that the theory is self-reflecting, it can prove the consistency of any finite fragment (this is true in PA, because PA proves the consistency of induction restricted to level N in the Arithmetic Hierarchy), and the axiomatization is weak, in that finitely many axioms are stuck in some finite fragment no matter how many times you use them. Self-reflection is interesting, but not that relevant for the incompleteness theorem.

To see that the Jech/Woodin proof is really a type I proof in disguise, it is important for the purpose of unpacking the construction to supplement the set theory with an effective procedure to give computational meaning to the models. This is just first order logic and the completeness theorem, as Andreas Caicedo states in the introduction. (To be continued --- I am too tired to avoid wrong statements--- sorry for the excessive length)

Answer 2

There are a couple well known proofs of incompleteness based on properties of PA degrees. PA degrees have been studied extensively in recursion theory.

A PA degree is a Turing degree that can compute a complete extension of PA. Obviously, to prove the incompleteness theorem, it's enough to show that no PA degree can be recursive. (If we had a consistent r.e. theory T extending PA that was not incomplete, then its completion would be recursive -- to decide whether $T \models \varphi$ or $T \models \neg \varphi$, simply look for a proof of $\varphi$ or $\neg \varphi$ from $T$, and because $T$ is assumed to be complete, this process always terminates and is hence recursive).

One way to see that there are no recursive PA degrees is to observe that any PA degree can compute a nonstandard model of PA via compactness and a Henkin construction. Now apply Tennenbaum's theorem that there are no recursive nonstandard models of PA.

Another way to see that there are no recursive PA degrees is with $\Pi^0_1$ classes. Every PA degree can compute a path through each $\Pi^0_1$ class (this is one direction of the Scott basis theorem). To finish, note that one can construct $\Pi^0_1$ classes that do not contain any recursive elements. For instance, there are $\Pi^0_1$ classes that contain only diagonally nonrecursive elements.

Answer 3

Besides the proofs already listed, one essentially different treatment which comes to mind is Gentzen's consistency proof of PA, which established that PA can prove the well-ordering of ordinal notations less than $\epsilon_0$ but could not prove the well-ordering of a notation for $\epsilon_0$, and that, in turn, the well-ordering of $\epsilon_0$ would suffice to prove the consistency of PA. Characterizing the proof-theoretic ordinal of a theory yields incompleteness results by an essentially different (and arguably far deeper / more general) route to that of Godel.

Answer 4

There’s also an “invariant definability” argument. I’ll sketch it quickly below, and then give an analysis to explain why I think it’s meaningfully different. Embarrassingly I can't find a source for it at the moment; I recall seeing it as a footnote in Kreisel's Model-theoretic invariants paper, but it doesn't seem to be there. Multiple authors have written on invariant definability (which this answer is not-so-secretly an advertisement of) so I haven't yet been able to conduct an exhaustive search for the reference, but when I find it I'll update this. Incidentally, this argument was referred to at the beginning of another answer of mine.

Below, “definable” means “definable without parameters.” For more pleasant language I'll call this argument the "Tarskian argument."

---

Argument

Let $T$ be an “appropriate” theory of arithmetic (say, $T\supseteq R$). We tweak Tarski’s undefinability theorem very slightly as follows. For $X\subseteq\mathbb{N}$ and $M\models T$, say that $X$ is pseudo-definable in $M$ if $X=D\cap \mathbb{N}$ for some definable $D\subseteq M$. We then have:

$(*)\quad$ Suppose $M\models T$. Then $Th(M)$ is not pseudo-definable in $M$.

The standard proof still works: supposing to the contrary that $\theta$ pseudo-defined $Th(M)$ in $M$, let $m$ be the Godel number of the formula $\eta(x)\equiv$ "$\theta$ fails on the number of the sentence gotten by plugging $x$ into the formula with number $x$" - appropriately formalized - and consider the sentence $\eta(\underline{m})$ (applying representability appropriately).

With this in hand we argue as follows. Suppose $S\supseteq T$ is computable and satisfiable. Then by representability we have that $S$ is pseudo-definable in $M$ for every $M\models T$. Taking $M\models S$, we have by $(*)$ that $S\not=Th(M)$, so $S$ is not complete.

---

Analysis

Now let me argue in favor of the Tarskian argument being a genuine variation.

First, there’s an easy negative observation: it applies to Willard’s self-verifying theories and so cannot yield the second incompleteness theorem as a direct corollary. More subjectively, the argument is fairly non-constructive, and doesn’t (as far as I can see) quickly yield a specific undecidable sentence.

Of course, this is also a feature of the many standard computability-theoretic arguments. I think there’s still a difference here - this time a positive one - due to the way the Tarskian argument interacts with the notion of invariant definability. There are a couple ways to frame this - see e.g. the beginning of the article Abstract Computability and Invariant Definability by Moschovakis for some discussion - and I'll use the following:

Definition:

• An arithmetic context is a set $\mathfrak{C}$ of models of Robinson's arithmetic $R$.

• For an arithmetic context $\mathfrak{C}$, a set $A\subseteq \mathbb{N}$ is $\mathfrak{C}$-invariantly definable if there is some formula $\varphi$ with $\varphi^M\cap\mathbb{N}=A$ for all $M\in\mathfrak{C}$.

(Here I’m indulging in the usual abusive conflation of $\underline{k}^M$ and $k$.)

• For a theory $E$ and an arithmetic context $\mathfrak{C}$, say that $E$ is $\mathfrak{C}$-satisfiable if some member of $\mathfrak{C}$ satisfies $E$.

Then the Tarskian argument in fact gives:

Proposition: Suppose $\mathfrak{C}$ is an arithmetic context. Then no $\mathfrak{C}$-satisfiable theory is $\mathfrak{C}$-invariantly definable.

(Since the computable sets are invariantly definable in every arithmetic context and every theory extending $R$ yields an arithmetic context, this is a generalization of essential undecidability.)

The point is that in general the $\mathfrak{C}$-invariantly definable sets need not support a good computability theory in any sense: by judiciously terrible choice of $\mathfrak{C}$, we can make the set of $\mathfrak{C}$-invariantly definable sets have basically no structural properties besides forming a Boolean algebra. So, for example, I don’t see how to whip up an analogue of the “inseparable c.e. sets” argument for arbitrary arithmetic contexts.

Of course, pathological arithmetic contexts are uninteresting, so it’s hard to argue that this aspect is actually valuable in any way. But it is - as far as I can tell - a nontrivial feature.

Answer 5

I seem to recall that in reasonable systems of arithmetic (there's got to be an algorithm for deciding whether a statement is an axiom, and there's got to be a proof-checking algorithm, and a certain amount of arithmetic has to be provable) there are only a finite number of sequences that can be proved to be random in the Kolmogorov--Chaitin sense, although there must be infinitely sequences that are random in that sense.

Answer 6

Yet another one, very belatedly - this time proving the second incompleteness theorem! Below I assume some reasonable bijective (for simplicity) Godel numbering system. This is due to Adamowicz and Bigorajska, Existentially closed structures and Godel's second incompleteness theorem.

Fix an r.e. theory $T\supseteq I\Delta_0+\mathit{exp}$. Say that $M\models T$ is 1-closed (with respect to $T$) iff for every extension $M\prec_0 N\models T$, every $\overline{a}\in M$, and every $\Sigma_1$ formula $\varphi$, we have $\varphi(\overline{a})^M\leftrightarrow\varphi(\overline{a})^N$. If $T\subseteq\Pi_2$ then $T$ has a 1-closed model via a union of chains construction. If $T$ isn't $\Pi_2$-axiomatizable, we can always shift attention to its set $T_2$ of $\Pi_2$ consequences; note that $T_2\vdash \mathit{Con}(T_2)$ iff $T\vdash \mathit{Con}(T)$ iff [etc.], so this is a benign shift for our purposes.

OK, so WLOG assume $T\subseteq \Pi_2$. The usual proof of Tarski's undefinability theorem in fact does more; it applies to nonstandard models via taking standard parts, and it restricts to complexity classes, in the following sense:

(Extended TUT) Let $\Gamma$ be a syntactic class and $\mathcal{M}\models T$. Then there is no formula $\varphi\in\check{\Gamma}$ (= the set of negations of formulas in $\Gamma$) such that, for all standard sentences $\gamma\in\Gamma$, we have $$\mathcal{M}\models\gamma\iff\mathcal{M}\models\varphi\left(\underline{\ulcorner\gamma\urcorner}\right).$$

The classical TUT takes $\mathcal{M}=\mathbb{N}$ and $\Gamma=\check{\Gamma}=\mathit{Fmla}$, but the proof is the same.

The claim is now that any 1-closed model of $T$ must satisfy $\neg \mathit{Con}(T)$. To see this, suppose $\mathcal{M}\models T+\mathit{Con}(T)$ is $1$-closed and consider the formula $$\psi(\varphi,x)\equiv \mathit{Con}(T+\varphi(\underline{x}))$$ (the right hand side is phrased "internally" - of course, the thing plugged in for $x$ might be nonstandard, but $\mathcal{M}$ will still think that it has a numeral). Fix $\varphi\in\Sigma_1$ and $m\in\mathcal{M}$.

• If $\mathcal{M}\models\varphi(m)$, then by internal $\Sigma_1$-completeness and $\mathcal{M}\models\mathit{Con}(T)$ we get $\mathcal{M}\models\psi(\varphi, m)$. Note that this does not use 1-closedness.

• Now suppose $\mathcal{M}\models\psi(\varphi,m)$. Adding constants to the language to name all elements of $\mathcal{M}$, let $T'$ be the theory consisting of $T$, the $\Sigma_1$ diagram of $\mathcal{M}$, and $\varphi(m)$. By $\Sigma_1$-completeness we get that $T'$ is (externally) finitely consistent, and so (externally) satisfiable. Fix an extension $\mathcal{M}\prec_0\mathcal{N}\models T'$, we get $\mathcal{N}\models\varphi(m)$ and so by 1-closedness $\mathcal{M}\models\varphi(m)$.

At this point we have a contradiction with the extended TUT above!

---

As an amusing aside, note that in fact every model of a "reasonable" theory can be extended to one that thinks that that theory is inconsistent. The simplest proof of that uses GIT2, but we can also attack it as follows: letting $T$ be "appropriate" with $\mathcal{M}\models T$ and $T'$ be the $\Pi^0_2$-consequences of $T$, we can find extensions $\mathcal{M}\prec_0\mathcal{N}\prec_0\mathcal{S}$ with $\mathcal{N}\models T'$ 1-closed with respect to $T'$ and $\mathcal{S}\models T$. But then $\mathcal{N}\models \neg Con(T')$ and hence $\mathcal{N}\models\neg Con(T)$, and this is upwards-absolute to $\mathcal{S}$.

Answer 7

One of the Smullyan books. I think this one...
Raymond M. Smullyan, The Lady or the Tiger? And Other Logic Puzzles Including a Mathematical Novel That Features Godel's Great Discovery

After many years I can no longer tell you how like or different it is to Gödel's original proof.

Answer 8

The motivation of your interest in finding the proof of the general first incompleteness theorem which does not 'naturally' (whatever you mean by that) imply the non-existence of finitely axiomatizable extensions of PA is unclear to me. For I would not overestimate the significance of the later (as long as you do not restrict yourself to the language of PA only, which seems unnecessarily restrictive to me). For if just one new unary predicate symbol is added to the language of PA, then the finitely axiomatized conservative extension of PA can already be constructed. This follows from the general result of Craig and Vaught extended from the one of Kleene. You can find the details and references here.