show/hide this revision's text 5 not --> not so much

So thanks -- I didn't want to prejudice things, but this is actually the answer I was hoping for! If it wasn't clear already, I'm interested in big numbers not so much for their own sake, but as a concrete way of comparing the expressive power of different notational systems. And I have a strong intuition that Turing machines are a "maximally expressive" notational system, at least for those numbers that meet my criterion of being "ultimately defined in terms of finite processes" (so in particular, independent of the truth or falsehood of statements like CH). If one could use ZFC to define integer sequences that blew my sequence f(n) out of the water (and that did so in a model-independent way), that would be a serious challenge to my intuition.

show/hide this revision's text 4 Fixed typo

Update :(8/5): After reading the first few comments, it occurred to me that the motivation for this question might not make sense to you, if you don't recognize a distinction between those mathematical questions that are "ultimately about finite processes" (for example: whether a given Turing machine halts or doesn't halt; the values of the super-recursive Busy Beaver numbers; most other mathematical questions), and those that aren't (for example: CH, AC, the existence of large cardinals). The former I regard as having a definite answer, independently of the answer's provability in any formal system such as ZFC. (If you doubt that there's a fact of the matter about whether a given Turing machine halts or runs forever, then you might as well also doubt that there's a fact of the matter about whether a given statement is or isn't provable in ZFC!) For questions like CH and AC, by contrast, one can debate whether it even means anything to discuss their truth independently of their provability in some formal system.

Yes, it's possible that my question could degenerate into philosophical disagreements. But a priori, it's also possible that someone can give a sequence that everyone agrees is "definable in terms of finite processes," and that blows my f(n) and z(n) out of the water. The latter would constitute a completely satisfying answer to the question.

Update (8/6): It's now been demonstrated to my satisfaction that z (as I defined it) is blown out of the water by f. The reason is that z is defined by quantifying over all models of ZFC. But by the Completeness Theorem, this means that z can also be defined "syntactically," in terms of provability in ZFC. In particular, we can compute z using an oracle for the $BB_1$ function (or possibly even the BB function?), by defining a Turing machine that enumerates all positive integers m as well as all ZFC-proofs that the predicate $\phi$ picks out m.

So thanks -- I didn't want to prejudice things, but this is actually the answer I was hoping for! If it wasn't clear already, I'm interested in big numbers not for their own sake, but as a concrete way of comparing the expressive power of different notational systems. And I have a strong intuition that Turing machines are a "maximally expressive" notational system, at least for those numbers that meet my criterion of being "ultimately defined in terms of finite processes" (so in particular, independent of the truth or falsehood of statements like CH). If one could use ZFC to define integer sequences that blew my sequence f(n) out of the water (and that did so in a model-independent way), that would be a serious challenge to my intuition.

So let me refocus the question: is my intuition correct, or is there some more clever way to use ZFC to define an integer sequence that blows f(n) out of the water?

Actually, a proposal for using ZFC to at least match the growth rate of f now occurs to me. Recall that we defined the sequence z by maximizing over all models M of ZFC. However, this definition ran into problems, related to the "self-hating models" that contain nonstandard integers encoding proofs of Not(Con(ZFC)). So instead, given a model M of ZFC and a positive integer k, let's call M "k-true" if every $\Pi_k$ arithmetical sentence S is true in M if and only if S is semantically true (i.e., true for the standard integers). (Here a $\Pi_k$ arithmetical sentence means a sentence with k alternating quantifiers, all of which range only over integers.)

Now, let's define the function

$z_k(n)$

exactly the same way as z(n), except that now we only take the maximum over those models M of ZFC that are k-true.

This remains to be proved, but my guess is that $z_k(n)$ should grow more-or-less like $BB_{k+c}(n)$, for some constant c. Then, to get faster-growing sequences, one could strengthen the k-truth requirement, to require the models of ZFC being maximized over to agree with what's semantically true, even for sentences about integers that are defined using various computable ordinals. But by these sorts of devices, it seems clear that one can match f but not blow it out of the water---and indeed, it seems simpler just to forget ZFC and talk directly about Turing machines.

show/hide this revision's text 3 Added update

So, I have a specific question about fast-growing integer sequences that are "well-defined," as I understand the term. But first, let me be clear about some ground rules: I'm certainly fine with integer sequences whose values are unprovable from (say) the axioms of ZFC, as sufficiently large Busy Beaver numbers are. Crucially, though, the values of your the sequence must not depend on any controversial beliefs about transfinite sets. So for example, the "definition"

makes sense in the language of ZFC, but it wouldn't be acceptable for my purposes. Even a formalist---someone who sees CH, AC, large-cardinal axioms, etc. as having no definite truth-values---should be able to agree that you've we've picked out a specific positive integer.

Update: After reading the first few comments, it occurred to me that the motivation for this question might not make sense to you, if you don't recognize a distinction between those mathematical questions that are "ultimately about finite processes" (for example: whether a given Turing machine halts or doesn't halt; the values of the super-recursive Busy Beaver numbers; most other mathematical questions), and those that aren't (for example: CH, AC, the existence of large cardinals). The former I regard as having a definite answer, independently of the answer's provability in any formal system such as ZFC. (If you doubt that there's a fact of the matter about whether a given Turing machine halts or runs forever, then you might as well also doubt that there's a fact of the matter about whether a given statement is or isn't provable in ZFC!) For questions like CH and AC, by contrast, one can debate whether it even means anything to discuss their truth independently of their provability in some formal system.

In this question, I'm asking about integer sequences that are "ultimately definable in terms of finite processes," and which one can therefore regard as taking definite values, independently of one's beliefs about set-theoretic questions. Of course, "ultimately definable in terms of finite processes" is a vague term. But one can list many statements that certainly satisfy the criterion (for example: anything expressible in terms of Turing machines and whether they halt), and others that certainly don't (for example: CH and AC). A large part of what I'm asking here is just how far the boundaries of the "definable in terms of finite processes" extend!

Yes, it's possible that my question could degenerate into philosophical disagreements. But a priori, it's also possible that someone can give a sequence that everyone agrees is "definable in terms of finite processes," and that blows my f(n) and z(n) out of the water. The latter would constitute a completely satisfying answer to the question.

show/hide this revision's text 2 Refocused the question in light of comments
show/hide this revision's text 1