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

[Richard Zach]

Reckow's thesis is available here: 
https://www.cs.toronto.edu/~sacook/homepage/reckhow_thesis.pdf

If I understand the dag-like ND proofs used in the paper correctly, it's 
simply a matter of allowing a formula in a proof to be used more than 
once as a premise of a rule. So such a proof can be written as a 
sequence of formulas (eg, Lemmon style natural deduction)?  In any case, 
Reckow's result applies to dag-like ND systems, not just tree ND systems 
(afaict).

-R

On 2016-10-17 12:30 PM, Alasdair Urquhart wrote:
> 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.
>

-- 
Richard Zach ...... http://www.ucalgary.ca/rzach/
Professor,             Department  of  Philosophy
University of Calgary, Calgary AB T2N 1N4, Canada