Return to Answer

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$.

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$.

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.

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$.

I think this becomes clear by stating the "Godel numbering lemma" explicitly. Writing "$Form_1$" for the (internal definition of the) set of formulas with only $x_1$ free (and possibly no free variables at all), we have:

ZFC proves "There is a function $\#: Form_1\rightarrow \mathbb{N}$ such that the relation $$Subs:=\{\langle i,j,k\rangle: i=\#(\#^{-1}(j)[x_1/\underline{k}])\}$$ is definable in $\mathbb{N}$.

(And for the incompleteness theorem we want more than that: we additionally want appropriate representability, or invariant definability, results for that numbering. But for Tarski this is all we need.)

From this we get:

ZFC proves "$\{F(\varphi): \varphi\in Sent, \mathbb{N}\models\varphi\}$ is not definable in $\mathbb{N}$."

There's no "creeping metatheory" issue here.

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.