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

[Richard Zach]

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>