The finite model property for various fragments of intuitionistic linear logic
- 1 June 1999
- journal article
- Published by Cambridge University Press (CUP) in The Journal of Symbolic Logic
- Vol. 64 (2) , 790-802
- https://doi.org/10.2307/2586501
Abstract
Recently Lafont [6] showed the finite model property for the multiplicative additive fragment of linear logic (MALL) and for affine logic (LLW), i.e., linear logic with weakening. In this paper, we shall prove the finite model property for intuitionistic versions of those, i.e. intuitionistic MALL (which we call IMALL), and intuitionistic LLW (which we call ILLW). In addition, we shall show the finite model property for contractive linear logic (LLC), i.e., linear logic with contraction. and for its intuitionistic version (ILLC). The finite model property for related substructural logics also follow by our method. In particular, we shall show that the property holds for all of FL and GL−-systems except FLc and of Ono [11], that will settle the open problems stated in Ono [12].Keywords
This publication has 7 references indexed in Scilit:
- Decidability of linear affine logicPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- The finite model property for BCI and related systemsStudia Logica, 1996
- Linear Logic: its syntax and semanticsPublished by Cambridge University Press (CUP) ,1995
- Advances in Linear LogicPublished by Cambridge University Press (CUP) ,1995
- The finite model property for BCK and BCIWStudia Logica, 1994
- Non‐commutative intuitionistic linear logicMathematical Logic Quarterly, 1990
- Linear logicTheoretical Computer Science, 1987