Implicit exchange in multiplicative proofnets (Q2719797)

Deductions in classical multiplicative linear logic are studied, with special attention paid to the number of exchange rules. In order to do this, the proofs in a system \(S\) with explicit exchange rule and the proofs in the system \(S^*\) where antecendent and succedent are (multi)sets and exchange becomes identity are considered. Main tool is the notion of proof structure. The basic idea is that standard proofnets may be regarded as orientable surfaces with boundary. Thus, a proof structure is a 2-complex where individual 2-cells correspond to the rules (their edges have side formulas and main formula as labels) and the way how they are glued together is linked to permutations. The topological structure of the resulting surface is used to study the behaviour of permutations. For example, the notion of rank is introduced (the number of generators in a homology group in dimension 1) and it is shown that the proof \(Q\) in \(S^*\) cannot be represented in \(S\) with less than \(\text{rk }Q/2\) exchange rules. The special case of one-sided sequents is considered. The author considers also the effect of cut-elimination on the rank. Links with the work of other authors considering various kinds of planar diagrams are discussed [e.g., \textit{M. Nagayama} and \textit{M. Okada}, Electronic Notes in Theoretical Computer Science 3, 11 p. (1996; Zbl 0909.03046), or \textit{G. Bellin} and \textit{A. Fleury}, Arch. Math. Log. 37, 309-325 (1998; Zbl 0905.03037)].