We show that arbitrary tautologies of Johansson’s minimal propositional logic
are provable by “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 for-
mulas, φ (∂), 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 ∂ c is at most
h (∂)×φ (∂), and hence polynomial in |ρ|. That minimal tautologies ρ are provable by tree-
like natural deductions ∂ with |ρ|-polynomial h (∂) and φ (∂) follows via embedding from
Hudelmaier’s result that there are analogous sequent calculus deductions of sequent ⇒ρ.
The notion of dag-like provability involved is more sophisticated than Prawitz’s tree-like
one and its complexity is not clear yet. Our approach nevertheless provides a convergent
sequence of NP lower approximations of PSPACE-complete validity of minimal logic (Sav-
itch in J Comput Syst Sci 4(2):177–192, 1970); Statman in Theor Comput Sci 9(1):67–72,
1979; Svejdar in Arch Math Log 42(7):711–716, 2003).

EB00000003910K

Available

• Proof Compression and NP Versus PSPACE