Axioms and Models of Linear Logic

Hesselink, W. H., 1990, In : Formal Aspects of Computing. 2, 28 p.

Research output: Contribution to journalArticleAcademicpeer-review

Copy link to clipboard


Girard's recent system of linear logic is presented in a way that avoids the two-level structure of formulae and sequents, and that minimises the number of primitive function symbols. A deduction theorem is proved concerning the classical implication as embedded in linear logic. The Hilbert-style axiomatisation is proved to be equivalent to the sequent formalism. The axiomatisation leads to a complete class of algebraic models. Various models are exhibited. On the meta-level we use Dijkstra's method of explicit equational proofs.
Original languageEnglish
Number of pages28
JournalFormal Aspects of Computing
Publication statusPublished - 1990


  • Phase structures, Equational proofs, Deduction theorem, Sequent calculus, Monoid, Model theory, Axiomatisation, Linear logic

Download statistics

No data available

ID: 3359894