But Gödel’s incompleteness theorem does not say that the statement “if M halts, it does so in fewer than x steps” is unprovable. So if you can prove a lower bound x on BB(k) using another Turing machine, and we certainly can do that, and prove this conditional statement; then it might actually be possible to give a ZFC proof about the value of BB(k). At least it doesn’t immediately follow from the incompleteness theorem that the value of BB(k) can not be proved.

Or am I missing something?

]]>The key insight is that “checking for infinite loops” is not a straightforward matter at all. For example, consider the following piece of pseudocode:

n := 2;

do {

n := n + 2;

if (IsItASumOfTwoPrimes(n) = FALSE) then halt;

}

where IsItASumOfTwoPrimes(n) returns TRUE if n can be written as a sum of two prime numbers, and FALSE otherwise. Also, n has the data type of an arbitrary positive integer—i.e., it can be as big as you want; the programming language will just allocate more and more memory for it.

The IsItASumOfTwoPrimes subroutine can clearly be written in a way where it always halts (just loop over the numbers from 1 to n, enumerate which ones are prime, and see if two of them sum to n).

But does the program as a whole halt? Well, that’s equivalent to asking whether every positive integer 4 or greater can be written as a sum of two prime numbers, which is the famous Goldbach Conjecture! If the Goldbach Conjecture is true, then you might say the program “contains an infinite loop,” but it’s not a loop of any simple kind, because the even number that’s being tested keeps increasing, and the only reason why the loop *is* a loop is that all of them can be written as a sum of two primes.

OK, but you might still think that with sufficient cleverness, it would be possible to create an infinite loop detector that worked even for programs like the above. But that’s precisely what Alan Turing ruled out in 1936, with his proof of the unsolvability of the halting problem. Go study that proof if you haven’t—I promise you won’t regret it. (My *Quantum Computing Since Democritus* book is one of many places where you could learn about it.)

Now, directly related to the unsolvability of the halting problem, is the ability to write a *single* computer program, which runs forever if (say) ZFC set theory is consistent, or halts if ZFC is inconsistent. So, this is a single program for which ZFC already can’t prove whether it halts or runs forever (on pain of violating Gödel’s Incompleteness Theorem). This was again known since the 1930s—i.e., it was clear that some program like that exists, with some number of states.

What Adam and I did, was simply to calculate the first *explicit* upper bound on the number of states in a Turing machine that has this property, of halting if and only if ZFC is inconsistent. We got 7910, although Stefan O’Rear has since improved our bound to below 1000.

I did not say that a Gödel statement does contradict ZFC.

I meant that computing a halting condition for any given statement can take so much time, so that the series of processed statements converges. Citing from the paper:

1. Z … enumerates, one after the other, each of the provable statements in ZFC

2. Z … halts if it ever reaches a contradiction,

3. Because this machine will enumerate every provable statement in ZFC, it will run forever if and only if ZFC is consistent.

Let’s take that step 2. requires t(i) time, so at step i the machine’s performance equals to 1 / t(i) statements in the unit of time. The total amount of processed statements would be equal to a sum of series 1 / t(i).

The statement 3. implicitly claims that this sum is infinite (“every provable statement”), whereas it will converge to a certain finite number, due to increase of contradiction check complexity.

]]>First, there’s never any violation of the Incompleteness Theorem, not if the machine runs forever and not if it halts.

Second, a Gödel statement doesn’t contradict ZFC (why would it?).

Third, the Z machine never makes any non-obvious semantic judgments about what statements do or don’t contradict ZFC. If we ignore the complications caused by the use of Friedman’s statement, such a machine simply halts if it finds a ZFC proof of 0=1 and runs forever if it doesn’t: that’s all.

]]>In that case the machine will run forever and still will not violate the Second Incompleteness Theorem.

]]>