# [FOM] Proof-theoretic proof of NP=PSPACE?

Richard Zach rzach at ucalgary.ca
Sat Oct 8 12:06:50 EDT 2016

```New on arXiv this week; has anyone read it/formed an opinion?

https://arxiv.org/abs/1609.09562

NP vs PSPACE
Lew Gordeev <https://arxiv.org/find/cs/1/au:+Gordeev_L/0/1/0/all/0/1>,
Edward Hermann Haeusler
<https://arxiv.org/find/cs/1/au:+Haeusler_E/0/1/0/all/0/1>
(Submitted on 30 Sep 2016)

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 =co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.

--
Richard Zach ...... http://www.ucalgary.ca/rzach/
Professor,             Department  of  Philosophy
University of Calgary, Calgary AB T2N 1N4, Canada

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20161008/edd64640/attachment-0001.html>
```