On $NP\cap coNP$ proof complexity generators

Abstract

Motivated by the theory of proof complexity generators we consider the following ${\Sigma }_2^p$ search problem $\mbox{DD}_P$ determined by a propositional proof system $P$: given a $P$-proof $\pi$ of a disjunction ${\bigvee }_i{\alpha }_i$, no two ${\alpha }_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\ne coNP$. The assumption concerns the existence of extensions of models of a bounded arithmetic theory and it is open at present if it holds.