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

[Joe Shipman]

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
>