A question on the diagonal lemma

Question

I have a quick question on the diagonal lemma that for any formula $\phi(x)$ with only one free variable $x$, there is a formula $G$ such that $\vdash_T G \leftrightarrow \phi (\ulcorner G \urcorner)$, where $T$ is a theory for diagnoalization. I'm wondering if $G$ can occur in $\phi$. For instance, let $\psi(\ulcorner\chi \urcorner)$ be $\chi \wedge Prov( \ulcorner \chi \urcorner)$. Can we take $\psi$ as $\phi$ so we can get the result that there is a formula $G$ such that $\vdash_T G \leftrightarrow (G \wedge Prov( \ulcorner G \urcorner)$?

My rough guess is we can't, because it derives a contradiction too easily: If I take $\phi(\ulcorner \alpha\urcorner)$ as $\neg\alpha \wedge \ulcorner \alpha\urcorner=\ulcorner \alpha\urcorner$ and the diagonal lemma works for $\phi$, then there should be $G$ such that $G\leftrightarrow (\neg G \wedge \ulcorner G\urcorner=\ulcorner G\urcorner)$. Since $x=x$ is a logical truth, either of assuming $G$ and $\neg G$ yields each other, so $T$ is inconsistent.

Then I'm wondering which conditions prevent this abusing because this way doesn't make more variables other than the initial $x$ (for instance, I may rewrite it as $\vdash_T G \leftrightarrow ((G \wedge \ulcorner G \urcorner=\ulcorner G \urcorner) \wedge \ulcorner G \urcorner=\ulcorner G \urcorner$) and it doesn't change anything).

Let me know if I have any confusions here and thanks in advance!

Answer 1

The formula $\phi(x)$ to which we are going to apply the diagonalization lemma needs to have, as you say, one free variable.

But if $\chi \land Prov(\ulcorner\chi\urcorner)$ has a free variable at all it has to be in $\chi$ since $Prov(\ulcorner\chi\urcorner)$ is a closed wff, even if $\chi$ isn't ($\ulcorner\chi\urcorner$ is a numeral in every case).

So you really need to write your $\psi$ as something like $\chi(x) \land Prov(\ulcorner\chi(x)\urcorner)$. And you can apply the lemma to that, but we get something quite different from what you wrote, i.e. there is $G$ such that $$\vdash G \equiv (\chi(\ulcorner G\urcorner) \land Prov(\ulcorner\chi(x)\urcorner)$$

Which is quite unproblematic.