the model (as via second-order logic). In this case, $z(n)$only involves standard or meta-theoretic definitions, andof ZFC in which $z(n)$ is bounded by a constant function.

Proof. If ZFC is consistent, then so is $ZFC+\negCon(ZFC)$. Let $V$ be any model of this theory, so thatthere are no models of ZFC there, and the second part ofthe definition of $z$ becomes vacuous, so it reduces to itsdefinable-in-$V$ first part. Let $M$ be an internalultrapower of $V$ by an ultrafilter on $\omega$. Thus, $M$is nonstandard relative to $V$. But the function $z$,defined externally, uses only standard definitions, and thedefinable elements of $M$ all lie in the range of theultrapower map. If $N$ is any $V$-nonstandard element of$M$, then every definable element of $M$ is below $N$, andso $z(n)\lt N$ for every $n$ in $M$. QED

Theorem. If ZFC is consistent, then there is a modelof ZFC in which $f(n)\lt z(10000)$ for every natural numberCon(ZFC)$Con(ZFC)+GCH$. Let $V$ be a countable model of $ZFC+\negCon(ZFC)+GCH$. Since $V$ has no models of ZFC, again thejust to the definability-in-$V$ part. Let $M$ again be anso that $M$ is anonstandard version of $V$, with nonstandard naturalnumbers. Let and let $N$ be a $V$-nonstandard natural number of $M$.

1

I think your question is not as precise as you portray it.

First, let me point out that you have not actually defined a function $z$, in the sense of giving a first order definition of it in set theory, and you provably cannot do so, because of Tarski's theorem on the non-definability of truth. We simply have no way to express the relation x is definable in the usual first-order language of set theory. More specifically:

Theorem. If ZFC is consistent, then there are models of ZFC in which the collection of definable natural numbers is not a set or even a class.

Proof. If V is a model of ZFC, then let $M$ be an internal ultrapower of $V$ by a nonprincipal ultrafilter on $\omega$. Thus, the natural numbers of $M$ are nonstandard relative to $V$. The definable elements of $M$ are all contained within the range of the ultrapower map, which in the natural numbers is a bounded part of the natural numbers of $M$. Thus, $M$ cannot have this collection of objects as a set or class, since it would reveal to $M$ that its natural numbers are ill-founded, contradicting that $M$ satisfies ZFC. QED

In such a model, your definition of $z$ is not first order. It could make sense to treat your function $z$, however, in a model as an externally defined function, defined outside the model (as via second-order logic). In this case, other problems arise.

Theorem. If ZFC is consistent, then there is a model of ZFC in which $f(n)\lt z(10000)$ for every natural number n in the meta-theory.

Proof. If ZFC is consistent, then so is $ZFC+\neg Con(ZFC)$. Let $V$ be a countable model of $ZFC+\neg Con(ZFC)+GCH$. Since $V$ has no models of ZFC, the second part of your definition is vacuous, and it reduces just to the definability-in-$V$ part. Let $M$ be an internal ultrapower of $V$ by an ultrafilter on $\omega$, so that $M$ is a nonstandard version of $V$, with nonstandard natural numbers. Let $N$ be a $V$-nonstandard natural number of $M$. Every definable element of $M$ is in the range of the ultrapower map, and therefore below $N$. In particular, for every meta-theoretic natural number $n$, we have $f(n)\lt N$ in $M$, since $f(n)$ is definable. Now, let $M[G]$ be a forcing extension in which the continuum has size $\aleph_N^M$. Thus, $N$ is definable in $M[G]$ by a relatively short formula; let's say 10000 symbols (but I didn't count). Since the forcing does not affect the existence of ZFC models or Turing computations between $M$ and $M[G]$, it follows that $f(n)\lt z(10000)$ in $M[G]$ for any natural number of $V$. QED

Theorem. If ZFC is consistent, then there is a model of ZFC with a natural number constant $c$ in which $z(n)\lt f(c)$ for all meta-theoretic natural numbers $n$.

Proof. Use the model $M$ (or $M[G]$) as above. This time, let $c$ be any $V$-nonstandard natural number of $M$. Since the definable elements of $M$ all lie in the range of the ultrapower map, it follows that every z(n), for meta-theoretic $n$, is included in the $V$-standard elements of $M$, which are all less than $c$. But $M$ easily has $c\leq f(c)$, and so $z(n)\lt f(c)$ for all these $n$. QED