19
$\begingroup$

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?

$\endgroup$
7
  • 1
    $\begingroup$ Your claim that if ZF is consistent, then so is ZFK amounts to a soundness assumption on ZF, that we can add true arithmetic assertions to it consistently. But this is an assumption going beyond ZF. $\endgroup$ Sep 13, 2017 at 1:13
  • 1
    $\begingroup$ What does it mean for a Turing machine to "prove all theorems of ZFK"? Do you mean that it enumerates them one after the other? If so, then of course this machine never halts. I have trouble making sense of this part of your argument. And what does it mean for a Turing machine to "prove its own consistency"? Or are you referring to the theory in that remark, or what? $\endgroup$ Sep 13, 2017 at 1:16
  • $\begingroup$ Sorry, you're right Joel. I meant that it checks all theorems, and halts if it finds an inconsistency; also that if it doesn't halt, it proves the consistency of ZFK. $\endgroup$ Sep 13, 2017 at 1:50
  • 2
    $\begingroup$ BTW: $k < 8000$ by Yedidia and Aaronson, scottaaronson.com/busybeaver.pdf $\endgroup$ Sep 13, 2017 at 5:38
  • 2
    $\begingroup$ Also note that if $k \ge 64$ you potentially have a proof of the non-existence of rank-into-rank cardinals (or the inconsistency of rank-into-rank cardinals with ZFK): cheddarmonk.org/papers/laver.pdf $\endgroup$ Sep 13, 2017 at 10:04

3 Answers 3

17
$\begingroup$

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.

$\endgroup$
21
  • 13
    $\begingroup$ Perhaps this isnt' a place to ask, but I've had a couple of students ask me what "actually true" means if truth depends on the model (that would usually be a smart student who learned about models). How do you answer such a question, from a pedagogical point of view? $\endgroup$ Sep 13, 2017 at 6:27
  • 4
    $\begingroup$ @AndrejBauer I believe that is a deep philosophical question. But one can begin to answer by making the theory/meta-theory distinction: when we use a theory, we are typically committed to certain mathematical assertions in the meta-theory. Often, a very weak meta-theory suffices, but one can also work in a strong meta-theory. For example, the model theorists typically undertake model theory in ZFC itself, and in this case one can view the meta-theory as ZFC, even when one analyzes ZFC as an object theory. But it is important to recognize that these two theories are not the same. $\endgroup$ Sep 13, 2017 at 11:50
  • 4
    $\begingroup$ To assert that a particular mathematical statement is "actually true" is to make the assertion in the meta-theory as opposed to the object theory, and questions of soundness are always about the interaction of this kind of truth. Matters get philosophically complicated, however, when you realize that there are many different meta-theories you might use, or indeed an entire hiearchy of theories, each of which might serve as a meta-theoretic context for the object theories it has. In this case, claims of "actually true" should be understood as reletive to a particular meta-theoretic context. $\endgroup$ Sep 13, 2017 at 11:52
  • 1
    $\begingroup$ I am not asking whether it's possible to arrange different values of $b_k$ but whether the two of us might actually discover different values. (Of course, my evil plan is to coax you into admitting that logic is an experimental science.) $\endgroup$ Sep 13, 2017 at 13:36
  • 1
    $\begingroup$ I think I got it now. The sentence $b_k$ is asserting equality between the value the base theory gives to $BB(k)$ and the value the meta-theory gives to $BB(k)$. (So even though both numbers might not be concretely representable, by asserting they are equal we get a stronger statement.) We could then iterate this process and get even stronger statements by working in a meta-meta-theory, etc... $\endgroup$ Sep 13, 2017 at 18:27
3
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ That makes sense, but for large enough k, will one of those machines also be a machine that searches for a proof in ZFK that 1=0? $\endgroup$ Sep 14, 2017 at 12:13
  • 2
    $\begingroup$ @RichardNgo You have defined ZFK to depend on $k$. For any fixed $k$, for large enough $k'$, one of the machines will be a machine that searches for contradictions in $ZFK_k$. But we can never take $k'=k$ by Godel's theorem. $\endgroup$
    – Will Sawin
    Sep 20, 2017 at 9:22
0
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.