Gödel’s incompleteness theorems, on SEP at last

The Stanford Encyclopedia of Philosophy (what would we do without it?) has at last filled one of its notable gaps in coverage: there is now a entry by Panu Raatikainen on Gödel’s Incompleteness Theorems. It isn’t quite how I would have written such an entry, but it is clear and very sensible, and certainly won’t lead the youth too badly astray (which needs to be said when it comes to discussions of these things!).

Here, though, are a few comments. I start with three places where the discussion could perhaps mislead:

(1)  There’s an early section on ‘The Relevance of the Church-Turing Thesis’, which starts

Gödel originally only established the incompleteness of a particular though very comprehensive formalized theory P, a variant of Russell’s type-theoretical system … it was, at the time, unclear just how general [his result] really was … What was still missing was an analysis of the intuitive notion of decidability, needed in the characterization of the notion of an arbitrary formal system.

This rather suggests that we only get a clean general result round about 1936 when we have homed in on a sharp general account of effective decidability. But of course, Gödel’s original paper already gives a perfectly sharp general formulation: if the axioms and rules of inference of a theory T are primitive-recursively definable, and T represents every primitive recursive relation, then T is incomplete so long as omega-consistent (and indeed there will be arithmetical sentences undecidable by T). Moreover, the restriction here to primitively-recursively axiomatized systems is no real restriction. And I’m not thinking here of the technical point that any recursively axiomatized theory can be primitive-recursively re-axiomatized; there’s a more humdrum point — any effectively axiomatized system you are likely to dream up will already be primitive-recursively axiomatized (unless we are trying to be perverse, we don’t ordinarily define a class of axioms, for example, in such a way that it will require an open-ended search to determine whether a given sentence belongs to the class). So: I think it would be better to say that Gödel 1931 already gives a beautifully general result. And the fact that we can extend it from the primitively-recursively axiomatized to recursively axiomatized theories is pretty much a technical footnote.

(2) In the section describing how the First Theorem might be proved, we read

The next and perhaps somewhat surprising ingredient of Gödel’s proof is the following important lemma … The Diagonalization Lemma

Let A(x) be an arbitrary formula of the language of F with only one free variable. Then a sentence D can be mechanically constructed such that

F ⊢ D ↔ A(^⌈D^⌉).

Well, not Gödel’s proof. As in fact Raatikainen himself notes later.

As to the Diagonalization Lemma, actually Gödel himself originally demonstrated only a special case of it, that is, only for the provability predicate. The general lemma was apparently first discovered by Carnap 1934.

But that’s still wrong on both counts. Gödel didn’t state even the restricted version in 1931, nor in his 1934 lectures. Nor does Carnap’s 1934 Logische Syntax der Sprache. 

We need to distinguish two different claims, which we might call the Diagonal Equivalence  and the Diagonal Lemma. The Lemma we have just met, and is a syntactic claim about what can be proved. The Equivalence is a semantic claim, to the effect that given an arbitrary formula A(x) we can construct as sentence D such that D is true on interpretation just in case A(⌈D⌉) is. And it is this semantic Equivalence claim that Gödel refers to in his 1934 lectures.

Now, in §35 of his 1934, Carnap neatly proves the general Diagonal Equivalence, and in §36 he uses this, together with the assumption that not provable is expressible by an open wff in his Language II to show that Language II is incomplete. But note that constructing the semantic Diagonal Equivalence is not to establish the Diagonalization Lemma. And Carnap doesn’t actually state or prove that in his §35. And when we turn to §36, we see that Carnap’s argument for incompleteness is the simple semantic argument depending on the assumed soundness of his Language II. So at this point Carnap is giving a version of the semantic incompleteness argument sketched in the opening section of Gödel 1931 (the one that appeals to a soundness assumption), and not a version of Gödel’s official syntactic incompleteness argument which appeals to omega-consistency. Indeed, Carnap doesn’t even mention omega–consistency in the context of his §36 incompleteness proof. He doesn’t need to.

Anyway, neither Gödel 1931 or 1934 nor Carnap 1934 state the modern syntactic Diagonalization Lemma (as opposed to the semantic Equivalence). And I’m not sure who first did.

(3) We’ve just touched on the point that Gödel 1931 has two proofs that there are undecidable sentences in sufficiently rich theories, the first one depending on the semantic assumption that the theory is sound (and the weak assumption that it can express primitive recursive relations), the other depending on the syntactic assumption that the theory is omega-consistent (and the stronger assumption that it can represent p.r. relations). Students ought to know this, or they will get confused when they read some other discussions.

Well, Raatikainen does bury some relevant remarks at the end of his piece. He speaks of

a weak version of the incompleteness result: the set of sentences provable in arithmetic can be defined in the language of arithmetic, but the set of true arithmetical sentences cannot; therefore the two cannot coincide. Moreover, under the assumption that all provable sentences are true, it follows that there must be true sentences which are not provable. This approach, though, does not exhibit any particular such sentence.

But this perhaps forgets that Gödel’s own initial semantic argument (p. 149 in Collected Papers Vol. I) does of course exhibit a particular undecidable sentence.

A couple more observations. First, I thought section on ‘Feferman’s Alternative Approach to the Second Theorem’ was probably too compressed to be very useful.  Second, it is natural to ask: are there ‘ordinary’ arithmetical statements which (like Gödel sentences) we can frame in the language of PA, which are also unprovable in PA, though we can prove them true using richer resources? The section on ‘Concrete Cases of Unprovable Statements’ addresses this, briefly, but then moves on to talking about unprovable statements in richer languages, unprovable in richer theories. Students might be puzzled about whether there is supposed to be any unity to these examples and what, if anything, they are supposed to show which they haven’t learnt from Gödel’s theorems.

But all that said, it is excellent to see the SEP filling an obvious gap with an accessible and (mostly) very clear discussion!