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

Lew Gordeew lew.gordeew at uni-tuebingen.de
Wed Oct 19 14:40:04 EDT 2016

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

```