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

[Alasdair Urquhart]

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).
>
> 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.