A few years ago, Scott Aaronson and a student of his published this paper, in which they demonstrate the existence of a 7918 state Turing machine whose behavior is independent of ZFC. In particular, whether the machine halts or not can not be proven by ZFC. This entails that ZFC cannot prove the value of BB(7918) – the number of steps taken by the longest running Turing machine with 7918 states before halting. And since ZFC is a first order theory and first order logic is complete, the unprovability of the value entails that BB(7918) actually has different values in different models of the axioms! So ZFC does not semantically entail its value, which is to say that ZFC underdetermines the Busy Beaver numbers!
This might sound really surprising. After all, the Busy Beaver numbers are a well-defined sequence. There are a finite number of N-state Turing machines, some subset of which are finitely-running. Just look at the number of steps that the longest-running of these goes for, and that’s BB(N). It’s one thing to say that this value is impossible to prove, but what could it mean for this value to be underdetermined by the standard axioms of math? Are there some valid versions of math in which this machine runs for different amounts of time than others? But how could this be? Couldn’t we in principle build the Turing machine in the real world and just observe exactly how long it runs for? And if we did this, then we certainly shouldn’t expect to get an indeterminate answer. So what gives?
Well, first of all, the existence of a machine like Aaronson and Yedidia’s is actually not a surprise. For any consistent theory T whose axioms are recursively enumerable, one can build a Turing machine M that enumerates all the syntactic consequences of the axioms and halts if it ever finds a contradiction. That is, M simply starts with the axioms, and repeatedly applies modus ponens and the other inference rules of T’s logic until it reaches a contradiction. Now, if T is strong enough to talk about the natural numbers, then it cannot prove whether or not M halts. This is a result of Gödel’s Second Incompleteness Theorem: If T could prove the behavior of M, then it could prove its own consistency, which would entail that it is inconsistent. This means that no consistent formal theory will be capable of proving all the values of the Busy Beaver numbers; for any theory T there will always be some number N for which the value of BB(N) is in principle impossible to derive from T.
On the other hand, this does not entail that the Busy Beaver numbers do not have definite values. This misconception arises from two confusions: (1) independence and unprovability are not the same thing, and (2) independence does not necessarily mean that there is no single right answer.
On (1): A proposition P is independent of T if there are models of T in which P is true and other models in which it is false. P is unprovable from T if… well, if it can’t be proved from the axioms of T. Notice that independence is a semantic concept (having to do with the different models of a theory), while unprovability is a syntactic one (having only to do with what you can prove using the rules of syntax in T). Those two are equivalent in first order logic, but only because it’s a complete logic: Anything that’s true in all models of a first-order theory is provable from its axioms, so if you can’t prove P from T’s axioms, then P cannot be true in all models; i.e. P is independent. Said another way, first-order theories’ semantic consequences are all also syntactic consequences.
But this is not so in second-order logic! In a second-order theory T, X can be unprovable from T but still true in all models of T. There is a gap between the semantic and the syntactic, and therefore there is a corresponding gap between independence and unprovability.
So while it’s true that the Busy Beaver numbers are independent of any first-order theory you choose, it’s not true that the Busy Beaver numbers are independent of any second-order theory that you choose. We can perfectly well believe that all the Busy Beaver numbers have unique values, which are fixed by some set of second-order axioms, and we just cannot derive the values from these axioms.
And on (2): Even the independence of the Busy Beaver numbers from any first order theory is not necessarily so troubling. We can just say that the Busy Beaver numbers do have unambiguous values, it’s just that due to first-order logic’s expressive limitations, we cannot pin down exactly the model that we want.
In other words, if BB(7918) is 𝑥 in one model and 𝑥+1 in another, this does not have to mean that there is some deep ambiguity in the value of BB(7918). It’s just that only one of the models of your theory is the intended model, the one that’s actually talking about busy beaver numbers and Turing machines, and the other models are talking about some warped version of these concepts.
Maybe this sounds a little fishy to you. How do we know which model is the “correct” one if we can’t ever rule out its competitors?
Well, the inability of first order logic to get rid of these nonstandard models is actually basic feature of pretty much any mathematical theory. In first-order Peano arithmetic, for instance, we find that we cannot rule out models that contain an uncountable number of “natural numbers”. But we don’t then say that we do not know for sure whether or not there are an uncountable infinity of natural numbers. And we certainly don’t say that the cardinality of the set of natural numbers is ambiguous! We just say that unfortunately, first order logic is unable to rule out those uncountable models that don’t actually represent natural numbers.
If this is an acceptable response here, if you find it tempting to say that the inability of first order theories of arithmetic to pin down the cardinality of the naturals tells us nothing whatsoever about the natural numbers’ actual cardinality, then it should be equally acceptable to say of the Busy Beaver numbers that the independence of their values from any given mathematical theory tells us nothing about their actual values!
Thanks a lot for the article, your explanation has clarified some of the things that confused me of the paper.
I still find it confusing anyway. What I thought I knew about recursiveness seems at first glance to contradict the results of the paper. As one example, the results related to the arithmetical hierarchy tell us that only the most basic sets of integers definable in first-order arithmetic (the ones in sigma01) are computable (the ones in pi10 too if you let the computer run forever), and after that, one arrives to an ever increasing hierarchy where each level is more uncomputable than the one before.
Another one is Tarski’s result on the undefinability of truth, which tells us that the godel numbers of “true” arithmetic expressions are not definable in arithmetic and therefore not even in the arithmetical hierarchy (even after an indefinite number of uncomputable levels).
And then it comes this paper which says that the consistency of ZFC (or ZF), which is way more powerful than arithmetic and which can prove the consistency of arithmetic, is equivalent to a very simple turing machine (which would put the problem in either sigma01 or pi01, I’m not sure which one of those two).
Your article suggests that the difference may be due to the fact that the “computable”, “first-order” version of ZFC is rather weak and there may be statements which are consequence of ZFC in, for example, second-order arithmetic, that escape that “computable” part that the paper talks about. The paper also mentions that the computable portion of ZFC and of ZF are equivalent, which seems to point to that direction.
Is there any suggestion for me on how could I get out of this cloud of misunderstanding I’m in about the problem?
So everything that you’ve said here is correct. Most sets of integers definable in first order arithmetic are uncomputable, that’s true. Some sets of integers are not only uncomputable, but also not even definable in first-order arithmetic, and your example of the set of Gödel numbers of true arithmetic expressions is spot on. And ZFC is recursively axiomatizable, meaning that there’s a Turing machine that semi-decides whether ZFC proves something. I.e. there’s a TM that takes as input a sentence X, returns “True” if X is provable from ZFC, and runs forever otherwise. So the set of Gödel-numbers-of-theorems-of-ZFC is semi decidable (recursively enumerable).
I think that maybe where your confusion is coming from is what is meant by “the set of true arithmetic expressions”. This set is not the same as “the set of arithmetic expressions proved by PA” or “the set of arithmetic expressions proved by ZFC”. Both of these theories are known to be incomplete, in the sense that there are sentences about arithmetic that are true in the standard model, and yet not provable. The key to understanding what’s going on is that ZFC has nonstandard models in which “the set of natural numbers” contains nonstandard elements that are infinitely large (larger than 0, 1, 2, and all the rest of the standard naturals). The axioms of ZFC are not sufficient to fully pin down the standard model of the natural numbers, and each of these nonstandard models satisfy all the axioms of ZFC. We could imagine adding new axioms to ZFC that rule out some of these nonstandard models and get closer to picking out the unique standard model (the model in which every natural number follows from finite applications of the successor function to 0). But it turns out that NO set of axioms, computable or otherwise, suffices to fully pin down the natural numbers.
The best we could possibly do, even given arbitrarily powerful oracles for any sorts of halting problems we like, is to just collect the set of all first-order sentences of ZFC that are true of the standard model of natural numbers. (Amazingly, even this set doesn’t pin down the natural numbers! I.e. even if you say every true thing about natural numbers that is expressible in first-order ZFC, you still end up with nonstandard models that have infinitely large numbers. We’d need a more powerful logic to give us the expressive power to uniquely define the natural numbers.) But regardless, this set is what’s referred to as “true arithmetic”: the set of all first-order sentences that are true in the standard model of natural numbers. The set of Gödel numbers of the axioms of true arithmetic is infinitely high on the computability hierarchy (it appears at the Turing degree 0^(w)), and thus the Turing machine that semi-decides the theorems of ZFC gets nowhere near semi-deciding true arithmetic.
I’m not sure if this was totally helpful, you can try rephrasing your question if it wasn’t.