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

[Lew Gordeew]

But we're talking about special dag-like natural deductions whose  
(novel) graph-theoretic notion of provability is more sophisticated  
than plain tree-like one. So that old result does not apply here  
(whether intuitionistic or minimal).

Best,
LG

Zitat von Alasdair Urquhart <urquhart at cs.toronto.edu>:

> 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.
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom