Why is the status of the period in Laver tables not settled? Sequence A098820 in the OEIS is purely combinatorially defined (all you need to know is integers), and non-decreasing; it is known (Laver, 95) that assuming Large Cardinal axiom I3 the sequence goes to infinity. However, under ZF or ZFC the convergence status is not known.
Now imagine Alice works under ZF+I3 while Bob works under ZF only. Bob starts writing:


*

*Pick any $A\in \Bbb N$. 

*Ask Alice to find $n\in \Bbb N$ such that $u_n\geq A$ in her world (we know that there is such an $n$) and communicate it to us. 

*Compute $u_n$ ourselves and see if $u_n\geq A$ here too, which it obviously is, since the definition of the sequence is purely combinatorial and does not rely on any complicated axioms.



How is this not a proof that the sequence goes to infinity under ZF?

My thought is that perhaps I3 is only not known to be inconsistent with ZF, which is quite different from known to be consistent with. So there would be two options: either the sequence provably goes to infinity in ZF, or I3 and ZF are inconsistent. Is this right or am I missing the point?
 A: This doesn't work - the issue is with nonstandard natural numbers.
(There's a related comment about complexity - the nonstandardness issue can be gotten around for $\Pi^0_1$ theorems, but your principle is $\Pi^0_2$ - but the nonstandardness issue really lies at the heart of the Alice-Bob idea, so I think it should be mentioned first.)

In the game you're imagining, why can Alice and Bob "share numbers"? Think of them as holding specific models $A\models\mathsf{ZFC}+I_3$ and $B\models\mathsf{ZF}$ respectively; in order for Alice to "see" Bob's questions we need $\omega^B\subseteq\omega^A$, and - far more importantly - in order for Bob to "use" Alice's answers we need $\omega^A\subseteq\omega^B$.


*

*To see the issue, suppose Bob is working with the true natural numbers and think about what would happen if we replace Alice with Sam, who holds a model $S\models\mathsf{ZF}+\neg Con(\mathsf{ZF})$. Bob is skeptical of Sam, and asks "What is an example of a (code for a) proof of a contradiction in $\mathsf{ZF}$?" Sam replies, "I'm glad you asked - it's [eldritch horror]." If Sam's response to Bob is a nonstandard natural number, there's not much use Bob can get from it. And of course the true nightmare situation is when two models have incomparable versions of the natural numbers.


So in order for the idea in your post to work as written, we would need the following: for every model of $\mathsf{ZF}$, there is a model of $\mathsf{ZFC}+I_3$ with the same natural numbers. And in fact this is false (unless $\mathsf{ZF}$ is inconsistent): $\mathsf{ZF}$ has a model which thinks (say) that $\mathsf{ZF}$ is inconsistent, but $\mathsf{ZFC}+I_3$ doesn't (regardless of whether it's consistent).

A more careful implementation of the same idea will show that whenever $\varphi$ is $\Pi^0_1$ and $\mathsf{ZFC}+I_3$ proves $\varphi$, then $\mathsf{ZF}$ proves "If $\mathsf{ZFC}+I_3$ is consistent then $\varphi$ is true." However, this still doesn't apply to the above problem, since unboundedness is $\Pi^0_2$.
