The finite model property for various fragments of intuitionistic linear logic

Mitsuhiro Okada, Kazushige Terui

Research output: Contribution to journalArticle

61 Citations (Scopus)

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 GL-c of Ono [11], that will settle the open problems stated in Ono [12].

Original languageEnglish
Pages (from-to)790-802
Number of pages13
JournalJournal of Symbolic Logic
Volume64
Issue number2
Publication statusPublished - 1999 Jun

Fingerprint

Finite Models
Linear Logic
Intuitionistic Logic
Fragment
Multiplicative
Substructural Logics
Contraction
Open Problems
Logic

ASJC Scopus subject areas

  • Logic

Cite this

The finite model property for various fragments of intuitionistic linear logic. / Okada, Mitsuhiro; Terui, Kazushige.

In: Journal of Symbolic Logic, Vol. 64, No. 2, 06.1999, p. 790-802.

Research output: Contribution to journalArticle

@article{455a9984e20b4d13b8d259d46855082c,
title = "The finite model property for various fragments of intuitionistic linear logic",
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 GL-c of Ono [11], that will settle the open problems stated in Ono [12].",
author = "Mitsuhiro Okada and Kazushige Terui",
year = "1999",
month = "6",
language = "English",
volume = "64",
pages = "790--802",
journal = "Journal of Symbolic Logic",
issn = "0022-4812",
publisher = "Association for Symbolic Logic",
number = "2",

}

TY - JOUR

T1 - The finite model property for various fragments of intuitionistic linear logic

AU - Okada, Mitsuhiro

AU - Terui, Kazushige

PY - 1999/6

Y1 - 1999/6

N2 - 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 GL-c of Ono [11], that will settle the open problems stated in Ono [12].

AB - 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 GL-c of Ono [11], that will settle the open problems stated in Ono [12].

UR - http://www.scopus.com/inward/record.url?scp=0033441201&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0033441201&partnerID=8YFLogxK

M3 - Article

AN - SCOPUS:0033441201

VL - 64

SP - 790

EP - 802

JO - Journal of Symbolic Logic

JF - Journal of Symbolic Logic

SN - 0022-4812

IS - 2

ER -