Tarski's truth theorem — semantic or syntactic?

If I recall correctly, Jech is using as his metatheory the class theory $\mathsf{NBG}$. In this context, "true" is a proxy for "true in the (class-sized) structure $V$."

Specifically, the (more) formal version of the natural-language Theorem $12.7$ is the following:

$Th(V)$ is not definable in $V$.

The definition of $Th(V)$ is taking place on the class level: it's a set of natural numbers defined by quantifying over classes. The same is true for the property "definable in $V$." So even though it looks like Jech is using a weirdly un-referring notion of "truth," it is in fact just the usual notion of truth with respect to a specific structure - that structure being $V$, and that whole facet of the argument being (annoyingly, perhaps) kept implicit. Note that this makes the whole "correctness-about-$\omega$" issue moot: Theorem $12.7$ is about a structure which by definition has the right $\omega$.


An in-my-opinion more satisfying version of the result, which makes correctness-about-$\omega$ nontrivial, is the following:

$T$ proves that for all $\mathcal{M}\models\mathsf{ZFC}$, $Th(\mathcal{M})$ is not the standard part of a definable subset of $\mathcal{M}$.

Here $T$ is a very weak theory indeed: $\mathsf{ACA_0^+}$ suffices (really the only need for strength being the requirement that the theory of a structure is actually a thing that makes sense in the first place - see e.g. here). Note that this version of the result does not apply only to models which are correct about $\omega$.


EDIT: And as Monroe Eskew pointed out below, if we drop models entirely we can go even lower. We can prove over a very weak base theory (e.g. $I\Sigma_1$ is already overkill) the following:

If $\mathsf{ZFC}$ is consistent, then there is no formula $\varphi$ such that for all sentences $\psi$ $\mathsf{ZFC}$ proves $\varphi(\#\psi)\leftrightarrow\psi$.


Tarski's theorem, as given in Undecidable theories, page 46, allows arbitrary numbering and is completely syntactic. I think this abstract version given by Tarski himself is the most clear. Let me summarize it here with some inessential variations.

Let $T$ be a consistent first-order theory (any consistent first-order theory). If $\varphi\mapsto \ulcorner\varphi\urcorner$ is a naming of formulas (any assignment of closed terms to formulas), then either the diagonalization function (the function $\varphi\mapsto \varphi(\ulcorner\varphi\urcorner)$) is not representable (under that naming), or the set of theorems is not representable (under the given naming), or both are not representable.

In the case of ZF, assuming it to be consistent, we know that if we choose a recursive naming, we can represent the diagonalization function but not the set of theorems. Also, we can easily choose a (nonrecursive) naming which allows us to represent the set of theorems, but, then, the diagonalization will not be representable.

The proof is quite simple. If the diagonalization is representable, the fixed-point lemma can be proved quite simply. Assume that $V$ is a formula representing the set of theorems. Apply the fixed point lemma to get $\varphi$, a sentence satisfying $T\vdash\varphi\leftrightarrow \neg V(\ulcorner\varphi\urcorner)$.

If $T\vdash\varphi$, then, since $V$ represents the theorems, $T\vdash V(\ulcorner\varphi\urcorner)$, and $T$ is inconsistent. If $T\nvdash \varphi$, then, since $V$ represents the theorems, $T\vdash\neg V(\ulcorner\varphi\urcorner)$, and $T\vdash \varphi$ by the choice of $\varphi$. Therefore, $T\vdash \varphi$ and it is inconsistent by the previous argument.

EDIT

Motivated by the question in the comment, I will prove the fixed point lemma I have used above:

We are assuming that $T$ is a first-order theory and that the diagonalization is represented in $T$ under the arbitrary naming $\varphi\mapsto\ulcorner\varphi\urcorner$. It means that there is a formula $D(x,y)$ such that $T\vdash\forall y(D(\ulcorner\phi\urcorner, y)\leftrightarrow y=\ulcorner\phi(\ulcorner\phi\urcorner)\urcorner)$.

Now, let $W(y)$ be an arbitrary formula. Let $\phi(x)$ be the formula $\exists y(D(x,y)\wedge W(y))$ and let $\varphi$ be the sentence $\phi(\ulcorner\phi\urcorner)$, the diagonalization of $\phi$. This sentence is a fixed point for $W(y)$.

Indeed, $\varphi$ is $\exists y(D(\ulcorner\phi\urcorner,y)\wedge W(y))$, which, from the hypothesis on the representation of the diagonalization, is equivalent to $\exists y(y=\ulcorner\varphi\urcorner\wedge W(y))$. The last sentence is logically equivalent to $W(\ulcorner\varphi\urcorner)$, and we are done.

Therefore, Tarski's result applies to arbitrary first-order theories and to arbitrary namings. The moral is that no matter what first-order theory and naming of formulas you choose, the representation of at least one of two simple metatheoretical notions (diagonalization and theoremhood) within the object theory will always fail.