Multiplicative-Additive Linear Logic

Let $\mathcal{A}$ be a countable set of propositional constants.

Formula

$\mathrm{Form}(\mathcal{A})$ is given by the following grammar:

$$\begin{array}{rl}A,B::=& a|a^{\perp }\\ & \perp |1|A⅋B|A\otimes B\text{(multiplicative)}\\ & \top |0|A\&B|A\oplus B\text{(additive)}\end{array}$$

Idea

& and $⅋$ are invertable but $\otimes$ and $\oplus$ are not. What is additive?

Theory

$$\begin{array}{rlrlrl}\text{id}\frac{}{A,A^{\perp }}& \text{cut}\frac{\Gamma ,A{A}^{\perp },\Delta }{\Gamma ,\Delta }& & (base)& & \\ \text{⅋}\frac{\Gamma ,A,B}{\Gamma ,A⅋B}& \text{⊗}\frac{\Gamma ,A\Delta ,B}{\Gamma ,\Delta ,A\otimes B}& \perp \frac{\Gamma }{\Gamma ,\perp }\frac{}{1}& (multiplicative)& & \\ \text{⊕}\frac{\Gamma ,A\Delta ,B}{\Gamma ,\Delta ,A\oplus B}& \text{⊕}\frac{\Gamma ,A}{\Gamma ,A\oplus B}& \text{⊕}\frac{\Gamma ,B}{\Gamma ,A\oplus B}& \perp \frac{\Gamma }{\Gamma ,\perp }& & (additive)\end{array}$$