<p>See the Wikipedia article for <a href="http://en.wikipedia.org/wiki/Propositional_proof_system" rel="noreferrer">propositional proof complexity</a>. p-simulation is similar to reductions between complexity classes. Existence of a p-optimal proof system is a well-known open problem in proof complexity.</p>

<p>It is statement 7 in Krajicek and Pudlak 1989. See page 1066 and 1067 for a list of statements implied/implying it. There are more statements that you can find by Googling.</p>

<p>There are experts who conjecture that extended Frege is an p-optimal proof system. Existence of a p-optimal proof system is a weaker statement than existence of a super proof system (which is equivalent to $\mathsf{NP}=\mathsf{coNP}$). </p>

<p>Jan Krajicek and P. Pudlak, "<a href="http://www.karlin.mff.cuni.cz/~krajicek/scan10.pdf" rel="noreferrer">Propositional Proof Systems, the Consistency of First Order Theories and the Complexity of Computations</a>", J. Symbolic Logic, 54(3), (1989), pp. 1063-1079.</p>

<p>Yijia Chen and Jörg Flum, "<a href="http://eccc.hpi-web.de/report/2010/008/" rel="noreferrer">On optimal proof systems and logics for PTIME</a>", 2010.</p>

<p>Zenon Sadowski, "<a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.4934" rel="noreferrer">On an optimal propositional proof system and the structure of easy subsets of TAUT</a>", 2002.</p>

CC BY-SA 3.0
2012-11-09T05:50:35.073Z
2012-11-09T06:14:35.007Z
2012-11-09T06:14:35.007Z
Kaveh
<p>I'm reading a <a href="http://eccc.hpi-web.de/report/2010/008/download/" rel="nofollow noreferrer">paper</a> which shows the result:</p>

<p>$(1)$ There is a $p$-optimal proof system for $\operatorname{TAUT}$. $\Leftrightarrow$ 
$(2)$ $L_{\leq}$ is a $P$-bounded logic for $P$.</p>

<p>Both $(1)$ and $(2)$ are unproven Conjectures.</p>

<p>A proof system for a problem $Q \subseteq \Sigma^*$ is a surjective function $P: \Sigma^* \to Q$ computable in polynomial time <a href="https://cstheory.stackexchange.com/questions/14088/intuition-behind-proof-systems">(see my other question)</a>. A proof system is $p$-optimal if for every proof system $P'$ for Q there is polynomial computable $T: \Sigma^* \to \Sigma^*$ such that f.a. $w \in \Sigma^*$</p>

<p>$$P(T(w)) = P'(w).$$</p>

<p>My first question is an intuition of the  $p$-optimal property: Does it mean that $P$ is minimal in a way? How does that work? Is it similar to the polynomial reduction one uses to show that a problem is $\operatorname{NP}$-hard?</p>

<p>A Logic $L$ is $P$-bounded for $P$ if there is a algorithm which decides the model relation $\mathcal{A} \models_{L} \varphi$ polynomial in $|\mathbb{A}|$. $L_{\leq}$ is variant of least fixed point logic (LFP). A formula $\varphi$ is $m$-invariant if for all structures $\mathcal{A}$ of size at most $m$ we have for all orderings $&lt;_1, &lt;_2$</p>

<p>$$(\mathcal{A},&lt;_1) \models_{LFP} \varphi \Leftrightarrow (\mathcal{A},&lt;_2) \models_{LFP} \varphi.$$ A formula in $L_{\leq}$ is satisfied on a structure $\mathcal{A}$ if it is at least $|\mathcal{A}|$-invariant and $(\mathcal{A},&lt;) \models_{LFP} \varphi$ for one $&lt;$.</p>

<p>I am interested in the consequences if $(1)$ was true (or even consequences if it was false?). $\operatorname{TAUT}$ is in $\mathrm{co}-\mathrm{NP}$ and $\operatorname{SAT}$ is in $\mathrm{NP}$. Is $(1) \Rightarrow \operatorname{NP} = 
co-\operatorname{NP}$ and why? Is okay to "mildly assume" that $\operatorname{NP} = co-\operatorname{NP}$ is not true?</p>

<cc.complexity-theory><complexity-classes><descriptive-complexity><proof-complexity><conditional-results>
Consequences of a $p$-optimal proof system for $\operatorname{TAUT}$
Joachim
# Consequences of a $p$-optimal proof system for $\operatorname{TAUT}$

(Asked by: username_0 on 2012-11-08)

I'm reading a [paper](http://eccc.hpi-web.de/report/2010/008/download/) which shows the result:

$(1)$ There is a $p$-optimal proof system for $\operatorname{TAUT}$. $\Leftrightarrow$
$(2)$ $L\_{\leq}$ is a $P$-bounded logic for $P$.

Both $(1)$ and $(2)$ are unproven Conjectures.

A proof system for a problem $Q \subseteq \Sigma^\*$ is a surjective function $P: \Sigma^\* \to Q$ computable in polynomial time [(see my other question)](https://cstheory.stackexchange.com/questions/14088/intuition-behind-proof-systems). A proof system is $p$-optimal if for every proof system $P'$ for Q there is polynomial computable $T: \Sigma^\* \to \Sigma^\*$ such that f.a. $w \in \Sigma^\*$

$$P(T(w)) = P'(w).$$

My first question is an intuition of the $p$-optimal property: Does it mean that $P$ is minimal in a way? How does that work? Is it similar to the polynomial reduction one uses to show that a problem is $\operatorname{NP}$-hard?

A Logic $L$ is $P$-bounded for $P$ if there is a algorithm which decides the model relation $\mathcal{A} \models\_{L} \varphi$ polynomial in $|\mathbb{A}|$. $L\_{\leq}$ is variant of least fixed point logic (LFP). A formula $\varphi$ is $m$-invariant if for all structures $\mathcal{A}$ of size at most $m$ we have for all orderings $<\_1, <\_2$

$$(\mathcal{A},<\_1) \models\_{LFP} \varphi \Leftrightarrow (\mathcal{A},<\_2) \models\_{LFP} \varphi.$$ A formula in $L\_{\leq}$ is satisfied on a structure $\mathcal{A}$ if it is at least $|\mathcal{A}|$-invariant and $(\mathcal{A},<) \models\_{LFP} \varphi$ for one $<$.

I am interested in the consequences if $(1)$ was true (or even consequences if it was false?). $\operatorname{TAUT}$ is in $\mathrm{co}-\mathrm{NP}$ and $\operatorname{SAT}$ is in $\mathrm{NP}$. Is $(1) \Rightarrow \operatorname{NP} =
co-\operatorname{NP}$ and why? Is okay to "mildly assume" that $\operatorname{NP} = co-\operatorname{NP}$ is not true?

**Tags:** cc.complexity-theory, complexity-classes, descriptive-complexity, proof-complexity, conditional-results

---

## 1 answers

### Answer by username_1 on 2012-11-09. Score: 5 | Accepted answer

See the Wikipedia article for [propositional proof complexity](http://en.wikipedia.org/wiki/Propositional_proof_system). p-simulation is similar to reductions between complexity classes. Existence of a p-optimal proof system is a well-known open problem in proof complexity.

It is statement 7 in Krajicek and Pudlak 1989. See page 1066 and 1067 for a list of statements implied/implying it. There are more statements that you can find by Googling.

There are experts who conjecture that extended Frege is an p-optimal proof system. Existence of a p-optimal proof system is a weaker statement than existence of a super proof system (which is equivalent to $\mathsf{NP}=\mathsf{coNP}$).

Jan Krajicek and P. Pudlak, "[Propositional Proof Systems, the Consistency of First Order Theories and the Complexity of Computations](http://www.karlin.mff.cuni.cz/~krajicek/scan10.pdf)", J. Symbolic Logic, 54(3), (1989), pp. 1063-1079.

Yijia Chen and Jörg Flum, "[On optimal proof systems and logics for PTIME](http://eccc.hpi-web.de/report/2010/008/)", 2010.

Zenon Sadowski, "[On an optimal propositional proof system and the structure of easy subsets of TAUT](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.4934)", 2002.


---

