[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