<p>When you say "undecidable" I assume you mean it is independent of a theory such as ZFC. There will be statements like
$$B(m)&gt;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.</p>

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

<p>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&gt;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&gt;\sum_{i=1}^k 2B(m_i)n_i\tag{*}$$
and so arguably (*) provides a <strong>Yes</strong> answer to your question.</p>

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

CC BY-SA 4.0
2018-08-15T18:31:53.240Z
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.
Stella Biderman
CC BY-SA 4.0
2018-08-15T23:36:17.643Z
@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 https://arxiv.org/abs/1605.04343
Bjørn Kjos-Hanssen
CC BY-SA 4.0
2018-08-15T18:24:38.430Z
2018-08-15T18:24:38.430Z
Bjørn Kjos-Hanssen
<p>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 <span class="math-container">$2^{2^{2^{2}}}$</span> would also be an acceptable thing to write down.</p>

<p>The value of the Busy Beaver function, <span class="math-container">$BB(x)$</span>, cannot be determined (in ZFC, or any reasonable consistent axiomatic system) for large values of <span class="math-container">$x$</span>. In particular, <span class="math-container">$BB(10^4)$</span> cannot be determined <a href="https://www.scottaaronson.com/busybeaver.pdf" rel="nofollow noreferrer">as per this paper</a>. However, this doesn't mean that we cannot compare values of the Busy Beaver function. For example, we can prove that <a href="https://cstheory.stackexchange.com/q/9652/22045"><span class="math-container">$BB(x)$</span> is strictly monotonic</a>.</p>

<p>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)?</p>

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

<p>If we let <span class="math-container">$f(x)$</span> take on the value of <span class="math-container">$3$</span> if <span class="math-container">$BB(x) &gt;$</span> [something ungodly large and inexpressible on this website] and <span class="math-container">$7$</span> if it’s not, then <span class="math-container">$f(10^4)$</span> and <span class="math-container">$6$</span> are incomparable.</p>

<p>This doesn’t satisfy me, largely because <span class="math-container">$f$</span> 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.</p>

CC BY-SA 4.0
2018-08-15T17:41:11.530Z
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
CC BY-SA 4.0
2018-08-15T18:07:37.233Z
@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.
Stella Biderman
CC BY-SA 4.0
2018-08-15T18:25:30.053Z
According to the answer in this post: https://cstheory.stackexchange.com/questions/9652/is-every-busy-beaver-strictly-monotonic-asymptotically, it seems like BB is indeed strictly monotonic
Avi Tal
CC BY-SA 4.0
2018-08-17T09:32:18.393Z
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).
Andrej Bauer
<computability><undecidability>
Non-comparable natural numbers
Stella Biderman
# Non-comparable natural numbers

(Asked by: username_0 on 2018-08-15)

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](https://www.scottaaronson.com/busybeaver.pdf). 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](https://cstheory.stackexchange.com/q/9652/22045).

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.

**Tags:** computability, undecidability
> **Comments:**
> **username_1**: 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.  
> **username_0**: @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.  
> **username_2**: According to the answer in this post: https://cstheory.stackexchange.com/questions/9652/is-every-busy-beaver-strictly-monotonic-asymptotically, it seems like BB is indeed strictly monotonic  
> **username_3**: 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).  

---

## 1 answers

### Answer by username_4 on 2018-08-15. Score: 9 | Accepted answer

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

> **Comments:**
> **username_0**: 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.  
> **username_4**: @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 https://arxiv.org/abs/1605.04343  

---

