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?
