Hostname: page-component-586b7cd67f-g8jcs Total loading time: 0 Render date: 2024-11-28T16:01:24.012Z Has data issue: false hasContentIssue false
  • English
  • Français

The finite model property for various fragments of intuitionistic linear logic

Published online by Cambridge University Press:  12 March 2014

Mitsuhiro Okada  and
Kazushige Terui
Mitsuhiro Okada
Affiliation:
Department of Philosophy, Keio University, 2–15–45 Mita, Minatoku, Tokyo 108, Japan E-mail: [email protected]
Kazushige Terui
Affiliation:
Department of Philosophy, Keio University, 2–15–45 Mita, Minatoku, Tokyo 108, Japan E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

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].

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 64 , Issue 2 , June 1999 , pp. 790 - 802
Copyright
Copyright © Association for Symbolic Logic 1999

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1] Abrusci, V. Michele, Non-commutative intuitionistic linear propositional logic, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, vol. 36 (1990), pp. 297–318.CrossRefGoogle Scholar
[2] Buszkowski, W., The finite model property for BCI and related systems, Studia Logica, vol. 57 (1996), pp. 303–323.Google Scholar
[3] Girard, Jean-Yves, Linear logic, Theoretical Computer Science, vol. 50 (1987), pp. 1–102.Google Scholar
[4] Girard, Jean-Yves, Linear logic: Its syntax and semantics, Advances in linear logic (Girard, J.-Y., Lafont, Y., and Regnier, L., editors), Cambridge University Press, 1995, Proceedings of the Workshop on Linear Logic, Ithaca, New York, 06 1993, pp. 1–42.Google Scholar
[5] Kopylov, Alexei P., Decidability of linear affine logic, Tenth Annual IEEE Symposium on Logic in Computer Science (San Diego, California) (Kozen, D., editor), 06 1995, pp. 496–504.Google Scholar
[6] Lafont, Yves, The finite model property for various fragments of linear logic, this Journal, vol. 62 (1997) , no. 4, pp. 1202–1208.Google Scholar
[7] Meyer, Robert K., Improved decision procedures for pure relevant logic, 1973, Manuscript.Google Scholar
[8] Meyer, Robert K. and Ono, H., The finite model property for BCK and BCIW, Studia Logica, vol. 53 (1994), pp. 107–118.Google Scholar
[9] Okada, Mitsuhiro, Phase semantics for higher order completeness, cut-elimination and normalization proofs, Theoretical Computer Science, to appear, 11 1999.Google Scholar
[10] Okada, Mitsuhiro, Phase semantics for higher order completeness, cut-elimination and normalization proofs (extended abstract), ENTCS (Electronic Notes in Theoretical Computer Science) (Girard, J.-Y., Okada, M., and Scedrov, A., editors), vol. 3: A Special Issue on the Linear Logic 96, Tokyo Meeting, Elsevier-ENTCS, 1996.Google Scholar
[11] Ono, Hiroakira, Semantics for substructural logics, Substructural logics (Došen, K. and Schröder-Heister, P., editors), Oxford University Press, 1994, pp. 259–291.Google Scholar
[12] Ono, Hiroakira, Decidability and finite model property of substructural logics, The Tbilisi Symposium on Logic, Language and Computation: Selected Papers (Studies in Logic, Language and Information) (Ginsburg, J. et al., editors), CLSI, 1998, pp. 263–274.Google Scholar
[13] Sambin, Giovanni, The semantics of pretopologies, Substructural logics (Došen, K. and Schröder-Heister, P., editors), Oxford University Press, 1994, pp. 293–307.Google Scholar
[14] Troelstra, Anne S., Lectures on linear logic, CSLI Lecture Notes 29, Center for the Study of Language and Information, Stanford, California, 1992.Google Scholar
[15] Troelstra, Anne S. and van Dalen, Dirk, Constructivism in Mathematics: An Introduction, Studies in logic and the foundations of mathematics 121, vol. 1, North Holland, 1988.Google Scholar