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?


1 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).

  • 1
    $\begingroup$ What exactly do you mean by "lower bounds to algorithms"? And by "algorithms whose correctness can be efficiently proven in the proof system", do you mean in some related theory? $\endgroup$
    – Karteek
    Commented Jan 3, 2014 at 5:24
  • $\begingroup$ @Karteek, I mean lowerbounds on the length of their execution history, which imply lowerbounds on their running times. I mean in propositional proof systems, but often there is some nice related theory where we can prove the correctness and then perform a propositional translation to obtain a proof in the propositional proof system. $\endgroup$
    – Kaveh
    Commented Jan 4, 2014 at 2:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.