[FOM] Proof-theoretic proof of NP=PSPACE?
lew.gordeew at uni-tuebingen.de
Mon Oct 17 16:40:05 EDT 2016
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).
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).
>> 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
More information about the FOM