Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Modelling Multiplicative Linear Logic via Deep Inference

Tomer Galor, Andrea Schalk

TL;DR

This paper looks in detail at existing translations between a deep inference system and the standard sequent calculus one, provides a simplified translation, and provides a formal proof that a standard approach to modelling is indeed invariant to all these translations.

Abstract

Multiplicative linear logic is a very well studied formal system, and most such studies are concerned with the one-sided sequent calculus. In this paper we look in detail at existing translations between a deep inference system and the standard sequent calculus one, provide a simplified translation, and provide a formal proof that a standard approach to modelling is indeed invariant to all these translations. En route we establish a necessary condition for provable sequents related to the number of pars and tensors in a formula that seems to be missing from the literature.

Modelling Multiplicative Linear Logic via Deep Inference

TL;DR

This paper looks in detail at existing translations between a deep inference system and the standard sequent calculus one, provides a simplified translation, and provides a formal proof that a standard approach to modelling is indeed invariant to all these translations.

Abstract

Multiplicative linear logic is a very well studied formal system, and most such studies are concerned with the one-sided sequent calculus. In this paper we look in detail at existing translations between a deep inference system and the standard sequent calculus one, provide a simplified translation, and provide a formal proof that a standard approach to modelling is indeed invariant to all these translations. En route we establish a necessary condition for provable sequents related to the number of pars and tensors in a formula that seems to be missing from the literature.
Paper Structure (16 sections, 33 theorems, 40 equations, 7 figures)

This paper contains 16 sections, 33 theorems, 40 equations, 7 figures.

Table of Contents

  1. Introduction
  2. Background
  3. Derivation systems under consideration
  4. Models of linear logic
  5. Notation
  6. Properties of MLL
  7. A necessary condition for derivable formulae/sequents
  8. Translations between the two systems
  9. An alternative translation
  10. Cut Elimination
  11. Modelling derivations
  12. Concordance spaces
  13. Deep inference derivations as morphisms
  14. Sequent calculus derivations as cliques
  15. Equivalence of Transformations
  16. ...and 1 more sections

Key Result

Proposition 2.1

In $\mathalpha\textbf{MLL}^-_{\mathalpha DI}$, a formula is derivable with the following axioms: if and only if it is derivable with the following axioms:

Figures (7)

  • Figure 1: Proofs of the sequent ${\vdash \overline{P}, Q}$ for introduction and cut rules
  • Figure 2: Proofs of the sequent ${\vdash \overline{P}, Q}$ for switch
  • Figure 3: Proofs of the sequent ${\vdash \overline{P}, Q}$ for associativity
  • Figure 4: Proofs of the sequent ${\vdash \overline{P}, Q}$ for commutativity
  • Figure 5: Derivations showing how to append a formula $B$ with pars and tensors to the left and right of the formulae in the sequent ${\vdash \overline{P}, Q}$, obtained by a derivation $\Pi_{}$.
  • ...and 2 more figures

Theorems & Definitions (39)

  • Proposition 2.1
  • Proposition 2.2
  • Definition 1
  • Proposition 3.1
  • Proposition 3.2
  • Theorem 3.3
  • Corollary 3.4
  • Theorem 3.5
  • Corollary 3.6
  • Proposition 4.1
  • ...and 29 more