Is there an intuitive way to understand the split between additive and multiplicative connectives?

194 Views Asked by At

For example, where $\otimes$ is multiplicative conjunction, our rules are: $$ \frac { \Gamma ,\: A,\: B\: \Rightarrow \Delta }{ \Gamma ,\: A\otimes B\Rightarrow \Delta } \quad \quad \frac { \Gamma \: \Rightarrow \: A,\: \Delta \quad \quad \Gamma \prime \: \Rightarrow \: B,\: \Delta \prime }{ \Gamma ,\: \Gamma \prime \Rightarrow \: A\otimes B,\: \Delta ,\: \Delta \prime } $$ and where $\sqcap$ is additive conjunction, and only one of (A), (B) is present: $$\frac { \Gamma, \: (A),\: (B)\: \Rightarrow \: \Delta }{ \Gamma ,\: A\sqcap B\Rightarrow \: \Delta } \quad \quad \quad \frac { \Gamma \: \Rightarrow \: A,\: \Delta \quad \quad \Gamma \: \Rightarrow \: B,\: \Delta }{ \Gamma \: \Rightarrow \: A\sqcap B,\: \Delta } $$

I keep seeing explanations along the lines of "In the additive form, the context of the premises must be the same and it is contracted, whereas in the multiplicative form, the context of the premises can be different and it is not contracted."

I see that in the multi-sequent rules. What about the single-sequent rules? We need them this way if we want to avoid just having operator rules with built-in weakening or built-in contraction... but now we have built-in weakening on the multi-sequent rules and built-in contraction on the single-sequent rules, or vice versa, and I'm having trouble making sense of that.

Is there an intuitive way to understand what's going on here?

edit: I guess you could try to explain the additive single-sequent rules by saying "Every wff that is active in an additive rule must occur in the same context. Two wffs in the same sequent, as in $\Gamma ,\: A,\: B\: \Rightarrow \Delta$, are not in the same context: one is in $\Gamma ,\: ...,\: B\: \Rightarrow \Delta$ and one is in $\Gamma ,\: A,\: ...\: \Rightarrow \Delta$."

This seems like a mistake, since if applied the same line of thought to the multiplicative rule, we'd end up with $\Gamma ,\:\Gamma ,\:A,\: B,\: A\otimes B\Rightarrow \Delta, \:\Delta$—yikes.