On $NP \cap coNP$ proof complexity generators
This work addresses a foundational problem in computational complexity theory, specifically the NP vs coNP question, but it is incremental as it relies on an unproven assumption.
The paper tackles the problem of linking proof complexity generators to the NP vs coNP question by formulating a hypothesis (ST) about the unsolvability of a specific search problem in a student-teacher model, which implies NP ≠ coNP under a model-theoretic assumption.
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.