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