Formalized Meta-Theory of Linear Logic

This web-page documents the ongoing formalization of the meta-theory of several linear logic variants. Specifically, we are interested in the following meta-theorems.

• Cut-admissibility: this shows that the calculus is consistent, i.e., that it only proves theorems.
• Identity reduction: this shows that the calculus is syntactically complete, meaning every provable theorem can be proved using this calculus.
• Context monotonicity: this shows that the unrestricted hypotheses may be freely weakened or contracted.
• Context permutability: this shows that the unrestricted and linear hypotheses may be freely permuted, often done explicitly using an "exchange" rule.

For more details on the formalization, please see the following sequence of papers.

• LSFA/ENTCS version
• TCS version (under review)

The links below are to the HTML versions of the various developments. The actual Abella sources are also linked, but the development can be browsed without running Abella yourself.

Propositional linear logic variants / unfocused sequent calculi

• One-sided sequent calculus for MLL

  This is the logic that contains only the multiplicative connectives and uses a one-sided sequent calculus with dual atoms in the initial rule.

• One-sided sequent calculus for MALL

  This is the logic that contains the multiplicative and additive connectives of linear logic, and uses a one-sided sequent calculus.

• Two-sided sequent calculus for MALL

  This is the logic that contains the multiplicative and additive connectives of linear logic, and uses a two-sided sequent calculus.

• One-sided sequent calculus for MELL

  This is the logic that contains the multiplicative and exponentials, using a one-sided sequent calculus.

First-order linear logic variants / unfocused sequent calculi

• One-sided sequent calculus for first-order MALL

  Multiplicative and additive connectives of linear logic, with quantifiers. Using a one-sided sequent calculus.

Focused sequent calculi

• One-sided sequent calculus for focused MALL

  Multiplicative and additive connectives of linear logic. Using a one-sided sequent calculus with focusing.

---

Last updated: Fri Jan 25 14:09:56 CEST 2019