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.