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
Surprisingly, the answer is yes! Well, let me say that the answer
is yes for what I find to be a reasonable way to understand what
you've asked.
Specifically, what I claim is that if PA is consistent, then there
is a consistent theory $T$ in the language of arithmetic with the
following properties:
- The axioms of $T$ are definable in the language of arithmetic.
- PA proves, of every particular axiom of PA, that it satisfies the defining property of $T$, and so
$T$ extends PA.
- $T$ proves that the set of axioms satisfying that definition forms a consistent theory. In other words, $T$ proves that $T$ is consistent.
In this sense, the theory $T$ is a positive instance of what you
request.
But actually, a bit more is true about the theory $T$ I have in
mind, and it may lead you to think a little about what exactly you
want.
- Actually, PA proves that $T$ is consistent.
- Furthermore, the theory $T$ has exactly the same axioms as PA.
I believe that this was observed first by Feferman: S. Feferman, Arithmetization of metamathematics in a general setting, Fund. Math. 49 (1960-1961), 35--92. (Thanks to Andreas Blass for pointing out the precise reference.)
The idea of the proof is simple. We shall simply describe the
axioms of PA in a different way, rather than enumerating them in
the usual way. Specifically, let $T$ consist of the usual axioms
of PA, added one at a time, except that we add the next axiom only
so long as the resulting theory remains consistent.
Since we assumed that PA is consistent, it follows that actually
all the axioms of PA will actually satisfy the defining property
of $T$, and so PA will be contained in $T$. Furthermore, since PA
proves of any particular finite number of axioms of PA that they
are consistent, it follows that PA proves that any particular
axiom of PA will be in $T$.
Because of how we defined it, however, it is clear that PA and
hence also $T$ proves that $T$ is consistent, since if it weren't,
there would be a first stage where the inconsistency arises, and
then we wouldn't have added the axiom making it inconsistent.
Almost by definition, $T$ is consistent, and PA can prove that. So
$T$ proves that $T$, as defined by the definition we gave for it,
is consistent. So this theory $T$ actually proves its own consistency!
Meanwhile, let me point out that if one makes slightly stronger
requirements on what is wanted, then the question has a negative
answer, essentially by the usual proof of the second incompleteness theorem:
Theorem. Suppose that $T$ is a arithmetically definable
theory extending PA, such that if $\sigma$ is an axiom of $T$,
then $T$ proves that $\sigma$ is an axiom of $T$ and furthermore
PA proves these things about $T$. If $T$ is consistent, then it does not prove its own consistency.
Proof. By the Gödel fixed-point lemma, let $\psi$ be a
sentence for which PA proves $\psi\leftrightarrow\ \not\vdash_T\psi$. Thus, PA
proves that $\psi$ asserts its own non-provability in $T$.
I claim, first, that $T$ does not prove $\psi$, since if it did,
then since $T$ proves that its actual axioms are indeed axioms, it follows that $T$ would prove that that proof is indeed a proof, and so $T$ would prove that $\psi$ is provable in $T$, a statement which PA and hence $T$ proves is equivalent to $\neg\psi$, and so $T$ would also prove $\neg\psi$, contrary to
consistency. So $T$ does not prove $\psi$. And this is precisely
what $\psi$ asserts, so $\psi$ is true.
In the previous paragraph, we argued that if $T$ is consistent,
then $\psi$ is true. By formalizing that argument in
arithmetic, then since we assumed that PA proved our hypotheses on $T$, we see that PA proves that $\text{Con}(T)\to\psi$. So
if $T$ were to prove $\text{Con}(T)$, then it would prove $\psi$,
contradicting our earlier observation. So $T$ does not prove
$\text{Con}(T)$.
QED
Best Answer
Here is a conditional answer. It was shown by Macintyre and Wilkie that if (a weak variant of) Schanuel's Conjecture is true, then the first-order theory of the real exponential field $(\mathbb{R};0,1,+,\times,\exp)$ is decidable. In particular, the (very unwieldy) first-order sentence $$\bigvee_{n=A}^B \exp\exp\exp 79 = n,$$ where $A = 2^{2^{2^{79}}}$ and $B = 3^{3^{3^{79}}}$ is then decidable by finitary means. Of course, it is conceivable that Schanuel's Conjecture is false...
As pointed out by Dave Marker and George Lowther, Schanuel's Conjecture directly implies that $e^{e^{e^{79}}}$ is not an integer. Indeed, since $e^{79}$ is irrational, $79$ and $e^{79}$ are linearly independent over $\mathbb{Q}$, which means that $e^{79},e^{e^{79}}$ are algebraically independent over $\mathbb{Q}$. Since $79,e^{79},e^{e^{79}}$ are therefore linearly independent over $\mathbb{Q}$, it follows that $e^{79},e^{e^{79}},e^{e^{e^{79}}}$ are algebraically independent over $\mathbb{Q}$. In particular, $e^{e^{e^{79}}}$ is not an integer.