Finite axiomatizability and length of proofs

[Joe Shipman]

In the following, all theories are assumed formalized in the standard first-order predicate calculus.

For a finitely axiomatizable theory T, consider the function LP_T(n)=the maximum, over provable sentences S of length n, of the length of the shortest proof of S.

This is clearly well-defined up to an additive constant for finite axiomatizations, because any two finite axiomatizations each take only a finite amount of work to prove the axioms of the other one.

For a theory that is not finitely axiomatizable, this is not a sensible measure, because of the tradeoff between computational complexity of the function to recognize axioms and the proof length function.

For non-contrived theories which are not recursive, the length-of-proofs function will have busy-beaver-like growth, so I only care about recursive theories here (not necessarily complete theories, just theories where there is an algorithm for theoremhood).

For recursive theories T, consider the function ND_A_T(n)=the maximum, over theorems of length n, of the shortest possible running time of the nondeterministic algorithm A successfully recognizing the theorem.

This is NOT well-defined without specifying the algorithm A.

Here’s my question:
Is there a recursive, finitely axiomatizable theory such that there exists a nondeterministic theorem-recognizing algorithm A such that LP_T(n) is not O(ND_A_T(n))?

In other words, is there a theory with some kind of generalized computable proof system which outperforms any system of the form “classical predicate calculus proof from a finite set of axioms“?

Before this can be answered, perhaps one should consider the special case of the propositional calculus. The set of tautologies can be generated by a finite set of axioms using a traditional proof scheme, and because we don’t know the status of the NP-coNP problem we don’t know whether all tautologies have polynomial length proofs, but I’m not asking whether they have polynomial length proofs, only if there’s any way to recognize tautologies which involves a nondeterministic algorithm essentially faster than “traditional proof from propositional axioms”.

— JS

Sent from my iPhone