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

[Lew Gordeew]

Just adding my 5 cents to Hermann's exhaustive response to Alasdair's  
reply of Oct. 11, 2016.

There is no contradiction. The APAL paper in question deals with  
Hilbert-style proof system IL, whereas our construction yields daglike  
natural deductions (ND). The corresponding daglike ND provablity is  
more sophisticated and the correlated dag-to-tree unfolding usually  
requires exponential growth in size. We don't see how to pass from our  
polysize daglike ND to a polysize proof in IL or any other  
Hilbert-Frege-style system (w.r.t. intuitionistic and/or minimal logic).

Best,
LG

---------------------------------------
From: Alasdair Urquhart <urquhart at cs.toronto.edu>
Date: Tue, Oct 11, 2016 at 10:34 PM
Subject: [FOM]  Proof-theoretic proof of NP=PSPACE?
To: Foundations of Mathematics <fom at cs.nyu.edu>


I think there must be an error in this proof somewhere.
Pavel Hrubes proved an exponential lower bound on
proofs in the intuitionistic propositional calculus
(Annals of Pure and Applied Logic, Volume 146 (2007),
pp. 72-90.  There is an efficient translation from
intuitionistic logic into minimal logic, so the
claimed result contradicts the theorem of Hrubes.