NP vs PSPACE
CoRR๏ผ2016๏ผ
Abstract
We present a proof of the conjecture ๐ฉ๐ซ = ๐ซ๐ฎ๐ซ๐๐โฐ 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( โ) , and the total number of distinct formulas, ฯ( โ) , of a given tree-like deduction โ of a minimal tautology ฯ are both polynomial in the length of ฯ, | ฯ|, then the size of the horizontal dag-like compression is at most h( โ) รฯ( โ), and hence polynomial in | ฯ|. 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 ๐ฉ๐ซ= ๐๐๐ฉ๐ซ by reductions in diverse natural deduction formalisms for propositional logic. That idea included interactive use of minimal, intuitionistic and classical formalisms, so its practical implementation was too involved. The attached proof of ๐ฉ๐ซ=๐ซ๐ฎ๐ซ๐๐โฐ runs inside the natural deduction interpretation of Hudelmaier's cutfree sequent calculus for minimal logic.
MoreTranslated text
AI Read Science
Must-Reading Tree
Example
![](https://originalfileserver.aminer.cn/sys/aminer/pubs/mrt_preview.jpeg)
Generate MRT to find the research sequence of this paper
Chat Paper
Summary is being generated by the instructions you defined