On $NP \cap coNP$ proof complexity generators

TL;DR

This paper explores the complexity of a proof system-based search problem, linking its solvability to major complexity class separations and hypotheses about proof systems and one-way permutations.

Contribution

It introduces a new $ ext{NP} igcap ext{coNP}$ proof complexity generator problem and connects its difficulty to the existence of hard one-way permutations and complexity class separations.

Findings

Hypothesis (ST) implies NP ≠ coNP under certain model-theoretic assumptions.

The problem $ ext{DD}_P$ relates to proof complexity and proof systems.

The hypothesis follows from the existence of hard one-way permutations.

Abstract

Motivated by the theory of proof complexity generators we consider the following $\Sigma^p_2$ 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 $\alpha_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.