Diagonalization argument for indecidability of consistent theories

Question

I am trying to understand the classical proof that no consistent, sufficiently strong, axiomatised formal theory is decidable. I have a hard time to grasp the diagonalization argument used in the proof

Answer 1

I'm assuming you're talking about the diagonal lemma. For simplicity, I'm going to talk about the special case of PA.

In my opinion, the diagonal lemma is poorly named (and I prefer calling it the "fixed point lemma"). This is because neither it nor its application in the proof of Godel's theorem are really - in my opinion at least - classical diagonalization.

Its role is the following:

• We start with the Godel numbering function $\ulcorner\cdot\urcorner:Sentences\rightarrow\mathbb{N}$. There are many such functions; our hope is that the one we've picked is "reasonable," in the sense that basic properties of sentences wind up corresponding to definable properties of numbers. See the last bulletpoint below.

• The goal of the fixed point lemma is to let us perform some measure of self reference: sentences of arithmetic refer directly only to numbers, but via Godel numbering we can interpret them (at least sometimes) as saying things about sentences; in light of this, it's at least plausible that we could somehow cook up a sentence which "talks about itself" in some way. The fixed point lemma says that this is "maximally possible" - for any property $P$ of sentences whose "push-forward" under $\ulcorner\cdot\urcorner$ is definable in $\mathcal{N}$, we can express "This sentences has property $P$." Put another way, the fixed point lemma says - contra the intuition one might reasonably develop from the Liar paradox or similar - that self-reference is not inherently problematic; we've got a lot of it right here in arithmetic!

  • Note that this immediately gives Tarski's undefinability theorem: if the Godelization of the true theory of arithmetic, $\{\ulcorner\varphi\urcorner: \mathcal{N}\models\varphi\}$, were definable, then we could express "is the Godel number of a sentence which is false in $\mathcal{N}$" in the language of arithmetic; applying the fixed point lemma, we would be able to write "This statement is false," leading to a contradiction.

  • Note also that we're really proving things about the specific map $Sentences\rightarrow\mathbb{N}$ (that is, $\ulcorner\cdot\urcorner$) we've picked. Basically, a large part of the proof of Godel's theorem boils down to the statement, "There is a map $Sentences\rightarrow\mathbb{N}$ with [special properties]." Any such map would do. Incidentally, we can use this perspective to rephrase Tarski's undefinability theorem in a perhaps-less-mysterious way: it says that for any map $\mu: Sentences\rightarrow\mathbb{N}$, either this map lacks certain nice properties or the set $\{\mu(\varphi):\mathbb{N}\models\varphi\}$ is not definable in the language of arithmetic.

  • The focus on the specific map is also worth pointing out since this sort of statement makes sense in wide generality: given a structure $\mathcal{M}$ (here, the naturals) and a theory $T$ true of $\mathcal{M}$ (here, PA), we can talk about the relevant special properties which maps from sentences (in the language of $\mathcal{M}$) to $\mathcal{M}$ can possibly satisfy.

• OK, back to the topic. Phrased precisely, the fixed point lemma states that for any formula $\beta$ of one free variable, there is a sentence $\varphi$ such that PA proves $$\varphi\iff\beta(\ulcorner\varphi\urcorner).$$

• Now think back to the first bulletpoint. During our analysis of $\ulcorner\cdot\urcorner$, we show that "is provable" is definable; precisely, we show that the set $$\{\ulcorner\varphi\urcorner: PA\vdash\varphi\}$$ is definable in $\mathcal{N}$. Let $Prov$ be some formula defining this set. We now apply the fixed point lemma to $\neg Prov$ get a sentence $\theta$ such that PA proves $$\theta\iff \neg Prov(\theta).$$ Under reasonable assumptions on PA, we can show that $\theta$ is independent of PA.

  • Note that these "reasonable assumptions" are actually a bit stronger than mere consistency. To show that we really only need consistency - and this is crucial for the strong form of the incompleteness theorem you mention, since that applies to theories not satisfying this stronger condition - we use a trick due to Rosser. But the logical structure of the argument is the same.

---

Hopefully this shows how the fixed point lemma is used in Godel's theorem. There are of course a few gaps in the above outline. The one which is relevant here is:

How do we prove the fixed point lemma?

Unfortunately, the proof of the fixed point lemma - while short - is generally considered fairly unintuitive (just as with its computational analogue, the recursion theorem). Personally, I think working carefully through Wikipedia's writeup is a good way to learn it. But before you do so, I think it's better to understand the outline I've written above - you don't have to be confident that each piece works yet, but I think it is a good idea to internalize the overall strategy before diving into the specifics of the fixed point lemma.