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

Tue Oct 18 07:06:12 EDT 2016

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/2e2df122/attachment-0001.html>