Diagonalization and the Diagonal Lemma

A couple of recent M-Phi posts by Catarina have discussed the topic of diagonalization and the Diagonal Lemma in Gödel's incompleteness results.
Because I can't be bothered to get out of bed, this post consists in some Sunday afternoon rambling about how diagonalization is usually understood and how the Diagonal Lemma is proved (i.e., how to define a fixed-point, or self-referential, sentence).
Gödel's original 1931 paper on incompleteness, "On Formally Undecidable Propositions in Principia Mathematica and Related Systems, I", is brimming with new ideas, of which four important ones are:

(i) the notion of what is now called a primitive recursive function;
(ii) arithmetization of syntax (aka, gödel coding);
(iii) the diagonalization operation on a string;
(iv) given any $\mathcal{L}$-formula $\varphi (x)$, the construction of a "fixed-point" or self-referential sentence $\theta$ equivalent to $\varphi (⌜\theta ⌝)$.

There are short explanations of each of these below.

1. The (Usual) First-Order Language of Arithmetic

The language of arithmetic $\mathcal{L}$ is a first-order language with identity, and with signature $\{\underset{―}{0},S,+,\times \}$ and is intended to talk about about the structure $\mathbb{N}=(\mathbb{N},0,S,+,\times )$. The set of $\mathcal{L}$-terms, $Tm(\mathcal{L})$, is defined inductively, by starting with $\underset{―}{0}$ and all variables, $x_i$, and then closing under applying the function symbols $S,+,\times$. Then, an atomic $\mathcal{L}$-formula is defined to be of the form $t=u$, where $t,u\in Tm(\mathcal{L})$. And the set of $\mathcal{L}$-formulas, $Form(\mathcal{L})$, is defined inductively, by starting with atomic formulas $t=u$, and then closing under applying the unary connective $\mathrm{\neg }$, the binary connective $\to$ and quantifiers $\mathrm{\forall }{x}_i$. (Other connectives, and $\mathrm{\exists }$, can be defined.)

It is useful sometimes to abuse notation and conflate the symbol $\underset{―}{0}$ and its denotation, the number $0\in \mathbb{N}$; or the symbol $S$ and its denotation, the function $S:\mathbb{N}\to \mathbb{N}$, etc. Context is usually sufficient to disambiguate. If one is considering a non-standard $\mathcal{L}$-interpretation $\mathcal{A}$ (i.e., $\mathcal{A}$ is not isomorphic to $\mathbb{N}$), then $S^{\mathcal{A}}$ will be the denotation of $S$ in $\mathcal{A}$; ${+}^{\mathcal{A}}$ the denotation of $+$, and so on.

Although taking $\underset{―}{0},S,+$ and $\times$ as undefined primitives is fairly standard, some presentations include the binary relation symbol $x<y$ and a binary function symbol $exp(x,y)$ (denoting the exponential function, $x^y$) as additional primitives. But in fact both can be defined in $\mathbb{N}$: for $x<y$, this is obvious, but for $exp(x,y)$, it is not so obvious.

A bounded quantifier has the form $(\mathrm{\forall }x\le t)$ or $(\mathrm{\exists }x\le t)$, where $t$ is a term, and $x\le t$ is the formula $\mathrm{\exists }z(x+z=t)$. A bounded formula $\varphi$ is a formula in which all quantifiers are bounded. A ${\mathrm{\Sigma }}_1$-sentence has the form $\mathrm{\exists }{x}_1\dots \mathrm{\exists }{x}_k\varphi$, where $\varphi$ is bounded.

2. Canonical Numerals for Numbers

Because of the presence of $\underset{―}{0}$ and $S$ in $\mathcal{L}$, there is a canonical way of denoting numbers, using canonical numerals. Roughly, the number $n$ is denoted by the term $S...S\underset{―}{0}$, with $S$ repeated $n$ times. More exactly, one defines a function

$\underset{―}{}:\mathbb{N}\to Tm(\mathcal{L})$,

by primitive recursion as follows:

$\underset{―}{0}:=\underset{―}{0}$
$\underset{―}{n+1}:=S\underset{―}{n}$

So, for example, the number 7 is denoted by $\underset{―}{7}$, which is the term $SSSSSSS\underset{―}{0}$. By induction, it is easy to prove that $(\underset{―}{n}{)}^{\mathbb{N}}=n$.

3. Robinson Arithmetic: $Q$

A very important weak system of arithmetic is Robinson arithmetic, $Q$. Its axioms are:

$(Q_1)\mathrm{\forall }x(Sx\ne \underset{―}{0})$
$(Q_2)\mathrm{\forall }x\mathrm{\forall }y(Sx=Sy\to x=y)$
$(Q_3)\mathrm{\forall }x(x\ne \underset{―}{0}\to \mathrm{\exists }y(x=Sy))$
$(Q_4)\mathrm{\forall }x(x+\underset{―}{0}=x)$
$(Q_5)\mathrm{\forall }x\mathrm{\forall }y(x+Sy=S(x+y))$
$(Q_6)\mathrm{\forall }x(x\times \underset{―}{0}=\underset{―}{0})$
$(Q_7)\mathrm{\forall }x\mathrm{\forall }y(x\times Sy=x\times y+x)$

It is noteworthy that $Q$ does not have as an axiom scheme the induction scheme,

$(\varphi (\underset{―}{0})\wedge \mathrm{\forall }x(\varphi (x)\to \varphi (Sx)))\to \mathrm{\forall }x\varphi (x)$

Extending $Q$ with the induction scheme gives Peano arithmetic.
The system $Q$ is sound and complete for certain classes of sentences. That is,

$Q⊢\varphi$ if and only if $\varphi$ is true.

This holds when $\varphi$ is a quantifier-free sentence, a bounded sentence or a ${\mathrm{\Sigma }}_1$-sentence.

In general, $Q$ can correctly perform finite computations using successor, addition and multiplication. However, $Q$ is not very good at algebra. For example, $Q$ does not prove $\mathrm{\forall }x\mathrm{\forall }y(x+y=y+x)$. Importantly, although $Q$ has axioms for addition and multiplication, it does not have axioms for exponentiation.

3. Gödel Coding

Under gödel coding, each primitive symbol $\alpha$ of the alphabet of $\mathcal{L}$ is given a code number, $c(\alpha )$. Also, each finite sequence $(n_1,\dots ,n_k)$ of numbers can be coded as a number, sometimes written as $⟨n_1,\dots ,n_k⟩$. For example, one might use the coding

$⟨n_1,\dots ,n_k⟩:=(p_1{)}^{n_1+1}\times \cdots \times (p_k{)}^{n_k+1}$,

where $p_1,p_2,\dots$ are the primes in ascending order, beginning with 2. (And we assign $0$ as the code of the empty string $()$.) For example, $⟨10,0,1⟩=2^{11}\times 3\times 5^2$. Such numbers are then called sequence numbers.

Because $\mathcal{L}$-strings are sequences of primitive symbols, the code of an $\mathcal{L}$-string $({\alpha }_1,\dots ,{\alpha }_k)$ is defined as:

$\mathrm{\#}({\alpha }_1,\dots ,{\alpha }_k):=⟨c({\alpha }_1),\dots ,c({\alpha }_k)⟩$.

(One needs to be a bit careful as the code of a primitive symbol, say $\mathrm{\forall }$, is not the same as the code of the corresponding one-element string $(\mathrm{\forall })$. For example, if $c(\mathrm{\forall })=10$, say, then $\mathrm{\#}(\mathrm{\forall })=2^{11}$.)

Because each $\mathcal{L}$-string $\varphi$ now has a code, say $n=\mathrm{\#}\varphi$, we can think of the numeral $\underset{―}{n}$ as a kind of name of $\varphi$. So, if $n=\mathrm{\#}\varphi$, then the numeral $\underset{―}{n}$ is written: $⌜\varphi ⌝$, and is sometimes called the gödel quotation name of $\varphi$.

So, using coding, the interpreted language of arithmetic is able to talk (indirectly) about the syntax of $\mathcal{L}$. For each syntactical entity $\varphi \in \mathcal{L}$ has a kind of name $⌜\varphi ⌝$ in $\mathcal{L}$ itself. Furthermore, special sets of (and relations amongst) syntactical entities become sets of numbers under coding. If $A$ is a set of syntactical entities, then $\mathrm{\#}(A)$ is $\{\mathrm{\#}(\alpha ):\alpha \in A\}$, the corresponding set of numbers. For example, the variables of $\mathcal{L}$ are coded as a set of numbers; the set of terms is coded as a set of numbers. Etc. Then one can ask whether these sets (or relations) are "expressible" in the language of arithmetic.

In general, these syntactical sets and relations come out, under coding, as either primitive recursive, or recursive, or recursively enumerable.

4. Primitive Recursive Functions

The primitive recursive functions are nowadays defined a bit differently from Gödel's original approach. (See this SEP article for more details.) First,

The basic functions:
(i) the zero function $Z:\mathbb{N}\to \mathbb{N}$, by $Z(n)=0$.
(ii) the successor function $S:\mathbb{N}\to \mathbb{N}$, by $S(n)=n+1$.
(iii) the projection functions $P_j^k:{\mathbb{N}}^k\to \mathbb{N}$ (with $j\le k$), by $P_j^k(n_1,\dots ,n_k)=n_j$.

One may then build up more functions by either composition, or by primitive recursion. That is, given functions $g:{\mathbb{N}}^k\to \mathbb{N}$ and $h:{\mathbb{N}}^{k+2}\to \mathbb{N}$, we say that $f:{\mathbb{N}}^{k+1}\to \mathbb{N}$ is obtained by primitive recursion from $g$ and $h$ just if, for all $x,y_1,\dots ,y_k\in \mathbb{N}$,

$f(y_1,\dots ,y_k,0)=g(y_1,\dots ,y_k)$
$f(y_1,\dots ,y_k,x+1)=h(x,y_1,\dots ,y_k,f(y_1,\dots ,y_k,x))$

The primitive recursive functions are then defined to be those functions obtainable from the basic functions by composition and primitive recursion.

There is a further operation on functions---minimization. Closing the primitive recursive functions under that operation then yields the recursive functions.

The notion of recursiveness can be extended to subsets of, and relations on, $\mathbb{N}$ by considering the characteristic function of the set or relation. Suppose $A\subseteq \mathbb{N}$. The characteristic function ${\chi }_A$ is defined by:

${\chi }_A(n)=1$ if $n\in A$, and 0 otherwise.

If ${\chi }_A$ is (primitive) recursive, we say that $A$ is (primitive) recursive.
For a relation $R\subseteq {\mathbb{N}}^k$, the definitions are analogous.

5. Representability in $Q$

There are two main notions of "expressing" a numerical function or relation. The first is semantical: given some set $A\subseteq \mathbb{N}$, simply whether there is an $\mathcal{L}$-formula $\varphi (x)$ such that

$A=\{n:\mathbb{N}\models \varphi (\underset{―}{n})\}$.

If so, we say that $\varphi (x)$ defines $A$.

The other notion is syntactical, and always involves a theory $T$ in $\mathcal{L}$. Given a function $f:{\mathbb{N}}^k\to \mathbb{N}$, we say $f$ is representable in $T$ just when there is an $\mathcal{L}$-formula $\varphi (x_1,\dots ,x_k,y)$ such that, for all $n_1,\dots ,n_k$,

$T⊢\mathrm{\forall }y(y=\underset{―}{f(n_1,\dots ,n_k)}\leftrightarrow \varphi (\underset{―}{n_1},\dots ,\underset{―}{n_k},y))$

Given a theory $T$, a similar notion can be applied to subsets, and relations on, $\mathbb{N}$. Suppose $A\subseteq \mathbb{N}$. We say that $A$ is strongly representable in $T$ just when there is some formula $\varphi (x)$, such that for all $n\in \mathbb{N}$,

(i) if $n\in A$ then $T⊢\varphi (\underset{―}{n})$
(ii) if $n\notin A$, then $T⊢\mathrm{\neg }\varphi (\underset{―}{n})$

We say that $A$ is weakly representable in $T$ just when condition (i) holds, but with "if ... then" replaced by "... iff ..." (thanks to Kai Wehmeier for the correction).
An analogous definition can be given for a relation $R\subseteq {\mathbb{N}}^k$ to be strongly or weakly representable.

The most important representation property for $Q$ is:

Representability in $Q$
All recursive functions are representable in $Q$.

To prove this, one shows first that each of the basic functions is representable in $Q$; and then one shows that the representable functions are closed under composition, primitive recursion and minimization. Details of how to do this are given in standard textbooks, such as H. Enderton, A Mathematical Introduction to Logic. As Aldo Antonelli notes in the comments below, in order to show that functions obtained by primitive recursion are representable, one needs to show how sequence coding and decoding can be expressed in $\mathcal{L}$, which only has $S,+$ and $\times$ as primitives. The crucial result required is Gödel's Beta Function Lemma, using the Chinese Remainder Theorem. These results need only to be proved in the metatheory, not in $Q$ itself (which lacks induction).
The converse of the representability theorem is true as well: if $f$ is representable in $Q$, then $f$ is recursive.

A corollary of the representation theorem for $Q$ is that all recursive sets and relations are strongly representable in $Q$. So, if $R\subseteq {\mathbb{N}}^k$ is recursive, there is a formula $\varphi (x_1,\dots ,x_k)$ such that, for all $n_1,\dots ,n_k\in \mathbb{N}$,

(i) if $R{n}_1\dots n_k$, then $Q⊢\varphi (\underset{―}{n_1},\dots ,\underset{―}{n_k})$.
(ii) if $\mathrm{\neg }R{n}_1\dots n_k$, then $Q⊢\mathrm{\neg }\varphi (\underset{―}{n_1},\dots ,\underset{―}{n_k})$.

As it turns out, for a standard axiomatic theory $T$, the set of (codes of) axioms is recursive (for example, a computer program can be written to decide of a given input string whether it is an axiom or not), indeed, primitive recursive. Furthermore, the proof-in-$T$ relation, "$d$ is a proof of $\varphi$ (in $T$)", is primitive recursive. So, there are $\mathcal{L}$-formulas which strongly represent (in $Q$) such relations. In particular, there is a formula $Pr{f}_T(y,x)$ which strongly represents the proof-in-$T$ relation: $y$ is the code of the proof-in-$T$ of formula with code $x$. Then the formula $\mathrm{\exists }yPr{f}_T(y,x)$ expresses "$x$ is a theorem of $T$" and is written $Pro{v}_T(x)$.

6. Diagonalization

Consider the binary syntactic operation on strings,

the result of substituting the quotation of string $A$ for all free occurrences of a variable in string $B$.

Although this is binary, obviously, one can take this operation on the same argument, i.e.,

the result of substituting the quotation of string $A$ for all free occurrences of a variable in string $A$.

Informally, this is (syntactic) diagonalization.
For example, the diagonalization of

$x$ contains 23 symbols

is

"$x$ contains 23 symbols" contains 23 symbols

If $\varphi$ is a formula of the language of arithmetic, with at most the variable $x$ free, then its diagonalization is defined to be:

$\varphi (x/⌜\varphi ⌝)$

I.e., the result of substituting the gödel quotation $⌜\varphi ⌝$ for all free occurrence of $x$ in $\varphi$.
An alternative, but equivalent (in predicate logic) is:

$\mathrm{\exists }x(x=⌜\varphi ⌝\wedge \varphi )$

Clearly, this syntactic operation of diagonalization corresponds to a numerical function, $d:\mathbb{N}\to \mathbb{N}$, given by, for any $\mathcal{L}$-string $\varphi$,

$d(\mathrm{\#}\varphi )=\mathrm{\#}(\varphi (x/⌜\varphi ⌝))$ if $\varphi$ is an $\mathcal{L}$-formula with at most $x$ free;
$d(n)=0$ if $n$ is not the code of such an $\mathcal{L}$-formula

One can show (the details are tedious) that $d$ is primitive recursive.
Because all recursive functions are representable in $Q$, it follows that there is an $\mathcal{L}$-formula $Diag(x,y)$ such that, for all $n\in \mathbb{N}$,

$Q⊢\mathrm{\forall }y(y=\underset{―}{d(n)}\leftrightarrow Diag(\underset{―}{n},y))$

7. The Diagonal (or Fixed Point) Lemma

Let $\varphi (x)$ be an $\mathcal{L}$-formula with at most $x$ free. (If $\varphi$ happens to have only one variables free, say $y$, but not $x$, then one can do a relabelling of variables to ensure that $\varphi$ has only $x$ free.) We want to find a formula $\theta$ that is in some sense equivalent to $\varphi (⌜\theta ⌝)$.
First consider informally, the expression,

the diagonalization of $x$ is $\varphi$

If one diagonalizes this, one gets,

the diagonalization of "the diagonalization of $x$ is $\varphi$" is $\varphi$

Call this statement $\theta$. Now $\theta$ says that a certain thing is $\varphi$. This thing is the diagonalization of "the diagonalization of $x$ is $\varphi$"---but this is precisely the statement $\theta$ itself. Such a statement $\theta$ is called a fixed-point sentence for the original formula $\varphi (x)$, and it says of itself that it is $\varphi$.

So, to get this into the formalized language $\mathcal{L}$, we begin with some formula $\varphi$ and we consider,

$\mathrm{\exists }y(Diag(x,y)\wedge \varphi (y))$

Call this formula $\psi (x)$. Let $\theta$ be the diagonalization of $\psi$. That is, $\theta$ is $\psi (⌜\psi ⌝)$. So, trivially, we have,

$⊢\theta \leftrightarrow \psi (⌜\psi ⌝)$

In particular, $\mathrm{\#}(\theta )=d(\mathrm{\#}(\psi ))$. So, the term $⌜\theta ⌝$ is the numeral $\underset{―}{d(\mathrm{\#}(\psi ))}$. And thus, trivially, we have

$⊢⌜\theta ⌝=\underset{―}{d(\mathrm{\#}(\psi ))}$

Furthermore, since $Q$ represents $d$, we have,

$Q⊢\mathrm{\forall }y(y=⌜\theta ⌝\leftrightarrow Diag(⌜\psi ⌝,y))$

Let us now reason about $Q$:

$Q⊢\theta \leftrightarrow \psi (⌜\psi ⌝)$
$Q⊢\theta \leftrightarrow \mathrm{\exists }y(Diag(⌜\psi ⌝,y)\wedge \varphi (y))$
$Q⊢\theta \leftrightarrow \mathrm{\exists }y(y=⌜\theta ⌝\wedge \varphi (y))$
$Q⊢\theta \leftrightarrow \varphi (⌜\theta ⌝)$

This establishes the

Diagonal Lemma
Given an $\mathcal{L}$-formula $\varphi (x)$, there is an $\mathcal{L}$-sentence $\theta$ such that

$Q⊢\theta \leftrightarrow \varphi (⌜\theta ⌝)$

8. Diagonal Lemma using a Function Term

For the Diagonal Lemma, one needs that the external syntactic operation of diagonalization on a string be represented in the theory. Under coding, the diagonalization operation corresponds to a primitive recursive function, $d:\mathbb{N}\to \mathbb{N}$, the diagonal function.

$Q$ has the property that all recursive functions are representable --- which means that for any recursive function $f:{\mathbb{N}}^k\to \mathbb{N}$, there is a formula ${\varphi }_f(x_1,\dots ,x_k,y)$ which represents it. Note that the choice of such a formula is not unique. But $Q$ is weak, and it is not always true that $Q$ proves that this formula is functional. In particular, $Q$ may not prove $\mathrm{\forall }{x}_1\dots \mathrm{\forall }{x}_k\mathrm{\exists }y{\varphi }_f(x_1,\dots ,x_k,y)$. For example, $Q$ cannot prove the totality of exponentation.

However, if one extends $Q$ with the induction scheme, then this situation changes. $PA$ is strong enough to prove the totality of any primitive recursive function. In particular, one can choose the formula $Diag(x,y)$ representing the diagonal function $d$ such that,

$PA⊢\mathrm{\forall }x\mathrm{\exists }yDiag(x,y)$

When this is so, one can introduce, by explicit definition, a new function symbol $diag(x)$ as follows:

$y=diag(x):=Diag(x,y)$

Let $P{A}^{+}$ be the result of adding this definition to $PA$. By the representablity of $d$, we have,

(*) $P{A}^{+}⊢diag(⌜\varphi ⌝)=⌜\varphi (⌜\varphi ⌝)⌝$

Returning to the Diagonal Lemma, suppose that one wishes to find the fixed-point for a given formula $\varphi$. As noted, one needs an $\mathcal{L}$-formula expressing,

the diagonalization of $x$ is $\varphi$

which one then diagonalizes to obtain $\theta$.
Above, "the diagonalization of $x$ is $\varphi$" was expressed with

$\mathrm{\exists }y(Diag(x,y)\wedge \varphi (y))$

But with a function term $diag(x)$, one can use instead

$\varphi (diag(x))$

One may then diagonalize this, to obtain a fixed point sentence $\theta$

$\theta :=\varphi (diag(⌜\varphi (diag(x))⌝))$

Note that $\theta$ has the form $\varphi (t)$, where $t$ is the term $diag(⌜\varphi (diag(x))⌝)$. To show that this works, note that we have from (*),

$P{A}^{+}⊢diag(⌜\varphi (diag(x))⌝)=⌜\varphi (diag(⌜\varphi (diag(x)⌝)⌝$

and so,

$P{A}^{+}⊢t=⌜\varphi (t)⌝$

So, $\varphi (t)$ is a self-referential sentence containing a term $t$ provably (in $PA$) denoting the code of $\varphi (t)$. And we have a modified version of the Diagonal Lemma,

Diagonal Lemma using a Term $diag(x)$
Let $P{A}^{+}$ be $PA$ extended with an explicit definition of a function term $diag(x)$. Let $\varphi (x)$ be an $\mathcal{L}$-formula. Then there is a term $t$ such that,

$P{A}^{+}⊢t=⌜\varphi (t)⌝$

9. Gödel Sentence

For an arithmetic theory $T$ to which Gödel's incompleteness theorem applies, a gödel sentence $G$ is usually defined to be a fixed-point of the formula $\mathrm{\neg }Pro{v}_T(x)$ where $Pro{v}_T(x)$ is a formula expressing "$x$ is a theorem of $T$". That is,

$Q⊢G\leftrightarrow \mathrm{\neg }Pro{v}_T(⌜G⌝)$

The construction above shows that, if we use $PA$ instead of $Q$ as our underlying syntax theory, $G$ can be expressed rather vividly as follows:

$G:=\mathrm{\neg }Pro{v}_T(diag(⌜\mathrm{\neg }Pro{v}_T(diag(x))⌝))$

So, $G$ has the form $\mathrm{\neg }Pro{v}_T(t)$, where $t$ denotes the code of $G$.