# Is there a "standard" normal form for formulas in linear logic?

For propositional logic, for every formula, there is an equivalent formula in the CNF and DNF. These normal forms have the advantage of being representable in a "tabular" form rather than a "tree" form, which may be more computationally friendly.

Is there something similar for linear logic? I am mainly interested in the additive-multiplicative fragment.

• Is this what you mean by "linear logic"? en.wikipedia.org/wiki/Linear_logic May 2, 2023 at 14:13
• Yes, that's what I mean. May 3, 2023 at 13:11

The thing that makes DNF and CNF work for classical propositional logic is that conjunction and disjunction distribute over each other. The fact that $$A \wedge (B \vee C) \equiv (A \wedge B) \vee (A \wedge C)$$ lets us push conjunctions under disjunctions, and dually $$A \vee (B \wedge C) \equiv (A \vee B) \wedge (A \vee C)$$ lets us do the reverse. We also have, by De Morgan's laws, that negation distributes over both conjunction and disjunction, so negation can be pushed down to the propositional variables.
A similar normal form is polynomials for rings. Here, we make use of the fact that $$x(y + z) = xy + xz$$ is a theorem of ring theory to convert all of the expressions of ring theory into the form $$n_xx + n_yy + n_zz + n_{x^2}x^2 + n_{xy}xy + n_{xz}xz + \dots$$ for $$n_{abc} \in \mathbb Z$$ and formal variables $$x$$, $$y$$, and $$z$$. You could call polynomials “additive normal form”, but usually we don't because there is no contrasting “multiplicative normal form”, given that addition does not distribute over multiplication.
In classical linear logic, every connective satisfies a De Morgan law with respect to $$(-)^\bot$$, so we can produce a negation normal form. However, among the main connectives, there are many pairs with no distributivity laws. For example, we have that $$A \& (B \oplus C) \nvdash (A \& B) \oplus (A \& B)$$, intuitively because we're forced to make a choice between $$A\&B$$ and $$A\&C$$ before being able to inspect the $$B \oplus C$$, or after discarding the $$A$$. The multiplicative connectives similarly do not distribute over each other, and neither do, say, $$\otimes$$ and $$\&$$. These lacks of distributive laws mean that we can arbitrarily nest connectives to produce logically distinct formulae from any finitely tabulated form.
We do, however, have some useful distributivity laws in linear logic. We have that $$A \otimes (B \oplus C) \equiv (A \otimes B) \oplus (A \otimes C)$$, and dually that $$A ⅋ (B \& C) \equiv (A ⅋ B) \& (A ⅋ C)$$. The pattern we may notice here is that both $$⊗$$ and $$⊕$$ are positive connectives, while $$⅋$$ and $$\&$$ are both negative connectives. We can therefore say that any hereditarily positive formula has a $$⊕$$-normal form, and any hereditarily negative formula has a $$\&$$-normal form. Hereditarily positive/negative formulae occur naturally within polarised linear logic formulae – being delimited by polarity shifts $$!$$ and $$?$$. These normal forms remind us of polynomials, with the distributivity laws only going one way, producing an additive normal form in each case.