Reading through the proof of the diagonal lemma related to Gödel incompleteness theorem on wikipedia, I feel its a little bit complex. As far as this lemma relates to proving Gödel incompleteness theorem-I, I see the following being simpler:
Lemma: if $T$ is a first order theory capable of representing all computable functions, and $\mathcal F(x)$ is a formula in $T$ with one free variable, then there is a sentence $\mathcal C$ such that: $$ \vdash_T \mathcal C \iff \mathcal F(\ulcorner \mathcal C\urcorner)$$
We'll take $T$ to be $\sf PA$.
Initial thoughts about the above lemma is that the only obstacle to it is if there is an arithmetical formula $\mathcal F(x)$ that opposes truth at all naturals, that is whatever natural $n$ such that $\mathcal F(n)$ and $n=\ulcorner \mathcal C \urcorner$ then $\neg \mathcal C$, and whatever $n$ such that $\neg \mathcal F(n)$ and $n=\ulcorner \mathcal C \urcorner$ then $\mathcal C$. In simple English: $\mathcal F$ holds of all Gödel numbers of false sentences, and $\neg \mathcal F$ holds of all Gödel numbers of true sentences. Now if there can exist such a truth opposing formula $\mathcal F(x)$, then it can be shown that this opposes Tarski's undefinability theorem, as follows:
Lets define an extractor function $ \zeta $ that sends $\ulcorner\mathcal A (\ulcorner \mathcal A(x) \urcorner)\urcorner$ to $\ulcorner \mathcal A(x) \urcorner $, I view this function as extracting the latter from the former. Along this setting $\ulcorner \mathcal A(x) \urcorner$ to be called the extractee of $\ulcorner\mathcal A (\ulcorner \mathcal A(x) \urcorner)\urcorner$. This is computable and so definable in the language of arithmetic (i.e. arithmetical)
Now since $\mathcal F(x)$ is arithmetical, then we can define a new arithmetical formula $\mathcal F'(x)$ such that:
$\textbf{Define: } \mathcal F'(x) \iff \mathcal F(x) \lor \exists y: \mathcal F(y) \land x=\zeta (y)$
In English: $\mathcal F'(x)$ holds of all Gödel numbers of false sentences and the extractees of those numbers and $\neg \mathcal F'(x)$ holds of all Gödel numbers of true sentences and the extractees of those numbers.
Now, the question about whether $\mathcal F'(\ulcorner \mathcal F'(x) \urcorner)$ or $\neg \mathcal F'(\ulcorner \mathcal F'(x) \urcorner)$ is true, is paradoxical!
So $\mathcal F(x)$ cannot exist. Which proves the lemma.
I see this proof to be very simple, virtually just a two step proof, as compared to multi-step proof present in the Wikipedia.
First, is this proof correct?
Can this proof be carried out under all the grounds the proof in the wikipedia are carried under?
My point is that if this proof is correct, then being so simple might mean that it is restricted in some sense, hence the question?
Best Answer
I think this proof requires to add the assumption that "$T$ is complete". So, it suites to prove the diagonal lemma in the context of proving the first of Gödel incompleteness theorems by reductio ad absurdum!
Now, truth opposition by a $T$-formula $\mathcal F(x)$ is expressible as a schema "$\textbf{Sch} $" in the language of $T$. This is:
$\textbf{Sch: } $ if $\mathcal C_0, \mathcal C_1, \mathcal C_2,..$ are all of the sentences in the language of $T$, then: $$ \vdash_{T} \forall n: n=\ulcorner \mathcal C_i \urcorner \to [\mathcal F(n) \leftrightarrow \neg \mathcal C_i]$$
. Now from the main posting it is proved that $\textbf{Sch} $ for any $T$-formula $\mathcal F(x)$ would be inconsistent. Since we assumed $T$ to be complete, then there should be a sentence $\mathcal C_i$ that fulfills the negation of an instance of the above scheme, i.e. we have $$\vdash_{T} \exists n: n=\ulcorner \mathcal C_i \urcorner \land \neg [\mathcal F(n) \leftrightarrow \neg \mathcal C_i]$$, and thus proving the Lemma. Otherwise $T$ (being complete) would prove all instances of $\textbf{Sch} $, and so be inconsistent.
I don't know if the proof can work under weaker assumptions.