Linear Logic

logic

Definition

Linear Logic

todo

Operators

Multiplicative Conjunction

Definition

Multiplicative Conjunction ( Linear Logic)

bundles and as independent resources, each available exactly once. In a proof / program, is produced from disjoint portions of the context and consumed one and one at a time.

Right sequent (introduce ): split resources to build each side

Left sequent (use ): to use a bundle, open it

With as its neutral element, forms a monoid :

Link to original

Additive Disjunction

Definition

Additive Disjunction ( Linear Logic)

means the provider makes an internal choice: it commits to either or and proceeds on that branch (the other branch is discarded). No implicit copying or discarding beyond the chosen branch.

In a proof / program, constructing means you present either a proof of (left injection) or a proof of (right injection), tagged accordingly.

Analogy: A notification bot chooses its channel:

The additive disjunction is associative/commutative with neutral element :

Duality: .

Link to original

Additive Conjunction

Definition

Additive Conjunction ( Linear Logic)

(read “with”) means the environment makes an external choice: it may demand either or , and the provider must be ready to handle the chosen branch. Only the chosen branch continues.

In a proof / program, constructing means you can produce and (with the same context) produce ; offering promises readiness for either.

Analogy: A service menu:

The additive conjunction is associative/commutative with neutral element :

Duality: .

Link to original

No Weakening

See Monotonicity of Entailment (Propositional Logic).

In classical logic, if you know is true, you can infer that is true (contraction, idempotent), and you can also use as many times as you want. If you can prove from , and you know , then is true, and remains available. Similarly, if you have proved , you can infer even if wasn’t used (weakening).

Linear logic operates differently: Every hypothesis (premise) must be used exactly once in a derivation. You cannot simply ignore a resource. From , inferring is not allowed.