On $NP \cap coNP$ proof complexity generators
Jan Krajicek
TL;DR
The paper studies a Σ^p_2 search problem ${\rm DD}_P$ derived from a $P$-proof of a disjunction with disjoint atoms, and investigates its solvability in the constant-round student-teacher model ${\rm ST}[{\mathcal P}, O(1)]$. It proposes a model-theoretic approach, via extensions of bounded-arithmetic models, to derive lower bounds for ${\rm DD}_P$ and connect ${\rm ST}$-hardness to the separation ${\rm NP} \neq {\rm coNP}$ under a plausible extension hypothesis. The main result shows that if the extension problem has an affirmative solution, then Hypothesis (ST) implies ${\rm NP} \neq {\rm coNP}$, and this yields a stronger consequence that strong proof systems lack a feasible disjunction property for disjoint disjunctions. The work links proof complexity, bounded arithmetic, and model theory and outlines a path to unconditional lower bounds by further investigating model-theoretic extensions of bounded theories.
Abstract
Motivated by the theory of proof complexity generators we consider the following $Σ^p_2$ search problem $\mbox{DD}_P$ determined by a propositional proof system $P$: given a $P$-proof $π$ of a disjunction $\bigvee_i α_i$, no two $α_i$ having an atom in common, find $i$ such that $α_i \in \mbox{TAUT}$. We formulate a hypothesis (ST) that for some strong proof system $P$ the problem $\mbox{DD}_P$ is not solvable in the student-teacher model with a p-time student and a constant number of rounds. The hypothesis follows from the existence of hard one-way permutations. We prove, using a model-theoretic assumption, that (ST) implies $NP \neq coNP$. The assumption concerns the existence of extensions of models of a bounded arithmetic theory and it is open at present if it holds.