Intuition behind the diagonal lemma while proving Tarski's theorem about truth [duplicate]

Question

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?

Answer 1

You’re being a bit sloppy throughout about the distinction between numbers and terms of the language of $F$. This is important because two terms $t_1$, $t_2$ can be provably equal in $F$ (i.e. equal as the numbers they denote), while being syntactically different, and hence having different Gödel numbers — e.g. the terms “2+2” and “4”.

In particular, in your statement of the diagonal lemma, you refer to “the Gödel number of the formula $A(n)$”. This isn’t quite well-defined, since the thing being substituted into $A$ should be a term, not a number.

The first fix one might think of would be to replace “$A(n)$” by “$A(\bar{n})$” (where $\bar{n}$ denotes the standard numeral for $n$). However, your proof doesn’t give this — and indeed, as Emil Jeřábek points out in comments, this version is false for the standard ways of setting up Gödel numbering. Specifically, at the last step of the proof, you’ve proven in $F$ that $n = sub(c,c)$, and that this is the Gödel number of the formula $A(sub(c,c))$. However, that formula is not syntactically the same as the formula $A(\bar{n})$.

If you go through the proof being more careful about this distinction, you’ll find you’ve proved:

Lemma For any formula $A(x)$ with one free variable, there’s a term $t$ such that $F$ proves that $t$ is equal to the Gödel number of the sentence $A(t)$.

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?

I don’t have a terribly satisfactory answer to this, but a partial one: the form of $C$ is not so surprising if you’re acquainted with the Y combinator and similar phoenomena in the λ-calculus. On the other hand, these themselves may seem equally mysterious; see “Can someone explain the Y combinator?” for attempts (again not entirely satisfactory, I think) to motivate how one might come up with it. Also, I doubt this motivation is historically correct, though I’m not sure — see “What is the history of the Y combinator?” for some relevant dates.