Skip to main content
1 of 4
Noah Schweber
  • 21.1k
  • 10
  • 110
  • 331

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.

Noah Schweber
  • 21.1k
  • 10
  • 110
  • 331