[FOM] Proof-theoretic proof of NP=PSPACE?
lew.gordeew at uni-tuebingen.de
Fri Oct 14 04:00:09 EDT 2016
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).
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.
More information about the FOM