<p>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.</p>

<p>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.</p>

<p>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.</p>

<p>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).</p>

CC BY-SA 3.0
2014-01-03T05:24:14.950Z
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?
Karteek
CC BY-SA 3.0
2014-01-04T02:54:15.443Z
@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.
Kaveh
CC BY-SA 3.0
2014-01-02T22:40:39.430Z
2014-01-03T03:55:06.160Z
2014-01-03T03:55:06.160Z
Kaveh
<p>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 <a href="http://www.sciencedirect.com/science/article/pii/0304397585901446">Haken</a> and <a href="http://link.springer.com/article/10.1007/BF01302964">Ajtai</a> fix a propositional proof system and prove that a certain family (PHP in this case) requires super polynomial length proofs.</p>

<p>My Question:
Are there results which <strong>do not fix</strong> 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?</p>

<cc.complexity-theory><proof-complexity>
Proof complexity and lower bounds
Karteek
# Proof complexity and lower bounds

(Asked by: username_0 on 2014-01-02)

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](http://www.sciencedirect.com/science/article/pii/0304397585901446) and [Ajtai](http://link.springer.com/article/10.1007/BF01302964) 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?

**Tags:** cc.complexity-theory, proof-complexity


---

## 1 answers

### Answer by username_1 on 2014-01-02. Score: 3 | Accepted answer

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

> **Comments:**
> **username_0**: 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?  
> **username_1**: @username_0, 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.  

---

