Return to Revisions

To add a semantic argument: models of tensor logic are given by symmetric monoidal categories with an exponentiating object $\bot$ serving as pole; negation is then given by $\neg A = \bot^A$. For example, one may choose any object of a symmetric monoidal closed category as pole, and degenerate special cases of this are given by abelian groups viewed as discrete categories. Now take eg the additive group of integers, and $1$ as pole. Then an arrow $\bot\otimes\bot\to\bot$ in the model would mean that $1+1=1$.