2. For an alternative argument, one could use the so-called Reflection Principle (Schema), which says for any finite list a_1, …, a_n of axioms of ZFC, ZFC proves the formal statement that “The conjunction a_1 ^ … ^ a_n has a standard transitive model”. Here, a_1, …, a_n in the formal statement are really the obvious formalized descriptions of the axioms a_1, …, a_n. [Note that the reflection schema is weaker than ZFC proving that “for any finite list if axioms, their conjunction has a model”; also, the latter would imply that ZFC proves “ZFC is consistent”, by Gödel’s COMpleteness Theorem – and this would in turn, by the INCOMpleteness theorem imply that ZFC is actually inconsistent. As such, the Reflection schema does not contradict consistency of ZFC.] The reasoning would now be as follows: Suppose someone finds a proof from ZFC of the statement “ZFC is inconsistent”. Let a_1, … a_n be the finitely many axioms needed to (formalize notions required to even speak of the statement “ZFC is consistent” and to) prove “ZFC is inconsistent”. If we believe in the set-theoretic principles needed for the proof of the Reflection schema, then we actually have a standard transitive model of a_1^ …. ^ a_n, and the same argument as in 1. implies that ZFC is really inconsistent since “ZFC is inconsistent” holds in this model.

Again, a finitist would not be happy to accept this. At first sight, one might actually think that (s)he would at least agree that the above demonstrates that ZFC proves the formal statement “if ZFC is consistent, then ZFC does not prove the formal statement “ZFC is inconsistent” “ (which would surely be better than the finist’s conclusion in (1), but still not of convincing power since it could just be that ZFC proves “ZFC is inconsistent” in which case none of the conclusions are surprising). However, (s)he would _not_ agree with that, for the subtle reason that part of the above argumentation cannot even be formalized in ZFC. When we used the Reflection schema, we quantified over an unknown finite list of axioms, and this is a misuse beyond its applicability (indeed, the same kind of misuse as when incorrectly concluding the the Reflection schema contradicts consistency of ZFC – here, though, the misuse would take place at a formal level).

[If one tries to convince the finitist this by formalizing not the entire argument, but only the part of the argument that comes after the identification of a_1, …, a_n, one ends up only demonstrating to him/her the dull fact that if ZFC proves “ZFC is inconsistent”, then ZFC proves “ZFC is inconsistent”.]

Now, I am not trying to argue that there is good reason to morally, whole-heartedly reject the above arguments. However, we are wondering whether there might be a purely finitistic argument demonstrating that if ZFC is consistent, ZFC does not prove its own inconsistency. Or – even settling for less – might there be an argument _formalizable in ZFC_ demonstrating that if ZFC is consistent, ZFC does not prove its own inconsistency? In short, argument (1) fails in this regard because it makes a stronger assumption than mere consistency, and argument (2) fails because it cannot be formalized properly.

We are looking forward to hearing your thoughts on this!

Best,

Nicholas

I had some technical issues posting the commentary, so I don’t really know what it’s going to look like eventually. At some point I tried splitting it into parts, and now it would seem that at least the first part is properly posted. I tried to post the second part as well, but I don’t see it displayed yet. (Please feel free to eventually delete any surplus posts…)

In the second part, I end by asking whether one could hope to find a finitistic proof that consistency of ZFC implies that ZFC does not prove its own inconsistency – or, less ambitiously, if one could even hope to find a prove _formalizable in ZFC_ of this implication.

Now, however, I think I found an answer myself, and it’s quite beyond what we had expected (Tobias deserves all the credit for stumbling over Löb’s theorem and pointing out that it might shed some light on the problem!) – it is also so strange that I couldn’t resist posting it:

Suppose that there _is_ in fact some argument, formalizable in ZFC, that consistency of ZFC implies that ZFC does not prove “ZFC is inconsistent”. In other words, suppose that ZFC proves the formal statement

“if ZFC is consistent, then ZFC does not prove “ZFC is inconsistent” “

Then, by contraposition, ZFC proves

“if ZFC proves “ZFC is inconsistent”, then ZFC is inconsistent”

Löb’s theorem asserts that if F is a formal system (subject to the usual requirements on expressivity) and L a sentence, then, if F proves the statement “if F proves “L”, then L”, then F proves L. Therefore, by Löb’s theorem, we conclude from the above that ZFC proves “ZFC is inconsistent”. In other words, there is no way of justifying in ZFC that consistency of ZFC prevents ZFC from proving its own inconsistency, unless it is in fact the case that ZFC proves its own inconsistency. I would say this more or less answers my original question in the negative.

At this point, I tried (again!) to google my way to enlightenment on this issue, and I finally came across the page

https://www.umsu.de/wo/archive/2005/04/15/Suppose_ZFC_proves_its_own_inconsistency

on which the poster seems to have made the same observation, though using in stead Gödel’s 2nd incompleteness theorem. This reasoning is somehow more elegant, in the sense that Gödel’s theorem is weaker than Löb’s (which implies Gödel’s, by letting L be some contradiction). Basically the argument is as follows:

ZFC proving

“if ZFC is consistent, then ZFC does not prove “ZFC is inconsistent” “

is equivalent to ZFC proving

“if ZFC is consistent, then ZFC + “ZFC is consistent” is consistent“

The latter implies that ZFC+”ZFC is consistent” proves “ZFC + “ZFC is consistent” is consistent“, but by Gödel’s theorem this can only happen if ZFC+”ZFC is consistent” is in fact consistent, i.e. if ZFC proves “ZFC is inconsistent”.

I cannot believe I didn’t know this strange fact before. There seems to be simply no way of ruling out that FZC proves its own inconsistency, unless you assume something stronger than ZFC being consistent, such as omega-consistency or, as mentioned earlier, that ZFC has a standard model (which is stronger than omega-consistency).

What are your thoughts on this? 🙂

Best,

Nicholas

A few days ago I was having a discussion with a colleague of mine, Tobias Fritz, about the relationship between undecidability of a decision problem and independence (say, from ZFC) of statements about particular instances of the problem. At some point, we were studying your paper and dwelled on the following statement:

“It follows that Z is a Turing machine for which the question of its behavior (whether or not it halts when run indefinitely) is equivalent to the consistency of ZFC. Therefore, just as ZFC cannot prove its own consistency (assuming ZFC is consistent), ZFC also cannot prove that Z will run forever.

This is interesting because, while the undecidability of the halting problem tells us that there cannot exist an algorithmic method for determining whether an arbitrary Turing machine loops or halts, Z is an example of a specific Turing machine whose behavior cannot be proven one way or the other using the foundation of modern mathematics.”

We see why ZFC cannot prove that Z will run forever, assuming consistency of ZFC, since this would violate Gödel’s 2nd Incompleteness Theorem. However, which argument do you have in mind when asserting that ZFC, if consistent, cannot prove that Z will _not_ run forever?

This would be equivalent to ZFC proving the formal statement “ZFC is inconsistent”. Whereas that would certainly be a perplexing circumstance, it is a fact that _if_ there exist at all consistent formal systems expressive enough to render themselves vulnerable to Gödel’s incompleteness results, _then_ there exist such consistent systems which prove their own inconsistency.

Indeed, starting with a consistent system S, the system T := S + “S is inconsistent” is also consistent, by Gödel’s theorem. Clearly, T proves “S is inconsistent”. But T also proves the implication “if S is inconsistent, then T is inconsistent”. Therefore, T proves “T is inconsistent”, even though it is in fact consistent.

Is there some argument (necessarily specific to ZFC) which shows that, if ZFC is consistent, then ZFC cannot prove its own inconsistency?

I can think of two slightly different arguments that seem to work if one is willing to believe in certain non-finitistic constructs.

1. For example, if there exists a so-called _standard_ model of ZFC (i.e. a model in which the elements of the universe are actual sets, and the interpretation of the membership relation is the actual membership relation), then there exists, by way of the Mostowski collapse, a standard _transitive_ model, and in such a model the interpretations of finitistic objects (I’m using this term somewhat casually) coincide with the actual, ‘real’ objects. In particular, if the formal statement “ZFC is inconsistent” is true in such a model, then the object in the model that witnesses (internally) the existence of a deduction from ZFC of a contradiction _is_ actually (externally) a deduction from ZFC of a contradiction, and so ZFC is inconsistent. Hence, if there is a standard model of ZFC, it is impossible that ZFC proves its own inconsistency.

A ‘finitist’ would not be content with such an argument; (s)he would only agree, that the above demonstrates that ZFC proves the formal statement “if there is a standard model of ZFC, then ZFC does not prove the formal statement “ZFC is inconsistent” “ (note that there are now two levels of formality).

[It deserves to be mentioned that is an intricate matter to settle the existence of a standard model. In fact, if ZFC has a standard model, then one cannot prove the formal statement “if ZFC has a model, then ZFC has a standard model”! The reason is that, assuming the existence of a standard model, one can show that some level in the constructible hierarchy is a standard transitive model, and in the lowest such level the interpretation of the implication is false.]

(CONTINUES BELOW)

]]>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.