# Finding a lower bound on possible derivations for a contradiction within a theory like Zermelo–Fraenkel set theory

Not a logician here, so please bear with me and please correct any possible misconceptions I may have about this subject.

Gödel’s second incompleteness theorem implies that the consistency of say Zermelo–Fraenkel set theory cannot be derived within Zermelo–Fraenkel set theory. Furthermore Zermelo–Fraenkel set theory may turn out to be inconsistent. And in this case, we may be easily able to find this out by simply deriving a contradiction within it.

However, even if Zermelo–Fraenkel set theory turns out to be inconsistent, it may still be possible that the nearest contradiction from its axioms is so far away that we may actually never encounter it. Assuming its inconsistency, we may consider the least length of derivations of contradictions in it. Maybe it’s larger than the number of grains of sand in the observable universe?

1. Is it, in principle, possible to establish a lower bound on the lengths of possible derivations of contradictions in formal theories like Zermelo–Fraenkel set theory? Or has this been shown to be impossible, as it would seem typical of the world of higher logic?
2. If Zermelo–Fraenkel set theory turns out to be inconsistent, but with the length of the smallest derivations of contradictions in it being larger than the number of grains of sand in the observable universe, would we still throw all our higher mathematics relying on axiomatic set theory into the garbage can or is there a justification of keeping it by virtue of all of it still being far off the lands of contradiction?
• $(1)$ Goedel's result show that we cannot prove the consistency of a sufficient strong theory within the theory itself. We could use a stronger theory to show this, but then we would run into a follow-problem. Gentzen's proof avoided this trap, but we cannot prove transifnite induction to be consistent either. $(2)$ If ZFC can derive some statement AND its negation, it is already inconsistent. This need not be a long statement, Russel's discovery was a big surprise and forced mathematicians to modify the set theory. – Peter Jul 13 at 11:31
• $(3)$ Inconsistency does not at all mean that mathematics breaks down then. It just means that the particular formal system is not suitable. But this does not affect the truth of statements like $1+1=2$. If a statement is true with respect to every interpretation , it can be proven (and its negation disproven). In particular, mathematics is not suddenly utterly wrong just because of a flaw in a formal system. $(4)$ There is no guarantee for consistency, but considering the time no issue has been found, we can be quite sure that ZFC is consistent. – Peter Jul 13 at 11:36
• $(5)$ Hilbert's dream was a formal system being able to prove all true and to disprove all false theorems. Goedel and Turing were the most important persons involved in the discovery that this is unfortunately not possible. And Goedel's second theorem seems to make it worse. But this is not so dramtical as it appears. The impact on the math we need for "practical purposes" is almost $0$. – Peter Jul 13 at 11:40

So there are two scenarios to consider here.

# Case I: The make-believe inconsistency

We know that $$\sf ZFC$$ does not prove its own consistency, as you said, so we can try and study the theory $$\sf ZFC+\lnot\operatorname{Con}(ZFC)$$, which may very well be consistent itself. In this case situation the internal inconsistency of $$\sf ZFC$$ is coded by a non-standard integer. It could be that the proof is "that long", or maybe we needed to refer to non-standard inference rules, or involve some other statement that has non-standard length.

In this case the inconsistency is not only larger than any number you can fit into the universe, it is in fact larger than any number "we in the meta-theory" even consider to be a natural number.

The reason is that our coding of first-order logic is so robust that for the standard integers it is the same between the theory and its meta-theory. That means that if the theory thinks that $$\sf ZFC$$ is consistent, then no standard integer can code a proof of contradiction, even in models of theories that disagree on said consistency of $$\sf ZFC$$.

# Case II: The possible grim reality

But maybe $$\sf ZFC$$ is really inconsistent. What a pity. Of course, we don't know that for sure, and so we can't say maybe it's just the Axiom of Infinity, maybe it's Power Set, or maybe it's Replacement. Maybe it's already the arithmetic theories that are inconsistent, who knows. Maybe the issue is not the length of the proof, but the axioms that are used there. Maybe the inconsistency is a proof of just nine steps, but it requires us to use $$\Sigma_n$$-Replacement axioms for $$n$$ so preposterously large that the axiom itself is longer than the universe.

So it's hard to say exactly what's going on. But we still have some "good" or at least "known" upper bounds.

Scott Aaronson and Adam Yedidia came up with a Turing machine (using what is probably the most basic version of the idea) with just under $$8000$$ states which halts if $$\sf ZFC$$ is inconsistent. This was ultimately improved to $$1919$$ states. This means that if we consider the Busy Beaver number, $${\rm BB}(1919)$$, it is an upper bound, modulo your choice of coding.

But that being said, $${\rm BB}(5)$$ is already insanely large, and to say that the growth rate of the Busy Beaver is fast would be a severe understatement.

• Wouldn’t a Turing machine halting if Zermelo–Fraenkel is inconsistent provide itself an upper bound on the least length of derivations of contradictions? – Or how does this give a lower bound? – k.stm Jul 13 at 11:47
• Err, yes. You're right. :-) – Asaf Karagila Jul 13 at 11:49
• But therefore, it is possible to verify that ZFC is consistant, by just checking all the proofs of length at most $BB(1919)$ ! Why is it not in contradiction with Gödel’s second incompletness theorem ? – QuinnLesquimau Jul 13 at 19:50
• @QuinnLesquimau: First of all, that number is unimaginably large. But a different way of reading the theorem of Aaronson and Yedidia is that ZFC just can't decide the exact value of this number. So even if you "could verify everything up to that number", which number is that? – Asaf Karagila Jul 13 at 20:05
• @spaceisdarkgreen: That's one hell of a whoopsie! Thanks. :-) – Asaf Karagila Jul 13 at 20:09