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

[Lew Gordeew]

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