Succinctly naming big numbers: ZFC versus Busy-Beaver Years ago, I wrote an essay called Who Can Name the Bigger Number?, which posed the following challenge:


*
You have fifteen seconds. Using standard math notation, English words, or both, name a single whole number---not an infinity---on a blank index card. Be precise enough for any reasonable modern mathematician to determine exactly what number you’ve named, by consulting only your card and, if necessary, the published literature.
The essay went on to discuss systems for naming increasingly huge numbers concisely---including the Ackermann function, the Busy Beaver function, and super-recursive generalizations of Busy Beaver.
Recently (via Eliezer Yudkowsky), the claim has come to my attention that there are ways to concisely define vastly bigger numbers than even the super-recursive Busy Beaver numbers, using set theory.  (See for example this page by Agustín Rayo, which proposes a definition based on second-order set theory.)  However, whether these definitions work or not seems to hinge on some very delicate issues about definability in set theory.
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 the sequence must not depend on any controversial beliefs about transfinite sets.  So for example, the "definition"


*
n := 1 if CH is true, 2 if CH is false


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 we've picked out a specific positive integer.

Let me now describe the biggest numbers I know how to name, consistent with the above rules, and then maybe you can blow my numbers out of the water.
Given a Turing machine M, let S(M) be the number of steps made by M on an initially blank tape, or 0 if M runs forever.  Then recall that BB(n), or the nth Busy Beaver number, is defined as the maximum of S(M) over all n-state Turing machines M.  BB(n) is easily seen to grow faster than any computable function.  But for our purposes, BB(n) is puny!  So let's define $BB_1(n)$ to be the analogue of BB(n), for Turing machines equipped with an oracle that computes $BB_0(n):=BB(n)$.  Likewise, for all positive integers k, let $BB_k$ be the Busy Beaver function for Turing machines that are equipped with an oracle for $BB_{k-1}$.  It's not hard to see that $BB_k$ grows faster than any function computable with a $BB_{k-1}$ oracle. 
But we can go further: let $BB_{\omega}$ be the Busy Beaver function for Turing machines equipped with an oracle that computes $BB_k(n)$ given (k,n) as input.  Then let $BB_{\omega+1}$ be the Busy Beaver function for Turing machines with an oracle for $BB_{\omega}$, and so on.  It's clear that we can continue in this way through all the computable ordinals --- i.e. those countable ordinals $\alpha$ for which there exists a way to describe any $\beta < \alpha$ using a finite number of symbols, together with a Turing machine that decides whether $\beta < \beta'$ given the descriptions of each.
Next, let $\alpha(n)$ be the largest computable ordinal that can defined (in the sense above) by a Turing machine with at most n states.  Then we can define
$f(n) := BB_{\alpha(n)}(n),$
which grows faster than $BB_{\alpha}$ for any fixed computable ordinal $\alpha$.

A different way to define huge numbers is the following.  Given a predicate $\phi$ in the language of ZFC, with one free variable, say that $\phi$ "defines" a positive integer m if m is the unique positive integer that satisfies $\phi$, and the value of $m$ is the same in all models of ZFC.
Then let z(n) be the largest number defined by any predicate with n symbols or fewer.
One question that immediately arises is the relationship between f(n) and z(n).  I don't think it's hard to show that there exists a constant c such that $f(n) < z(n+c)$ for all n (please correct me if I'm wrong!)  But what about the other direction?  Does z(n) grow faster than any function definable in terms of Turing machines, or can we find a function similar to f(n) that dominates z(n)?  And are there other ways of specifying big numbers that dominate them both?

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.
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.

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 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.
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.
 A: It seems that the philosophical position you're taking for granted is close to the position called "predicativism" advocated by mathematicians such as Poincarè and Weyl, and whose boundaries have been delineated more precisely by Solomon Feferman. Roughly, Feferman's position is that the notion of an "arbitrary set" is not well-defined enough for statements like AC and CH to take on definite values. So instead we should restrict our attention to the natural numbers and any questions which are "implicit" in our concept of the natural numbers; for example, talking within Peano Arithmetic (PA) makes sense, but so does talking about the truth of PA-strings, and talking about the truth of strings which talk about the truth of PA-strings, and so on. In his system, questions about the Busy Beaver functions $BB_\alpha$ have definite values whenever $\alpha$ is an ordinal less than $\Gamma_0$, where $\Gamma_0$ is the Feferman-Schutte ordinal.
It might be possible to extend predicativity to some ordinals greater than $\Gamma_0$ without losing "truth-definiteness"; for example, this is argued by Nik Weaver. But I think extending to the first non-recursive ordinal (i.e. the Church-Kleene ordinal), which is implicit in the function $f(n) = BB_{\alpha(n)}(n)$ defined in the OP, is problematic. This is because the notion of "ordinalhood" is not a notion which is "ultimately definable in terms of finite processes", in your terms. To be more specific, let's recall that a computable ordinal is a computable ordering of $\mathbb N$ with the property that every nonempty subset of $\mathbb N$ has a least element with respect to this ordering. The notion of a computable ordering is certainly well-defined, but the ordinalhood property depends on universal quantification over the realm of subsets of the integers. According to Feferman, such quantification is ill-defined because "the concept of the totality of arbitrary subsets of $\mathbb N$ is essentially underdetermined or vague" -- because sets are introduced by definitions, and no formal system for describing how we define things can capture all of the different ways in which we can define things.
Now, you may disagree with Feferman on this point, perhaps being skeptical only of definite totalities consisting of all subsets of $\mathbb R$ or higher types. In which case I think that would be a new philosophical position, and it would be worth expanding on what exactly the boundaries of this system are, and what the motivation for those boundaries are.
On the other hand, without accepting the notion of a totality of subsets of $\mathbb N$, one can philosophically accept the notion of ordinalhood as somehow describing the "well-definedness" of concepts -- that is, an ordering of the integers is said to be an ordinal if any recursive definition (in a particular formal language) of a function $f:\mathbb N\to\mathbb N$ of the form
$$
f(n) = F(f\upharpoonleft \{m : m < n\})
$$
determines a well-defined total function $f:\mathbb N\to\mathbb N$. But this raises issues of whether the concept of "well-definedness" is really a well-defined concept. Certainly, a diagonal argument may cause problems if we intend to mean the same thing by the two uses of the phrase "well-defined" in the previous sentence. Also, the dependence of this concept on the formal language used for the universal quantification over $F$ may also be problematic. (You can't quantify over all formal languages for the same reason you can't quantify over all sets.) But perhaps these philosophical issues are not too troublesome, in which case the question of whether or not a given ordering of the natural numbers is a well-ordering always has a definite truth value.
But in any case, it seems to me that if one accepts the notion of "well-definedness" described above, then one is no longer talking about those things which are "ultimately definable in terms of finite processes" -- instead, one has introduced new notions and is now talking about them.
So in conclusion, I don't think that the entry $f(n) = BB_{\alpha(n)}(n)$ given in the original post satisfies the rules for the contest laid down in the original post.
........
I've also spent some time thinking about the main question of this post, that is, what is the best strategy for winning a largest-number contest? After looking at a number of case studies (which I hope to write up at some point), I concluded that there are only three types of largest-number contests:


*

*Those in which whoever has the (slightly) bigger paper to write on wins.

*Those in which whoever has the most faith in (true) large cardinal axioms wins.

*Those which are not well-defined as mathematical contests, but instead ask philosophical questions.


The first kind of contest can usually be judged on a reasonable timescale, while the second kind of contest can often be judged on an unreasonable timescale. The third kind can't really be judged at all.
The simplest example is the Busy Beaver Contest: Given a (reasonably large) $n$, the challenge is to write a Turing machine on $n$ symbols, and the winner is whoever has the longest runtime (and is thus the best approximation to $BB(n)$). The optimal strategy is this:

*

*Pick a large cardinal axiom $\kappa$ that you think is $\omega$-consistent.

*Enter the following program into the contest:

For every $\sigma\leq 3\uparrow\uparrow\uparrow 3$(

For every Turing machine $m$ of Gödel number $\leq 3\uparrow\uparrow\uparrow 3$(

If $\sigma$ is the Gödel number of a proof in $ZFC+\kappa$ that $m$ halts(

Run $m$)))
        
        Essentially, what this strategy does is "run all of the strategies that your opponent might be using that you can prove halt". If your opponent is honest enough that he won't submit any entry that he doesn't believe will halt, and he doesn't believe any mathematical statement that can't be proven in a formal system of consistency strength $\leq ZFC+\kappa$, then you will win. So this is a contest of type 2.




An obvious modification to this contest would be to only allow entries which provably halt within some formal system, e.g. $\Sigma = PA$. (The proof of halting must be submitted with the entry, as otherwise the requirement is trivial since every program which halts, halts provably in PA.) Then the best strategy is to fix a large $n$ consider the formal system $\Sigma(n)$ which is the same as PA except that only statements of with $\leq n$ nested quantifiers are allowed in the proofs of theorems. Then $\Sigma(n)$ is provably $\omega$-consistent in PA, although the length of the proof of $\omega$-consistency increases as $n\to\infty$. So then you just replace $ZFC+\kappa$ by $\Sigma(n)$ in the previous strategy; now that strategy provably halts within PA. So as long as your $n$ is greater than your opponent's $n$, then you win. So this is a contest of type 1.
The original posting seems to be a largest-number contest of type 3...
A: I could be wrong, but I seem to have shown that $f$ is much faster growing than $z$. The intuition is that $f$ is a property of this beast with recursively growing Turing-degrees, while $z$ is defining numbers that TMs with low Turing degrees can figure out and outdo.
For any predicate $s$ in the language of ZFC with one free variable (call it "$x$"), let $M_s$ be a TM with an oracle for the halting problem that runs this algorithm given an integer $a$ as input:
   1  i := a
   2  REPEAT:
  *3      IF s(i->x) is a theorem of ZFC THEN:
   4          HALT AND RETURN i
   5      ELSE:
   6          i := i + 1

* Denotes a step that depends on the halting oracle

Now in the space of all TMs with an oracle for $BB_1$, for any $n$ you'll find some $T_n$ that runs the following algorithm when given a blank tape:
   1  biggest := 0
   2  FOR EACH n-or-fewer-character string s:
   3      IF s is a predicate in the language of ZFC with one free var "x" THEN:
 **4          IF M_s(1) halts THEN:
  *5              b := M_s(1)
 **6              IF M_s(b+1) loops forever THEN
   7                  // Now we know s defines b
   8                  IF b > biggest THEN:
   9                      biggest := b
  10  IDLE FOR biggest STEPS
  11  HALT

 *Denotes a step that depends on the BB_1 oracle by way of the halting oracle
**Denotes a step that depends on the BB_1 oracle

For all $n$, $T_n$ runs for a little longer than $z(n)$ steps when run on a blank tape. And there's no reason why the state count $S(T_n)$ of the most compact choice of $T_n$ should grow faster than $n$. Therefore $BB_2$(n) dominates $z(n)$.
A: This isn't an answer, but it's too long for a comment.
I don't think the computable ordinals are well enough defined for the function $f(n)$ to work. Suppose you give me a system mapping {$0,1$}$^* $ into the computable ordinals. I'll give you a system, which is your system together with a new symbol, $2$, which stands for the smallest ordinal you can't define in your system. I can then map the numbers {$0,1,2$}$^* $ back into {$0,1$}$^*$; my system reaches a computable ordinal that's not defined in your system, and it even defines it with length 2.
So the computable ordinals are a concept that makes sense, but it is impossible to have a single encoding that gives you all of them. Thus, I don't see how your function $f$, which is defined using the phrase 

Next, let $\alpha(n)$ be the largest
  computable ordinal that can defined
  (in the sense above) by a Turing
  machine with at most $n$ states.

works. You should be able to get a Turing machine with an oracle that corresponds to any computable ordinal, but that's where it stops.
A: I have another question which is too long to fit into a comment: how do you even know that $f(n)$ is increasing? 
If you have two Turing Machines $M$ and $M'$ that realize the same ordinal $\alpha$, there is no guarantee (as far as I can see) that $BB_\alpha^M(n) = BB_\alpha^{M'}(n)$, because (if $\alpha > \omega$) the Turing machine that computes $BB_\alpha^M$ needs to use the encoding defined by $M$ to index into ordinals less than $\alpha$.  With $M$ and $M'$, there may not even be a computable map from the index generated by $M$ to the index generated by $M'$. You might be able to compute this map using $BB_\alpha^M$, but I don't even see how to do that. Thus, $BB_\alpha(n)$ doesn't seem well-defined; you need to specify the encoding into ordinals less than $\alpha$ for it to be well-defined. So even if
$\alpha > \beta$, it's not clear that $BB^M_\alpha(n)$ grows faster than $BB^{M'}_\beta(n)$. It's possible that there are some computable ordinals where the index function is so complicated that you can't use it to compute anything useful. 
You should be able to fix this by defining $f(n)$ to be $BB_\alpha^M(n)$ for the Turing machine $M$ with $n$ states so that $BB_\alpha^M(n)$ takes the maximum value over all such Turing machines.
UPDATE: and now I have what may be an answer to Scott's question. Is there any reason you have to have the Turing machine $M$ that defines the oracle for $\alpha$ be a vanilla Turing machine. Couldn't you let it have access to an oracle for BB, as well. This way, you can define classes using machines like $T_\alpha^{M_\beta^{M'}}$. Now, just let $f(n)$ be the maximum value for $BB_\alpha^M(n)$ where $M$ is a machine defined in this recursive manner using $n$ symbols. 
Question: can you define ordinals that are strictly larger than any computable ordinal in this way? Or does this just define the same class of ordinals in much more complicated ways?
A: 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
A: This is not an answer. 
Scott, I am trying to understand the difference between the two. Could you please explain the reason for BB being OK? It seems to me that the usual argument for existence of the values for BB should be provable in a very weak set theory. We form the set of halting TM with n states, prove that it is finite, and take the maximum of steps before halting for each of them. The reason we can not compute the values is the logical complexity of the formula defining BB, we could compute it if it was $\Sigma_1$, but it is not. Am I correct? 
I guess that the distinction is about the complexity of the formula defining the function. It seems that you are OK with arbitrary quantifiers over natural numbers but not over sets of them. For example, what would you say if we use GC in place of CH?
So you are asking about arithmetical functions. What about BB for Turing machines with oracles in the arithmetical hierarchy?
Is using higher order quantifiers over natural numbers OK? What if I define it to be the BB for functions defined by such formulas?
I think the relation with truth predicate is that since you are OK with arithmetical formulas, you think they have definite truth values, but it seems that you don't think that formulas outside this hierarchy, e.g. those with set quantifiers over natural number necessary have definite truth values.
A: This picks up Scott's further question

can anyone come up with a better ZFC-based integer sequence that avoids these problems and matches or (better yet) exceeds the growth rate of f, while not being dependent on a particular model of ZFC?

I can't see anything in the Turing machine style definition that can't be encoded with ZFC.  Translate any TM-style definition of $f$ into a ZFC-style definition, using standard machinery such as treating the TM state transition table as a binary relation, letting an integer encode the current state of a tape, and collecting together the right objects into oracle sets.  Then let $z$ be the ZFC-style definition of $f$.
In your definition of $f$ you are using a description which is more compact than ZFC, in the sense that your parameterize it with $n$ states in each of the two TMs you compose, instead of $n$ symbols which is all you allow for $z$.
What am I missing: what specific feature does the TM style definition bring that is not already in ZFC?  I would agree that the TM style definition allows expressing larger numbers than an equivalent length ZFC description.  But this seems to be a feature of what is being counted, not necessarily that TMs are more expressive, let alone "maximally" expressive.
A: This is basically a comment but it's too long for that.  I'm hoping that maybe I can help explain to Scott why there's an issue with his "definition" of "$\phi$ defines $m$."
The fundamental problem is that it's not clear what it means for $m$ to "satisfy $\phi$".  We can certainly take the formula $\phi$ and syntactically insert $m$ to produce a formula $\phi(m)$.  But merely producing $\phi(m)$ does not determine whether "$m$ satisfies $\phi$."  Whether $m$ satisfies $\phi$ hinges on whether $\phi(m)$ is true.  And it's not clear what this means.
When I say that it's not clear what it means, I'm not saying that we don't know any algorithm for determining truth. If that were the only issue then there would be nothing for a classical mathematician to complain about.  The problem is worse than that.  We don't know what the word "true" even means here.  This is where Tarski's theorem comes in.  We can't even define the word "true" using ordinary mathematical means.  If we could, then we would be able to formalize that definition in ZFC, just like we can formalize all ordinary mathematical discourse, and that's just not possible.
Perhaps a concrete example will help.  Let $\phi(x)$ be "$x=1$ and there is a cardinal strictly between $\aleph_0$ and $2^{\aleph_0}$."  Does 1 satisfy $\phi$?
Now this problem isn't insurmountable.  There are ways you can try to define truth.  But it's a subtle business and you need to be explicit and careful.  Without that, we don't have a clear definition of what it means for $m$ to satisfy $\phi$ and hence we don't have a clear definition of what it means for $\phi$ to define $m$.
