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

[Lew Gordeew]

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