Diagonal Lemma

From ProofWiki
Jump to: navigation, search

Theorem

Let $T$ be the set of theorems of some theory in the language of arithmetic which contains minimal arithmetic.


For any formula $B(y)$ in the language of arithmetic, there is a sentence $G$ such that

$T\vdash G\leftrightarrow B(\hat G)$

where $\hat G$ is the Gödel number of $G$ (more accurately, it is the term in the language of arithmetic obtained by applying the function symbol $s$ to $0$ this many times).


Proof

There is a primitive recursive function $\mathrm{diag}$ which is defined by

$\mathrm{diag}(n) = \widehat{A(\hat A)}$ where $A(x)$ is the formula such that $\hat A = n$

where, again, the $\hat{ }$ sign denotes the Gödel number of the contained formula (and we are not being formal about distinguishing between integers and symbols in the language).

Informally, $\mathrm{diag}$ takes a Gödel number, decodes it to a formula, plugs in the Gödel number for that formula in place of a free variable, and encodes this new formula back to a new Gödel number.


Since $T$ contains $Q$, by Recursive Sets are Definable in Arithmetic applied to the graph of $\mathrm{diag}$, we have that there is some formula $\mathrm{Diag}(x,y)$ which defines the graph of $\mathrm{diag}$ in $T$.

That is:

$\mathrm{diag}(n) = m$ if and only if $T\vdash \mathrm{Diag}(n,m)$


Let $A(x)$ be the formula $\exists y (\mathrm{Diag}(x, y) \wedge B(y))$.

Let $G$ be $A(\hat A)$.


We then have $T \vdash \mathrm{Diag}(\hat A, \hat G)$, by checking the definitions.


Let $T' = T\cup \{G\}$.

Then $T'\vdash A(\hat A)$.
Hence $T'\vdash \exists y (\mathrm{Diag}(\hat A , y) \wedge B(y))$.
But since $\hat G$ is the only number such that $T\vdash \mathrm{Diag}(\hat A, \hat G)$, this gives us
$T'\vdash B(\hat G)$

Thus, $T\vdash G \rightarrow B(\hat G)$.


Let $T' = T\cup \{B(\hat G)\}$.

Again, we have $T\vdash \mathrm{Diag}(\hat A, \hat G)$, so this gives us
$T'\vdash \mathrm{Diag}(\hat A, \hat G) \wedge B(\hat G)$, and hence
$T'\vdash \exists y (\mathrm{Diag}(\hat A, y) \wedge B(y))$
But this is the same thing as
$T'\vdash G$

Thus, $T\vdash B(\hat G) \rightarrow G$.


Thus $G$ is as claimed.


$\blacksquare$



Sources