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
Martin Gardner's Annotated Alice: The Definitive Edition says only this:
Needless to say, all the Mock Turtle's subjects are puns (reading, writing, addition, subtraction, multiplication, division, history, geography, drawing, sketching, painting in oils, Latin, Greek). In fact, this chapter and the one to follow fairly swarm with puns. Children find puns very funny, but most contemporary authorities on what children are supposed to like believe that puns lower the literary quality of juvenile books.
Gardner then goes on to say that the "Drawling-master" is a reference to the art critic John Ruskin, and gives a couple of paragraphs of biographical information about Ruskin. Given Gardner's extensive knowledge of Carrolliana, it seems likely that Carroll never published any further comments about the "different branches of Arithmetic."
Best Answer
This question reminds me of a magical little-known theorem of Jean Pierre Ressayre that shows that every nonstandard model of $PA$ has a model of $ZF$ as a submodel of its Ackermann intepretation, more specifically:
Theorem. [Ressayre] Suppose $(M, +, \cdot)$ is a nonstandard model of $PA$, and $\in_{Ack}$ is the Ackermann epsilon on $M$, i.e., $a\in_{Ack}b$ iff $\mathcal{M}$ satisfies "the $a$-th digit in the binary expansion of $b$ is 1". Then for every consistent recursive extension $T$ of $ZF$ there is a subset $A$ of $M$ such that $(A,\in_{Ack})$ is a model of $T$.
Proof Outline: By Löwenheim-Skolem, it suffices to consider the case when $M$ is countable. Choose a nonstandard integer $k$ in $M$, and consider the submodel $M_k$ of $(M,\in_{Ack})$ consisting of sets of ordinal rank less than $k$ [as computed within $(M,\in_{Ack})$]. "Usual arguments" show that $(M,\in_{Ack})$ has a Tarskian truth-definition for $M_k$, which in turn implies that $(M_k,\in_{Ack})$ is recursively saturated. Since $M_k$ is also countable, $(M_k,\in_{Ack})$ must be resplendent [which means that it has an expansion to every recursive $\Sigma^1_1$ theory that its elementary diagram is consistent with].
Now add a new unary predicate symbol $A$ to the language ${\in}$ of set theory and consider the (recursive) theory $T^A$ consisting of sentences of the form $\phi^A$, where $\phi \in T$, and $\phi^A$ is obtained by relativizing every quantifier of $\phi$ to $A$. It is not hard to show that $T^A$ is consistent with the the elementary diagram of $(M_k,\in_{Ack})$, so by replendence the desired $A$ can be produced.
[I will be glad to add clarifications]
Ressayre's theorem appears in the following paper:
J. P. Ressayre, Introduction aux modèles récursivement saturés, Séminaire Général de Logique 1983–1984 (Paris, 1983–1984), 53–72, Publ. Math. Univ. Paris VII, 27, Univ. Paris VII, Paris, 1986.