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

[Joe Shipman]

Professor Gordeev,

For a general PSPACE-complete problem like QBF,

1) what is the degree of the best polynomial bound f(n) you have on the size of the compressed NP proof of the truth or falsity of the size-n instance of QBF?
2) given the compressed NP proof of size m=f(n), what is the degree of the best polynomial bound g(m) of the time complexity of verifying it as a function of m?

Of course, this is equivalent to having a proof of size h(n)=g(f(n)) with deg h = (deg g * deg f), that is verifiable by an algorithm with time complexity O(1 + epsilon), the proof being the "trace" of the previous verification algorithm.

-- JS

Sent from my iPhone

> On Oct 17, 2016, at 4:40 PM, Lew Gordeew <lew.gordeew at uni-tuebingen.de> wrote:
> 
> 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
> 
> 
> 
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom