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?
- 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?
- 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?