Graph explorer

NP vs PSPACE

We present a proof of the conjecture $\mathcal{NP}$ = $\mathcal{PSPACE}$ by showing that arbitrary tautologies of Johansson's minimal propositional logic admit "small" polynomial-size dag-like natural deductions in Prawitz's system for minimal propositional logic. These "small" deductions arise from standard "large"\ tree-like inputs by horizontal dag-like compression that is obtained by merging distinct nodes labeled with identical formulas occurring in horizontal sections of deductions involved. The underlying "geometric" idea: if the height, $h\left( \partial \right) $ , and the total number of distinct formulas, $ϕ\left( \partial \right) $ , of a given tree-like deduction $\partial$ of a minimal tautology $ρ$ are both polynomial in the length of $ρ$, $\left| ρ\right|$, then the size of the horizontal dag-like compression is at most $h\left( \partial \right) \times ϕ\left( \partial \right) $, and hence polynomial in $\left| ρ\right|$. The attached proof is due to the first author, but it was the second author who proposed an initial idea to attack a weaker conjecture $\mathcal{NP}= \mathcal{\mathit{co}NP}$ by reductions in diverse natural