# Consequences of a $p$-optimal proof system for $\operatorname{TAUT}$

I'm reading a paper 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). 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?

See the Wikipedia article for propositional proof complexity. 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", J. Symbolic Logic, 54(3), (1989), pp. 1063-1079.

Yijia Chen and Jörg Flum, "On optimal proof systems and logics for PTIME", 2010.

Zenon Sadowski, "On an optimal propositional proof system and the structure of easy subsets of TAUT", 2002.