[FOM] On lengths of proofs

[Joe Shipman]

Work in a finitely axiomatizable Set/class theory like NBG. Consider a different finite axiomatization of sets and classes A. We have a dichotomy:

If any axiom Phi of A is not a theorem of NBG, then there are arbitrarily large blowups in proof length when you move from Phi to NBG (consider statements of the form “Phi, or there is no proof of a contradiction in NBG of length < fastgrowingfunction(n)” ).

If NBG proves all the axioms of A, then there is only a constant additive blowup in proof length, not even a linear blowup with constant >1.

Thus, you can’t have an alternative axiomatization with a “quadratic proof blowup”.

On the other hand, consider a non-finitely-axiomatizable theory like ZFC. Then an alternative theory could have blowups bounded by a computable function but superlinear, because ZFC proving that the theory is relatively consistent with ZFC doesn’t entail that ZFC has blowup-free proofs, just that you can avoid blowups by settling for ZFC proofs of “ZFC proves X” instead of ZFC proofs of X.

A contrived example of such a system would be ZFC augmented by the axiom scheme “ZFC has no contradictions of length < f(n)” for some function n of moderate growth rate.

My question: Is a non-contrived (that is, proposed for doing math rather than to prove a metamathematical point) example known of an alternative foundational setup which (assuming Con(ZFC)) provably has a proof length blowup of moderate size (superlinear, but provably recursive — an extremely generous definition of “moderate”) when you move from it to ZFC?

— JS

Sent from my iPhone