# Proof complexity and lower bounds

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?

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.