Non-comparable natural numbers

Question

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.

Answer 1

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