Minimal Linear Logic

This example investigates minimal linear logic (often called intuitionistic linear logic). It specifies

the formulas of minimal linear logic

the system AND of annotated natural deduction in which the classification of introduction and elimination rules is explicit in the judgments

the sequent calculus LV with linear and modal zone on the left and single conclusion on the right

translations which are inductive and therefore demonstrate the equivalence of these systems from the point of view derivability:

natural deductions to annotated natural deductions ND -> AND

annotated natural deductions to sequent derivations AND -> LV

sequent derivations to annotated natural deductions LV -> AND

annotated natural deduction to natural deductions AND -> ND

some reduction rules for annotated natural deduction