Axioms and models of linear logic |
| |
Authors: | Wim H. Hesselink |
| |
Affiliation: | (1) Vakgroep Infonnatica, Rijksuniversiteit Groningen, P.O. Box 800, 9700 AV Groningen, Netherlands |
| |
Abstract: | 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. |
| |
Keywords: | Linear logic Axiomatisation Model theory Monoid Sequent calculus Deduction theorem Equational proofs Phase structures |
本文献已被 SpringerLink 等数据库收录! |