Proof complexity and lower bounds

Question

One way to prove NP$\neq$ coNP is to show that for every propositional proof system $f$ computable in polynomial time, there exists a family of tautologies for which $f$ requires super polynomial proof lengths (w.r.t the length of tautology being proven). Results like that of Haken and Ajtai fix a propositional proof system and prove that a certain family (PHP in this case) requires super polynomial length proofs.

My Question: Are there results which do not fix a proof system and show, possibly very weak, but non-trivial lower bounds on proof length? For Example: Are there results showing that for every propositional proof system, there exists a family of tautologies which requires superlinear proof lengths?

Answer 1

The statement is false for any polynomial time recognizable family of tautologies: the proof system will simply check if the formula is one of them and accept if it is. Proof length of them will be O(1). So I don't think any explicit example is known.

Recall that we don't even know if SAT $\notin$ DTime(O(n)) so we also don't know if SAT$\notin$ coNTime(O(n)) which is equivalent to your question TAUT $\notin$ NTime(O(n)) and follows from a positive answer to your question.

On the other hand, if NP is not equal to coNP, then the family consisting of all tautologies has super polynomial length in any efficient proof system.

Part of what people try to do in prof complexity is to rule out interesting classes of algorithms. A lower bound in a proof system implies a lower bound for all (co-nondeterministic) algorithms whose correctness can be efficiently proven in the proof system (if we can formalize and prove the correctness of an algorithm for SAT in a proof system we can consider its failing execution to find a satisfying assignment as proofs of the tautologihood).