[FOM] Proof-theoretic proof of NP=PSPACE?
urquhart at cs.toronto.edu
Mon Oct 17 14:30:19 EDT 2016
It's an old result that natural deduction systems for the
classical propositional calculus do not provide more than
a polynomial speedup over Hilbert-style proof systems.
This result already appears in the doctoral dissertation
of Robert Reckhow (U of Toronto 1975); it adapts immediately
to minimal and intuitionistic logic.
Consequently, the claimed polynomial upper bound for the Prawitz
system of natural deduction also implies a polynomial upper
bound for minimal and hence intuitionistic propositional
logic in a Hilbert-style proof system. This contradicts
Hrubes's exponential lower bound.
On Fri, 14 Oct 2016, Lew Gordeew wrote:
> 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