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, $z(n)$
only involves standard or meta-theoretic definitions, and
other problems arise.
Theorem. If ZFC is consistent, then there is a model
of ZFC in which $z(n)$ is bounded by a constant function.
Proof. If ZFC is consistent, then so is $ZFC+\neg
Con(ZFC)$. Let $V$ be any model of this theory, so that
there are no models of ZFC there, and the second part of
the definition of $z$ becomes vacuous, so it reduces to its
definable-in-$V$ first part. Let $M$ be an internal
ultrapower 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 the
definable elements of $M$ all lie in the range of the
ultrapower map. If $N$ is any $V$-nonstandard element of
$M$, then every definable element of $M$ is below $N$, and
so $z(n)\lt N$ for every $n$ in $M$. QED
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)+GCH$. Let $V$ be a countable model of $ZFC+\neg
Con(ZFC)+GCH$. Since $V$ has no models of ZFC, again the
second part of your definition is vacuous, and it reduces
just to the definability-in-$V$ part. Let $M$ again be an
internal ultrapower of $V$ by an ultrafilter on $\omega$,
and 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
Best Answer
There are many flavors of "meta" in logic. Most make very minimal use of the metatheory. For example, the Montague Reflection Principle in Set Theory says the following:
This is in fact an infinite collection of theorems, one for each formula $\phi(x)$. Gödel's theorem prevents ZFC from proving all of these instances at the same time. The proof of this metatheorem is by induction on the length of $\phi(x)$. The requirements on the metatheory are very minimal, all you need is enough combinatorics to talk about formulas, proofs, and enough induction to make sense of it all. This is by far the most common flavor of "meta" in logic. There really is not much to it. Most logicians don't worry about the metatheory in this context. Indeed, it is often irrelevant and, like most mathematicians, logicians usually believe in the natural numbers with full induction.
However, sometimes there is need for a much stronger metatheory. For example, the metatheory of Model Theory is usually taken to be ZFC. Gödel's Completeness Theorem is a nice contrasting example.
Recall that a theory is consistent if one cannot derive a contradiction form it, while a theory is satisfiable if it has a model. The consistency of a theory is a purely syntactic notion. When the theory is effective, consistency can be expressed in simple arithmetical terms in a manner similar to the one discussed above. However, satisfiability is not at all of this form since the models of a theory are typically infinite structures. This is why this theorem is usually stated in ZFC. For the Completeness Theorem, one can often get by with substantially less. For example, the system WKL0 of second-order arithmetic suffices to prove the Completeness Theorem for countable theories (that exist in the metaworld in question), but such a weak metatheory would be nothing more than a major inconvenience for model theorists.
Sometimes there are multiple choices of metatheory and no consensus on which is most appropriate. This happens in the case of Forcing in Set Theory, which has three common points of view:
Forcing is a way to extend a countable transitive model of ZFC' to a larger model of ZFC' with different properties. Here ZFC' is a finite approximation to ZFC, which makes this statement non-vacuous in ZFC because of the Reflection Principle above.
Forcing is a way to talk about truth in an alternate universe of sets. Here, the alternate universe is often taken to be a Boolean-valued model, formalized within the original universe.
Forcing is an effective way to transform a contradiction some type of extensions of ZFC into contradictions within ZFC itself. Here, ZFC could be replaced by an extension of ZFC.
The last point of view, which is the least common, is essentially arithmetical since it only talks about proofs. The second point of view is well suited for hard-core platonists who believe in one true universe of sets. The first point of view, which is probably most popular, essentially takes ZFC as a metatheory much like model theorists do.
Since there is no consensus, set theorists will often talk as if both $V$ and its forcing extension $V[G]$ are absolutely real universes of sets. Although this point of view is hard to justify formally, it is possible to makes sense of it using any one of the three viewpoints above and it has the advantage that it makes it easier to express ideas that go into forcing constructions, which is what set theorists really want to talk about.
Finally, the idea of analyzing which systems prove the consistency of other systems is very common in logic. In Set Theory, these systems often take the form of large cardinal axioms. In Second-Order Arithmetic these systems often take the form of comprehension principles. In First-Order Arithmetic these systems often take the form of induction principles. Together these form an incredibly long consistency strength hierarchy stretching from extremely weak basic arithmetical facts to incredibly deep large cardinal axioms. A very significant part of logic deals with studying this hierarchy and, as Andrej Bauer commented, logicians are usually very aware of where they are sitting in this hierarchy when proving metatheorems.