[FOM] Proof-theoretic proof of NP=PSPACE?
rzach at ucalgary.ca
Tue Oct 18 12:43:08 EDT 2016
Reckow's thesis is available here:
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
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).
>> 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
More information about the FOM