Axioms and Models of Linear LogicHesselink, W. H., 1990, In : Formal Aspects of Computing. 2, 28 p.
Research output: Contribution to journal › Article › Academic › peer-review
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.
|Number of pages||28|
|Journal||Formal Aspects of Computing|
|Publication status||Published - 1990|
- Phase structures, Equational proofs, Deduction theorem, Sequent calculus, Monoid, Model theory, Axiomatisation, Linear logic
No data available