A Kripke Type Semantics for Substructural Logics with Strong Negation (Abstract)

Norihiro Kamide

                        kamide@wakayama-nct.ac.jp

(Wakayama National College of Technology, Noshima 77, Nada, Gobo, Wakayama 644-0023, JAPAN)

Abstract

We introduce a Kripke type semantics for propositional substructural logics with strong negation, and show completeness theorems for these logics by using extended Ishihara’s canonocal model construction method. The present paper’s framework can deal with broard range of substructural logics with strong negation including Nelson’s logic N^{−}, Wansing’s logic COSPL (and its extensions), extended Visser’s basic propositional logic with strong negation and extended positive relevant logics with strong negation.

1 Introduction

First, we will present a short servey of Kripke type semantics for substructural logics and logics with strong negation. Second, we will show the organization of this paper.

Examples of substructural logics discussed in this paper are as follows: positive relevant logics in philosophical motivation, intuitionistic linear logic in computer science and BCK-logic closely related to BCK-algebras. A historical servey of Kripke type semantics for these logics is as follows. In 1972, Routley and Meyer introduced a Kripke type semantics for positive relevant logics, which semantics was characterized with three-termed accessibility relation. (See [2]). In 1985, Ono and Komori gave us a Kripke type semantics for FL-family including BCK-logic, intuitionistic linear logic and full Lambek logic FL, which semantics was characterized with semilattice-orderd monoid. (see [10]). In 1988, Došen introduced a Kripke type semantics, named groupoid semantics, for broard range of substructural logics including the logics mentioned above (see [4][5]). Došen’s semantics is essentially the same as Ono and Komori’s one, but the semantics was independently proposed. In 2000, Ishihara introduced a canonical model construction method for the semantics of Ono and Komori (see [6]). This method can deal with broard range of substructural logics including some Došen’s logics, Corsi’s logic F and the standard substructural logics mentioned above. A class of the logics characterized by this method is called, by Ishihara, normal substructural logic.

Next we explain a servey of logics with strong negation (or constructive negation) and their Kripke type semantics. The strong negation was first proposed by Nelson (1949) and Markov (1950) independently. The negation was introduced to express ”constructive falsity” in recursive realizability (see [8]). Nelson’s logics such as N and N^{−} have been studied by many logicians (see, e.g., [1] [14]). These logics are, roughly speaking, slight extensions or modifications of the intuitionistic logic. Kripke type semantics for Nelson’s logics are different from that for the intuitionistic logic. These semantics have two kinds of valuation: ⊧^{+} (correspond to provability) and ⊧^{−} (correspond to refutability). In 1969, Thomason introduced a Kripke type semantics for a predicate logic with strong negation, which semantics was characterized with binary accessibility relation similar to the binary relation of Kripke type semantics for the predicate intuitionistic logic (see [12]). In 1993, Wansing proposed propositional substructural logics with strong negation such as COSPL-family including some Nelson’s logics (roughly speaking, COSPL-family is obtained from FLfamily by adding strong negation). Wansing gave us a Kripke type semantics and its informational interpretation for these logics (see [14]). Wansing’s semantics is a natural extention of Došen’s one.

In the present paper, we extend Ishihara’s result to substructural logics with strong negation. As a result, we can deal with broad range of logics with strong negation such as Nelson’s N^{−} and Wansing’s COSPL (and its extensions). Thus, the result is also an extension of Wansing’s one.

Next we present the orgnization of the paper.

In Section 2, we present Ishihara’s basic normal substructural logic L and its extensions, and introduce new normal substructural logics such as Visser’s basic propositional logic BPL in [13] (a Hilbert style system for BPL is proposed in [9] [11]), relevant logics RMO^{+}, EMO^{+}, Corsi’s logics FT, FR, FRT in [3] and Méndez’s logics T_{+}^{∘}, E_{+}^{∘}, R_{+}^{∘}, RMO_{+}^{∘}, EMO_{+}^{∘}, S4_{+}^{∘} in [7]. (We can prove the compleateness theorem for the new logics by using Ishihara’s canonical model construction method.) Next we introduce extended basic normal substructural logic with strong negation L^{∼} and its extensions. These extensions include Nelson’s logic N^{−} and Wansing’s logic COSPL (and its extensions). Further we define a new family of normal substructural logics with strong negation. The new logics are as follows: extended Došen’s logic DE^{∼}, extended positive relevant logics B^{∼}, T^{∼}, E^{∼}, R^{∼}, RMO^{∼}, EMO^{∼}, extended strict implication S4^{∼}, extended Corsi’s logics F^{∼}, FT^{∼}, FR^{∼} FRT^{∼}, extended Visser’s logic BPL^{∼}, and extended Méndez’s logics T_{∘}^{∼}, E_{∘}^{∼}, R_{∘}^{∼}, EMO_{∘}^{∼}, RMO_{∘}^{∼}, S4_{∘}^{∼}.

In Section 3, we introduce a Kripke type semantics for the normal substructural logics with strong negation mentioned above and show soundness theorem and a correspondence between axiom schemes and conditions on frames.

In Section 4, we prove the completeness theorems for the logics by using extended Ishihara’s canonical model construction method. In the sequel, we can show the completeness theorem for any logic obtained from L^{∼} by adding arbitrary combinations of the axiom schemes introduced in Section 2.

References

[1] Almukdad, A., and D. Nelson, Constructible falsity and inexact predicates. Journal of Symbolic Logic 49 (1984), 231 - 233.

[2] Anderson, A. R., and N.D.JR. Belnap, Entailment Vol.1, Princeton university press, 1975.

[3] Corsi, G., Weak logics with strict implication. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 33 (1987) 389 - 406.

[4] Došen, K., Sequent systems and groupoid models. I. Studia Logica 47 (1988) 353 - 385.

[5] Došen, K., Sequent systems and groupoid models. II. Studia Logica 48 (1988) 41 - 65.

[6] Ishihara, H., A canonical model construction for substructural logics. Journal of Universal Computer Science 6 (2000) 155 - 168.

[7] Méndez, J M., A Routley-Meyer semantics for converse Ackermann property. Journal of Philosophical Logic 16 (1987) 65 - 76.

[8] Nelson, D., Constructible falsity. Journal of Symbolic Logic 14 (1949) 16 - 26.

[9] Ono, H., A note on Visser’s basic propositional logic. manuscript, 1997.

[10] Ono, H., and Y. Komori, Logics without the contraction rule. Journal of Symbolic Logic 50 (1985) 169 - 201.

[11] Suzuki, Y., and H. Ono, Hilbert style proof system for BPL. Research Report, Japan Advanced Institute of Science and Technology, 1997.

[12] Thomason, H., A semantical study of constructible falsity. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 15 (1969) 247 - 257.

[13] Visser, A., A propositional logic with explicit fixed points. Studia Logica 40 (1981) 155 - 174.

[14] Wansing. H., Informational interpretation of substructural propositional logics. Journal of Logic, Language and Information 2 (1993) 285 - 308.