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

Richard Zach rzach at ucalgary.ca
Wed Oct 19 13:15:09 EDT 2016

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

More information about the FOM mailing list