I am studying from Boolos' Computability & Logic (3rd edition). I need help unpacking what the Diagonal Lemma states, and understanding its proof. The Diagonal lemma is formalized on page 105 from these notes, it appears as lemma 2.
Diagonal Lemma states:
Let $T$ be a theory in which $\operatorname{diag}$ is representable. Then for any formula $B(y)$ (in the language of $T$, containing just the variable $y$ free), there is a sentence $G$ such that $\vdash_T G\leftrightarrow B(\ulcorner G\urcorner)$.
The terms utilized in this lemma are defined on the previous pages. I need help unpacking what this lemma states. What does $B(\ulcorner G\urcorner)$ mean? I know $\ulcorner G\urcorner$ is defined to be the Gödel number of a sentence $G$. I do not understand what $B(\ulcorner G\urcorner)$ means though.
Also, within the proof it states
Since $A(x,y)$ represents $\operatorname{diag}$ in $T$, one can think of it as meaning, informally, that “$y$ is the (g.n. of the) diagonalization of (the formula whose g.n. is) $x$”.
Does that mean that there is diagonalization of a formula, and the diag (Gödel number of the diagonalization) is represented as $x$ & that the $y$ is the diag (Gödel number) of $x$?
That doesn't make any sense to me, since I don't understand how a Gödel number which is some sequence of numbers that represents a formula, could also have a Gödel number. Since the original Gödel number is just a string of numbers.
Please help me unpack what Lemma 2 states (especially what $B(\ulcorner G\urcorner)$ means) and what $A(x,y)$ means.
Best Answer
I won't attempt to explain the exact wording of the proof in your link, but I will explain the proof using the same notation. I think you can go back to the link afterwards and make sense of it.
The Diagonal Lemma says: Let $T$ be a theory in which we can represent the process of diagonalization. Then every formula $B(y)$ in the language of $T$ "detects truth" for some sentence $G$. In other words,
$$T \vdash G \leftrightarrow B(\ulcorner G \urcorner)$$
So that $T$ proves $G$ is true if and only if $B$ holds for the Gödel number of $G$.
Proof: We first build a new formula $F$. This formula takes a value $x$, plugs $x$ into the $x$th formula, and then takes the Gödel number of that sentence and sticks it into $B$. In other words,
$$F = \exists y \Big(A(x,y) ~~ \& ~~ B(y)\Big)$$
As we have defined it, $F$ is a function of $x$. Let $n$ be its Gödel number. Now, we plug $n$ into $F$, to obtain a sentence $G = F(n)$. In essence, we obtain $G$ by giving the Gödel number of $F$ as input to itself.
We now claim that this $G$ is the sentence we have been searching for. Let $k$ be the Gödel number for $G$. We want to show that
$$T \vdash G \leftrightarrow B(\ulcorner G \urcorner) (= B(k))$$
Now, $T \vdash G$ iff $T \vdash F(n)$. But $T \vdash F(n)$ iff $T$ proves that $B$ holds for the Gödel number of the sentence given when plugging $n$ into the $n$th function. However, recall that the Gödel number of the sentence given when plugging $n$ into the $n$th function is just $\ulcorner F(n) \urcorner = \ulcorner G \urcorner = k$. Thus, $T \vdash F(n)$ iff $T \vdash B(k)$, and the proof is complete.