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

[Lew Gordeew]

Zitat von Richard Zach <rzach at ucalgary.ca>:

>> On the other hand, the use of Lemmon Style ND does not allow us to  
>> conclude that the existent lower bound for Frege systems directly  
>> apply to ND.   A dag-like proof, even in Lemmon Style,  cannot  
>> simply indicate that you  are using a formula more than once. Each  
>> formula has it is own natural dependency set of formulas. We cannot  
>> collapse equal formulas derived  from different set of formulas  
>> without taking care of annotating the new dependency, if we take  
>> this control seriously, we end up in a dag-like proof as defined in  
>> our article, and having to adjust the annotations to polynomial  
>> size and so on.
>>
> Ah, so I'm wrong then in thinking that your "dag-like proofs" merely  
> allow a premise to be used more than once.  If it is something else  
> (something that can't be represented by a sequence of sequents or  
> Lemmon-style as a sequence of formulas  with dependencies labelled  
> by line number), then you should probably explain in your paper what  
> that proof system is. I don't understand Definition 6; so it's not  
> obvious to me that it defines a sound and complete proof system. An  
> example would help. If in your soundness proof you translate a  
> dag-like proof into an exponentially longer linear proof, that might  
> might persuade your doubters that your system it is not susceptible  
> to Reckow's result.

Definition 6 presents a new kind of dag-like proof system for minimal  
logic that generalizes, while including, Prawitz's (tree-like!) ND. It  
is not a sort of Frege system as in Reckow's paper. The completeness  
follows immediately from that of Prawitz's ND (see Claim 3, Lemma 5  
and a passage right after Definition 6). Example 13 shows a simple  
dag-like deduction d^c that is obtained by compressing standard  
tree-like deduction d. More sophisicated examples are presented in  
Appendices B, C. The soundness is not obvious. It is proved by  
dag-to-tree unfolding that reduces dag-like provability under  
consideration to standard provability in Prawitz's tree-like ND (see  
Corollary 18). This translation is obviously exponential in size (in  
the general case). You can compare it with analogous (also  
exponential) dag-to-tree unfolding in term algebra with respect to  
standard tree-like form of a given algebraic term t and its minimal  
dag-like compression t^c that is obtained by merging all pairs of  
nodes labeled with identical subterms.

Best,
LG