New formally undecidable propositions: non-trivial lower bounds on proof complexity and related theorems

AbstractWithin a formal theory T where a ⊥-rule is provably valid and Gödel's second incompleteness theorem holds, it is not possible to prove any non-trivial lower bound LBT on proof complexity. Most calculi currently used in formalizing proofs are of this type. We give many sets of formulas where non-trivial lower bounds LBT are assumed in a simple way. Thus we have a new large class of formally undecidable mathematical propositions. To this we add the well-known theorems of recursive undecidability and proof speed-ups of T as well as examples resulting from proof-theoretic Π10-uniformity. Our examples also show that the formalistic goal of computing the “whole accessible mathematical world” is not attainable in a mathematically satisfactory way: the above mentioned LBT′({Fn}) with Fn provable in T can only be formally decided using known methods in extensions T′ of T if almost all Fn are assumed as axioms in T′. Such a completion T′ practically amounts to listing and not proving theorems. Finally we see that Cook's thesis NP≠P implies the existence of {Fn}⊆ TAUT having a lower bound LBT({Fn}) of an order of growth comparable to that in our examples. This is new evidence for the validity of Cook's conjecture. A proof of this conjecture has to overcome the proof-theoretic difficulty that if validity ⊨ is replaced by provability ⊢T in T, then this NP≠P-variant cannot be proved in T