Can you consistently add axioms about the Busy Beaver function to ZF?

Question

Consider a Turing Machine with $N$ states which checks all theorems of ZF and halts upon finding a contradiction. If ZF were consistent and could prove the value of $BusyBeaver(N)$, then it would be able to prove its own consistency, which Gödel proved impossible; so either ZF is inconsistent or the value of $BB(N)$ is independent of ZF.

But what if we add to ZF an extra axiom K, which specifies the exact (true) value for $BB(k)$ for some large $k$? If ZF is consistent (edit: and sound), then ZFK is consistent (else a contradiction in ZFK would be a proof in ZF of ~K). Now assume that there is a Turing machine with $k$ states or fewer which checks all theorems of ZFK. If it halts, then ZFK is inconsistent, so ZF is inconsistent or unsound. If it doesn't halt after $BB(k)$ steps, then it has proved the consistency of ZFK, which is impossible by Gödel.

It seems like I've shown that either ZF is inconsistent or unsound or that there is no such $k$-state Turing machine which proves the theorems of ZFK. But it seems obvious that for sufficiently large $k$, there are such Turing Machines, since all they need to do is symbolic manipulation of finite axioms. What's going on?

Answer 1

Let $b_k$ be the assertion that the busy beaver function at $k$ has the value that it actually has, that is, the value it has in the standard natural numbers of the meta-theory. We know that not all of these statements are provable in ZF, if ZF is consistent, since if they were then we would be able to compute the values of the busy beaver function by searching for such proofs.

Theorem. The following are equivalent.

1. The theory $\text{ZF}+b_k$ is consistent, for any particular $k$.

2. The theory $\text{ZF}+b_{k_0}+\cdots+b_{k_n}$ is consistent, for any finite list of numbers $k_0,\ldots,k_n$.

3. ZF is $\Sigma^0_1$-sound.

A theory is $\Sigma^0_1$-sound, if any $\Sigma^0_1$ statement that the theory proves is actually true. If ZF is $\Sigma^0_1$-sound, then any true $\Pi^0_1$ sentences must be consistent with ZF, for otherwise we would be able to prove the negation, which would be a false $\Sigma^0_1$-statement, contrary to soundness.

Proof. ($3\to 2$) Assume ZF is $\Sigma^0_1$-sound. It already proves all the true $\Sigma^0_1$ assertions about particular machines halting. The extra assertions of the various $b_k$ are $\Pi^0_1$ assertions that no additional Turing machines of the given size halt at some later point. By soundness, these are consistent with ZF, as desired.

($2\to 1$) Immediate.

($1\to 3$) Suppose that we can consistently add any statements $b_k$ to ZF. Suppose that ZF proves some assertion $\exists n\, \varphi(n)$, where $\varphi(n)$ is $\Delta^0_0$. Consider the program $e$ that embarks on a search to find such an $n$. This program uses $k$ states for some $k$, and so if there is such an $n$, then ZF would prove that it would have to stop before the busy beaver value $BB(k)$, since otherwise we would violate the definition of $BB(k)$. Thus, if $ZF+b_k$ is consistent, ZF would prove that there is such an $n$ below the actual value of $BB(k)$. So the $\Sigma^0_1$ statement was true, and therefore ZF was $\Sigma^0_1$-sound, as desired. $\Box$

Meanwhile, let me point out that it is relatively consistent with ZF that ZF is not $\Sigma^0_1$-sound. For example, in any model of ZF in which $\neg\text{Con}(ZF)$, then obviously ZF will be proving false $\Sigma^0_1$ statements in the model. So if ZF is consistent, then so is ZF plus the assertion that ZF is not $\Sigma^0_1$-sound.

Answer 2

Pick your $k$ so that you're adding an axiom to ZF which contains a number $N$ that you've pulled out of somewhere, that purports that $BB(k)=N$. That equality (by supposition) happens to be true, but since it can't be proved by normal means, the best you can say about your new axiom is that it purports something. Now there are potentially three classes of $k$-state Turing machines:

Class 1: those that halt in $\le N$ steps Class 2: those that eventually halt, but in more than $N$ steps. Class 3: those that never halt.

Your new axiom claims, simply, that class 2 is empty. That is, if you run all the $k$-state TM's for up to $N$ steps, at least one machine will halt on exactly the $N$th step, and those which haven't halted by then will never halt.

In other words, the new axiom asserts a whole lot of otherwise undecidable $\Pi^0_1$ sentences that various TM's don't halt.

For large enough $k$, one of those machines will be a machine that searches for a proof in ZFC that 1=0.

In other words, the new axiom asserts (among other things), CON(ZFC). So yes, if you add an axiom asserting CON(ZFC), then $\vdash$CON(ZFC) which is no big surprise. This still works if your new axiom has given the wrong value of $N$, since that means you have an inconsistent theory, and inconsistent theories prove anything. Since the halting problem is undecidable, if you actually do have the right value of $N$, you can never prove it, because of all the machines that it asserts never halt, but that (as far as you can tell) eventually might halt if you run them long enough.

Answer 3

I think your argument in fact proves that there is no a Turing machine with $k$ states which can check all theorems of ZFK:

axioms of ZF can be enumerated by a very simple Turing machine $M_1$. But to describe the extra axiom K (which is of the form $BB(k)=\overline{n}$) we needs to describe the number $n$ and it needs at least a Turing machine $M_2$ with $k$ states (by the definition of $BB$ function). So if we combine the Turing machines $M_1$ and $M_2$ and write a Turing machine $M_3$ which enumerate all axioms of ZFK and then check all its theorems, it seems reasonable that this machine need more than $k$ states. This is the fact that your argument proves:

Theoerm. (assuming that ZF is $\Sigma_1$-sound) for any $k \in \mathbb{N}$, any Turing machine which checks all theorems of ZFK(which is ZF+$BB(k)=\overline{n}$, where $n$ is the true value of $BB(k)$) has at least $k+1$ states.