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

[Richard Zach]

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