Let $F$ be a first order logic theory with a set of axioms that are primitively recursive and are supposed to capture arithmetic (in particular, we can define a Gödel number. Let $\mathbb N$ be the standard model for the natural numbers. Tarski proves that it is impossible to find a statement with one free variable $T(x)$ in the language such that for every natural number $n$, $T(n)$ holds if and only if $n$ is the Gödel number of a true statement (in $\mathbb N$).

One possible proof goes through a "diagonal lemma" like so:

Diagonal Lemma: For any statement with one free variable $A(x)$, there exists a natural number $n$ such that the Gödel number of the sentence $A(n)$ is $n$ itself.

Proof: As part of the Gödel numbering, there is a function $sub(x,y)$ that does the following: If $m$ is the Gödel number of a statemnt $\phi(x)$, then $sub(m,n)$ is the Gödel number of the statement $\phi(n)$.

Then, consider the formula $C(x) = A(sub(x,x))$. Let the Gödel number of this be $c$ and consider $B = A(sub(c,c))$. Then, I claim that the Gödel number of $B$ is equal to $sub(c,c)$. Indeed, $sub(c,c)$ is by definition the Gödel number of $C(c) = A(sub(c,c)) = B$. Therefore, we can take $n = sub(c,c) = A(n)$.

Question: The above proof is of course extremely simple but also to me, extremely mysterious. Why would anyone want to consider $C(x)$ in the first place?

My first attempt was to treat the Diagonal Lemma as saying that the function $n$ to Gödel number of $A(n)$ has a fixed point in $\mathbb N$. The naive way to proceed might be try some sort of iteration of this function or some modification of this. Can the diagonal lemma be seen as a sophisticated way of making this naive idea work?

Question 2: This is really a bonus question, feel free to ignore everything after this point. I find that I can prove Tarski's theorem directly in the following way:

Let us enumerate in a computable way all the statements with one free variable by $A_n(x)$. Suppose there was a statement $T(x)$ representing truth in the language. Then we can define $B(n) = \neg T(A_n(n))$. That is, $B(n)$ "says" that the statement $A_n(n)$ is false. However, since our enumeration was computable, $B(x)$ is itself a statement and occurs among the $A_n(x)$ at say $n = n_0$. However, then $B(n_0)$ effectively says "This statement is false" and immediately leads to a contradiction.

First: Is the above proof correct? Second: Can this approach be adapted to prove the diagonal lemma itself? Perhaps by enumerating all formulas with two variables or something clever along these lines?

Let $F$ be a first order logic theory with a set of axioms that are primitively recursive and are supposed to capture arithmetic (in particular, we can define a Gödel number. Let $\mathbb N$ be the standard model for the natural numbers. Tarski proves that it is impossible to find a statement with one free variable $T(x)$ in the language such that for every natural number $n$, $T(n)$ holds if and only if $n$ is the Gödel number of a true statement (in $\mathbb N$).

One possible proof goes through a "diagonal lemma" like so:

(The following is edited in response to the (valid) criticism below.)

Diagonal Lemma: For any statement with one free variable $A(x)$, there exists a term $t$ such that the Gödel number of the sentence $A(t)$ is $n$ and $t$ evaluates to $n$ in the standard model.

Proof: As part of the Gödel numbering, there is a function $sub(x,y)$ that does the following: If $m$ is the Gödel number of a statemnt $\phi(x)$, then $sub(m,n)$ is term that in the standard model corresponds to the Gödel number of the statement $\phi(n)$.

Then, consider the formula $C(x) = A(sub(x,x))$. Let the Gödel number of this be $c$ and consider $B = A(sub(\overline c,\overline c))$ where $\overline c$ is a term that evaluates to $c$. Then, I claim that the Gödel number of $B$ is equal to $sub(c,c)$. Indeed, $sub(\overline c,\overline c)$ is by definition a term corresponding to the the Gödel number of $C(\overline c) = A(sub(\overline c,\overline c)) = B$. This completes the proof.

Question: The above proof is of course extremely simple but also to me, extremely mysterious. Why would anyone want to consider $C(x)$ in the first place?

My first attempt was to treat the Diagonal Lemma as saying that the function $n$ to Gödel number of $A(n)$ has a fixed point in $\mathbb N$. The naive way to proceed might be try some sort of iteration of this function or some modification of this. Can the diagonal lemma be seen as a sophisticated way of making this naive idea work?

Question 2: This is really a bonus question, feel free to ignore everything after this point. I find that I can prove Tarski's theorem directly in the following way:

Let us enumerate in a computable way all the statements with one free variable by $A_n(x)$. Suppose there was a statement $T(x)$ representing truth in the language. Then we can define $B(n) = \neg T(A_n(n))$. That is, $B(n)$ "says" that the statement $A_n(n)$ is false. However, since our enumeration was computable, $B(x)$ is itself a statement and occurs among the $A_n(x)$ at say $n = n_0$. However, then $B(n_0)$ effectively says "This statement is false" and immediately leads to a contradiction.

First: Is the above proof correct? Second: Can this approach be adapted to prove the diagonal lemma itself? Perhaps by enumerating all formulas with two variables or something clever along these lines?