User:IssaRice/Computability and logic/Diagonalization lemma (Yanofsky method)

This page is just a rewritten version of the proof of the diagonalization lemma from Yanofsky's paper. There are some parts I found difficult to understand/gaps that I thought should be filled, so this version will hopefully be much more complete.

Theorem (Diagonalization lemma). Let $T$ be some nice theory (I don't remember the exact conditions, but Peano Arithmetic or Robinson Arithmetic would work). For any single-place formula $\mathcal{E}(x)$ with $x$ as its only free variable, there exists a sentence (closed formula) $\mathcal{C}$ such that $T⊢\mathcal{C}\leftrightarrow \mathcal{E}(⌜\mathcal{C}⌝)$.

Proof. We will use what's called the wikipedia:Lindenbaum–Tarski algebra in our proof, which the Yanofsky paper just calls Lindenbaum classes. The idea is to define an equivalence an equivalence relation on formulas, so that $A\sim B$ iff our theory $T$ can prove that $A$ and $B$ are logically equivalent. In other words, we define $A\sim B$ iff $T⊢A\leftrightarrow B$. This is easily verified to be an equivalence relation. One twist is that it doesn't make sense to compare two formulas with differing arity. For instance, what does it even mean to say "2+2=5" and "x+5=7" are or are not provably equivalent? For this reason, we make a separate equivalence relation for each arity, and so we end up with separate quotients for each arity. For $i=0,1,2,\dots$, we let ${\mathit{L}\mathit{i}\mathit{n}\mathit{d}}^i$ be the set of Lindenbaum classes of formulas with $i$ free variables.

That means that e.g. each element of ${\mathit{L}\mathit{i}\mathit{n}\mathit{d}}^0$ is not a sentence, but rather a set of sentences that are all provably equivalent. But every sentence is either true or false, so doesn't this mean ${\mathit{L}\mathit{i}\mathit{n}\mathit{d}}^0$ has just two element, $[\mathrm{\top }{]}_{\sim }$ and $[\mathrm{\perp }{]}_{\sim }$ (i.e. the class of true sentences and the class of false sentences)? No! That's because even if two sentences are both true, our theory may be unable to prove that it is so! That's the whole point of Gödel's first incompleteness theorem, which shows us that there can be true sentences (such as the famous "I am not provable" sentence $G$) which are not provable (so that even though $G$ is true, $G\notin [2+2=5{]}_{\sim }$).

In the paper, Yanofsky toggles fluidly between thinking of a formula like $\mathcal{B}(x)$ as a formula vs a set of formulas whose representative is $\mathcal{B}(x)$ (i.e. the class $[\mathcal{B}(x){]}_{\sim }$).

Acknowledgments: Thanks to Rupert McCallum for helping me work through the proof.

See also

• User:IssaRice/Computability_and_logic/Diagonalization_lemma