An algebraical proof of the Danos-Regnier correctness criterion for proof nets

Abstract proof structures in multiplicative linear logic are graphs with some extra structure, and the class of proof nets is an inductively defined subclass. F. M'etayer established a correctness criterion by defining homology groups for proof structures, which characterize the proof nets among these ([Meta94a]). Using this result, we will present a completely algebraical proof of the traditional "acyclic and connected"-criterion, due to Danos and Regnier (see [DaRe89]). Main ingredient is a lemma stating that each proof structure satisfying the tree condition has an initial (as opposed to splitting) pair. 1 Preliminaries 1.1 MLL The set of formulas of multiplicative linear logic (MLL) is defined as the smallest set containing atoms p 1 ; p 2 ; : : : and their formal negations p ? 1 ; p ? 2 ; : : : , and closed under the binary operations\Omega (tensor) and & (par ). Unary negation is defined by the (commutative) De Morgan laws, i.e. (a\Omega b) ? := a ? & b ? , etc. The ..