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 $E (x)$ with $x$ as its only free variable, there exists a sentence (closed formula) $C$ such that Failed to parse (unknown function "\ndash"): {\displaystyle T \ndash \mathcal C \leftrightarrow \mathcal E(\ulcorner \mathcal C \urcorner)}

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

See also