Non-comparable natural numbers

The "name the biggest number game" asks two players to write down a number secretly, and the winner is the person who wrote down the larger number. The game commonly allows players to write down functions evaluated at a point, so $$2^{2^{2^{2}}}$$ would also be an acceptable thing to write down.

The value of the Busy Beaver function, $$BB(x)$$, cannot be determined (in ZFC, or any reasonable consistent axiomatic system) for large values of $$x$$. In particular, $$BB(10^4)$$ cannot be determined as per this paper. However, this doesn't mean that we cannot compare values of the Busy Beaver function. For example, we can prove that $$BB(x)$$ is strictly monotonic.

Lets suppose that we allow players to write down expressions involving compositions of elementary functions, natural numbers, and the Busy Beaver function. Are there two expressions that the two players can write down such we can prove in ZFC that determining the winner in ZFC is impossible (assuming ZFC is consistent)?

EDIT: Originally this question said “... arbitrary combinations of computable functions, natural numbers, and the Busy Beaver function.”

If we let $$f(x)$$ take on the value of $$3$$ if $$BB(x) >$$ [something ungodly large and inexpressible on this website] and $$7$$ if it’s not, then $$f(10^4)$$ and $$6$$ are incomparable.

This doesn’t satisfy me, largely because $$f$$ isn’t a reasonable function for someone to use in this game. I don’t see how to phrase my intuition about this though, so I’ve restricted the question to avoid piecewise functions.

• Can the undecidability of $BB(10^4)$ be extended to, say, individual bits? If so, then you would just have to do something like compare the 3rd least significant bit of $BB(10^4)$ with the 8th least significant bit.
– mhum
Aug 15 '18 at 17:41
• @mhum questions like that are tricky because the value of $BB(x)$ is actually encoding dependent. There are encodings for which $BB(x)$ is always even, for example. My understanding is that all questions along those lines are either trivially computable or open, depending on the encoding. Aug 15 '18 at 18:07
• According to the answer in this post: cstheory.stackexchange.com/questions/9652/…, it seems like BB is indeed strictly monotonic Aug 15 '18 at 18:25
• The art of playing such games is to bend the rules, so I don't think it counts to say that some function is unreasonable. If we were to play the game, I would most definitely hit you with the most disgusting function I can think of (and I am a logician). Aug 17 '18 at 9:32

When you say "undecidable" I assume you mean it is independent of a theory such as ZFC. There will be statements like $$B(m)>n$$ (for natural numbers $m$, $n$) that are not decided by ZFC, assuming ZFC is consistent. Because otherwise we could compute the function $B$ just by searching for proofs in ZFC of such statements.
Since $B$ is Turing complete there is some Turing machine $\Phi$ with Con(ZFC)$\iff$ $\Phi$ accepts with oracle $B$ (on input 0, say) and $\neg$Con(ZFC)$\iff$ $\Phi$ rejects.
Now assuming that actually Con(ZFC) is true we know $\Phi$ accepts and there is some collection of facts $B(m_i)=n_i$, $1\le i\le k$ that was used in the computation (we may set it up so that the oracle access works in this way). Then $$\sum_{i=1}^k (B(m_i)-n_i)^2>0$$ is false, but this fact is not provable in ZFC, else ZFC would prove its own consistency. Of course this can be rewritten as $$\sum_{i=1}^k B(m_i)^2+n_i^2>\sum_{i=1}^k 2B(m_i)n_i\tag{*}$$ and so arguably (*) provides a Yes answer to your question.
However, I don't think we can figure out what these numbers $m_i$, $n_i$ are, because the queries are adaptive (what is asked about depends on answers to previous questions, and we don't know those answers).
• This is an excellent existence proof of what I’m looking for. However, I am specifically after an actual example of such an equation, with some kind of expression we could write down for $n,m$. You’re also right about my use of “undecidable” being incorrect, I’ve amended my question. Aug 15 '18 at 18:31
• @StellaBiderman yes and anyway if $n_0=B(7910)$ then the statement $B(7910)\le n_0$ is independent of ZFC by Aaronson and Yedidia's result at arxiv.org/abs/1605.04343 Aug 15 '18 at 23:36