1. Context
Let $(\mathscr{C}, \otimes, \top, \oplus, \bot, \delta ^l, \delta^r)$ be a linearly distributive category.
Let $(S,S', \alpha, \beta, \alpha‘, \beta‘)$ be a negation on $\mathscr{C}$. This data consists of:
- Two contravariant functors $S: \mathscr{C}^{op} \rightarrow \mathscr{C}$ and $S': \mathscr{C}^{op} \rightarrow \mathscr{C}$
- For any $A \in \mathscr{C}$ four morphisms: $$\alpha: SA \otimes A \rightarrow \bot \\ \alpha': A \otimes S'A \rightarrow \bot \\ \beta: \top \rightarrow A \oplus SA \\ \beta': \top \rightarrow S'A \oplus A$$ satisfying certain coherence diagrams.
Interpreting $\otimes$ as conjunction, $\oplus$ as disjunction, $\bot$ as falsity, $\top$ as truth and $\rightarrow$ as implication the morphisms $\alpha$ and $\alpha'$ are reminiscent of the principle of contradiction while $\beta$ and $\beta'$ look like tertium non datur.
2. Questions
- Can this observation be given mathematical meaning? Can it be made precise?
- If so, how do the coherence diagrams for $\alpha$ , $\alpha'$, $\beta$ , $\beta'$ relate to the law of excluded middle and the principle of contradiction?
I suppose this question arises from my (still remaining) lack of understanding of the connection between linear logic and linearly distributive categories.