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

Lew Gordeew lew.gordeew at uni-tuebingen.de
Tue Oct 18 17:15:20 EDT 2016

```I suppose that the whole decidability proof is formalizable in H.
Friedman's weak arithmetic EFA (whose proof theoretic strength is
omega^3). Certainly so are all constructions and corresponding
properties and estimates exposed in the paper. It remains to formalize
in EFA the underlying QBF connections.

Best,
LG

Zitat von Joe Shipman <joeshipman at aol.com>:

> 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
>> 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

```