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

Question

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?

Answer 1

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.