The finite model property for various fragments of intuitionistic linear logic

被引:65
作者
Okada, M [1 ]
Terui, K [1 ]
机构
[1] Keio Univ, Dept Philosophy, Minato Ku, Tokyo 108, Japan
关键词
D O I
10.2307/2586501
中图分类号
O1 [数学];
学科分类号
0701 ; 070101 ;
摘要
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 itituitionistic versions of those, i.e. intuitionistic MALL (which rye call IMALL). and intuitionistic LLW (which we call ILLW). In addition, we shall show the finite model properly for contractive li.rear 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 GC(-) -systems except FLC and GL(C)(-) of One II II, that will settle the open problems stated in Ono [12].
引用
收藏
页码:790 / 802
页数:13
相关论文
共 15 条
  • [1] NONCOMMUTATIVE INTUITIONISTIC LINEAR LOGIC
    ABRUSCI, VM
    [J]. ZEITSCHRIFT FUR MATHEMATISCHE LOGIK UND GRUNDLAGEN DER MATHEMATIK, 1990, 36 (04): : 297 - 318
  • [2] Buszkowski W., 1996, Studia Logica, V57, P303, DOI 10.1007/BF00370837
  • [3] LINEAR LOGIC
    GIRARD, JY
    [J]. THEORETICAL COMPUTER SCIENCE, 1987, 50 (01) : 1 - 102
  • [4] GIRARD JY, 1993, ADV LINEAR LOGIC, P1
  • [5] KOPYLOV AP, 1995, IEEE S LOG, P496, DOI 10.1109/LICS.1995.523283
  • [6] The finite model property for various fragments of linear logic
    Lafont, Y
    [J]. JOURNAL OF SYMBOLIC LOGIC, 1997, 62 (04) : 1202 - 1208
  • [7] Meyer R. K., 1994, Studia Logica, V53, P107, DOI 10.1007/BF01053025
  • [8] MEYER RK, 1973, UNPUB IMPROVED DECIS
  • [9] OKADA M, 1996, ENTCS ELECT NOTES TH, V3
  • [10] OKADA M, 1999, IN PRESS THEORET NOV