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

Edward Hermann Haeusler edward.haeusler at gmail.com
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,


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>

More information about the FOM mailing list