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

Lew Gordeew lew.gordeew at uni-tuebingen.de
Wed Oct 19 05:09:08 EDT 2016

```Sorry, I was confused by your reference to ZFC and PA. No, at the
moment I have no idea how to essentially improve upper bound degree
270. It's even harder to make sound predictions on lower bounds.

Best,
LG

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

> I meant to ask if you had any conjectures on lower and upper bounds
> for the degree which Edward pointed out is bounded above by 270, not
> on lower and upper bounds on the logical strength of the systems
> necessary, sorry if that wasn't clear!
>
> -- JS
>
> Sent from my iPhone
>
>> On Oct 18, 2016, at 5:15 PM, Lew Gordeew
>> <lew.gordeew at uni-tuebingen.de> wrote:
>>
>> 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 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
>>

```