[FOM] Proof-theoretic proof of NP=PSPACE?
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