Is multiset consequence trivial?

Abstract

Dave Ripley has recently argued against the plausibility of multiset consequence relations and of contraction-free approaches to paradox. For Ripley, who endorses a nontransitive theory, the best arguments that buttress transitivity also push for contraction—whence it is wiser for the substructural logician to go nontransitive from the start. One of Ripley’s allegations is especially insidious, since it assumes the form of a trivialisation result: it is shown that if a multiset consequence relation can be associated to a closure operator in the expected way, then it necessarily contracts. We counter Ripley’s objection by presenting an approach to multiset consequence that escapes this trap. This approach is multiple-conclusioned in a heterodox way, for multiple succedents are given a conjunctive, rather than a disjunctive reading. Finally, we address a further objection by French and Ripley to the effect that the informational interpretation of sequents in (affine) linear logic does not motivate cut.

Appendix: The sequent calculi \(\mathcal {ALL}_{2}\) and \(\mathcal {ALL}_{1}\)

The calculus $\mathcal {ALL}_{2}$ is formulated in a language containing the connectives $\otimes$ (intensional conjunction), $\oplus$ (intensional disjunction), $\sqcap$ (extensional conjunction), $\sqcup$ (extensional disjunction), $\lnot$ (negation). Intensional implication $\rightarrow$ and extensional implication $\leadsto$ are respectively definable as $\alpha \rightarrow \beta =\lnot \alpha \oplus \beta$ and $\alpha \leadsto \beta =\lnot \alpha \sqcup \beta$. $\mathcal {ALL}_{2}$-formulas are defined as usual, while $\mathcal {ALL}_{2}$-sequents are pairs of finite or empty multisets of $\mathcal {ALL}_{2}$-formulas. The postulates of the calculus follow:

$$\begin{aligned} \begin{array} [t]{lll} \alpha \Rightarrow \alpha \text { (Identity)} &{} &{} \dfrac{\varGamma \Rightarrow \varDelta ,\alpha \qquad \alpha ,\varPi \Rightarrow \varSigma }{\varGamma ,\varPi \Rightarrow \varDelta ,\varSigma }\text { (Cut)}\\ \dfrac{\varGamma \Rightarrow \varDelta }{\alpha ,\varGamma \Rightarrow \varDelta }\text { (Weakening L)} &{} &{} \dfrac{\varGamma \Rightarrow \varDelta }{\varGamma \Rightarrow \varDelta ,\alpha }\text { (Weakening R)}\\ \dfrac{\alpha ,\beta ,\varGamma \Rightarrow \varDelta }{\alpha \otimes \beta ,\varGamma \Rightarrow \varDelta }\text { (}\otimes \text {L)} &{} &{} \dfrac{\varGamma \Rightarrow \varDelta ,\alpha \qquad \varPi \Rightarrow \varSigma ,\beta }{\varGamma ,\varPi \Rightarrow \varDelta ,\varSigma ,\alpha \otimes \beta }\text { (}\otimes \text {R)}\\ \dfrac{\alpha ,\varGamma \Rightarrow \varDelta \qquad \beta ,\varPi \Rightarrow \varSigma }{\alpha \oplus \beta ,\varGamma ,\varPi \Rightarrow \varDelta ,\varSigma }\text { (}\oplus \text {L)} &{} &{} \dfrac{\varGamma \Rightarrow \varDelta ,\alpha ,\beta }{\varGamma \Rightarrow \varDelta ,\alpha \oplus \beta }\text { (}\oplus \text {R)}\\ \dfrac{\alpha ,\varGamma \Rightarrow \varDelta }{\alpha \sqcap \beta ,\varGamma \Rightarrow \varDelta }\quad \dfrac{\beta ,\varGamma \Rightarrow \varDelta }{\alpha \sqcap \beta ,\varGamma \Rightarrow \varDelta }\text { (}\sqcap \text {L)} &{} &{} \dfrac{\varGamma \Rightarrow \varDelta ,\alpha \qquad \varGamma \Rightarrow \varDelta ,\beta }{\varGamma \Rightarrow \varDelta ,\alpha \sqcap \beta }\text { (}\sqcap \text {R)}\\ \dfrac{\alpha ,\varGamma \Rightarrow \varDelta \qquad \beta ,\varGamma \Rightarrow \varDelta }{\alpha \sqcup \beta ,\varGamma \Rightarrow \varDelta }\text { (}\sqcup \text {L)} &{} &{} \dfrac{\varGamma \Rightarrow \varDelta ,\alpha }{\varGamma \Rightarrow \varDelta ,\alpha \sqcup \beta }\quad \dfrac{\varGamma \Rightarrow \varDelta ,\beta }{\varGamma \Rightarrow \varDelta ,\alpha \sqcup \beta }\text { (}\sqcup \text {R)}\\ \dfrac{\varGamma \Rightarrow \varDelta ,\alpha }{\lnot \alpha ,\varGamma \Rightarrow \varDelta }\text { (}\lnot \text {L)} &{} &{} \dfrac{\alpha ,\varGamma \Rightarrow \varDelta }{\varGamma \Rightarrow \varDelta ,\lnot \alpha }\text { (}\lnot \text {R)} \end{array} \end{aligned}$$

The calculus $\mathcal {ALL}_{1}$ is formulated in a language containing the connectives $\otimes$ (intensional conjunction), $\oplus$ (intensional disjunction), $\sqcap$ (extensional conjunction), $\sqcup$ (extensional disjunction), but no negation. $\mathcal {ALL}_{1}$-formulas are assembled from literals of the form p or of the form $\lnot p$ (for p a variable of the language) by iterated application of the connectives. A negation connective can be introduced into the metalanguage by stipulating the following inductive clauses for complex negated formulas:

$$\begin{aligned} \begin{array} [c]{ll} \lnot \lnot \alpha =\alpha \text {;} &{} \\ \lnot \left( \alpha \otimes \beta \right) =\lnot \alpha \oplus \lnot \beta \text {;} &{} \lnot \left( \alpha \oplus \beta \right) =\lnot \alpha \otimes \lnot \beta \text {;}\\ \lnot \left( \alpha \sqcap \beta \right) =\lnot \alpha \sqcup \lnot \beta ;\qquad &{} \lnot \left( \alpha \otimes \beta \right) =\lnot \alpha \sqcup \lnot \beta . \end{array} \end{aligned}$$

$\mathcal {ALL}_{1}$-sequents are finite or empty multisets of $\mathcal {ALL}_{1}$-formulas. The postulates of the calculus follow:

$$\begin{aligned} \begin{array} [c]{ll} \alpha ,\lnot \alpha \text { (Identity);} &{} \\ &{} \\ \dfrac{\varGamma ,\alpha \qquad \varDelta ,\lnot \alpha }{\varGamma ,\varDelta }\text { (Cut);} &{} \dfrac{\varGamma }{\varGamma ,\alpha }\text { (Weakening);}\\ &{} \\ \dfrac{\varGamma ,\alpha \qquad \varDelta ,\beta }{\varGamma ,\varDelta ,\alpha \otimes \beta }\text { (}\otimes \text {);} &{} \dfrac{\varGamma ,\alpha ,\beta }{\varGamma ,\alpha \oplus \beta }\text { (}\oplus \text {);}\\ &{} \\ \dfrac{\varGamma ,\alpha \qquad \varGamma ,\beta }{\varGamma ,\alpha \sqcap \beta }\text { (}\sqcap \text {);} &{} \dfrac{\varGamma ,\alpha /\beta }{\varGamma ,\alpha \sqcup \beta }\text { (}\sqcup \text {).} \end{array} \end{aligned}$$