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

[Joe Shipman]

Thank you!

So a corollary is that there is a ZFC proof of the truth or falsity of any n-quantifier QBF sentence of size O(n^270), and similarly for PA-proofs because your arguments appear to be formalizable in PA. Do you have any conjectures for a lower bound or a better upper bound?

-- JS

Sent from my iPhone

> On Oct 18, 2016, at 7:06 AM, Edward Hermann Haeusler <edward.haeusler at gmail.com> wrote:
> 
> Dear prof. Shipman,
> 
> 
> 
> Thank you very much for the attention on our article, here it goes the answers for your questions. Note that these are rough upper-bounds, the best ones we cannot say yet.
> 
> 1- Consider a QBF formula A=Qmy_m...Q1y_1B(y_1,...,y_m) in prenex form with only \bot and --> occurring in B. Svejdar reduction produces a propositional formula of size 8*len(B)*m that is intuitionistically valid, iff, A is valid. 
> Eliminate \bot to get a purely minimal logic formula A^{\star} of size
> (8*len(B)*m)^2. This formula is a minimal tautology, iff, A is valid. Observe that A^{\star} has is a purely implicational formula. 
> 
> 2- According to our corollary 12, if A^{\star} is valid, then it has a dag-like proof of size (number of vertexes) O( len(A^{\star})^5). In terms of A=Qmy_m...Q1y_1B(y_1,...,y_m),  itself,  this  dag-like proof is of size O(m^10*len(B)^{10}). The encoding of any dag-like proof G results in a string of size O(||G||^3), lemma 21, in the article. Thus, the size of the dag-like encoded proof is of size O(m^{30}*len(B)^{30}). Finally, a naive algorithm to verify that a dag-like proof of $A^{\star}$, the minimal implicational formula that it is its conclusion,  runs in time  O(||G||^{9}) , where G is the size of the dag-like proof. 
> 
> As you see for any QBF formula A of size n, there is a dag-like proof of size n^30 that can be verified in time (n^{30})^9.   We hope this answer your question. Of course, the degree 270 is quite a big one !!!  It can be reduced on the basis of what is detailed in the article, however, this is the easiest upper-bound to show from what is in the article. This is may not be the best. There is much work to do in this direction...
> 
> 
> 
> All the Best, 
> 
> 
> 
> Hermann 
> 
> 
> Em 18/10/2016 2:42 AM, "Joe Shipman" <joeshipman at aol.com> escreveu:
>> 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20161018/c4347539/attachment-0001.html>