Labelled Sequent Calculi and Completeness Theorems for Implicational Relevant Logics

Ryo Kashima

Department of Mathematical and Computing Sciences Tokyo Institute of Technology Ookayama, Meguro, Tokyo 152-8552, Japan.

                             e-mail: kashima@is.titech.ac.jp

This is the first section of the research report “Labelled Sequent Calculi and Completeness Theorems for Implicational Relevant Logics” (No. C-140, Department of Mathematical and Computing Sciences, Tokyo Institute of Technology).

1 Introduction

A natural semantic treatment of relevant logics was given by Urquhart [10]. (See [1], [2] and [4] for information on relevant logics.) Let E be the implicational fragment of the relevant logic E. (In this paper, we treat only “→” (implication) as a logical symbol; therefore, E/R/S4⋯ will denote the implicational fragments of themselves.) An Urquhart’s model for E (we call it an E-model) consists of two structures ⟨I, ·, e⟩ and ⟨W, R⟩ where the former is an idempotent commutative monoid (i.e., semilattice with identity e) and the latter is a quasi-ordered set (i.e., R is a reflexive and transitive relation on W). The structure ⟨I, ·, e⟩ is considered to be a “structure of information”—I is a set of pieces of information, · is a binary operator which combines two pieces of information, and e is an empty piece of information; and the structure ⟨W, R⟩ is, like a Kripke’s model for modal logics, considered to be a “structure of possible worlds”—W is a set of worlds, and R is an accessibility relation. The notion “α, x ⊧ A” (a formula A holds according to a piece α of information at a world x) is inductively defined by the following.

α, x ⊧ B→C ⟺ ∀β ∈ I, ∀y ∈ W [(xRy) & (β, y ⊧ B) ⇒ (α·β, y ⊧ C)].

We say that a formula A is valid in the model if e, x ⊧ A for any x ∈ W. The completeness theorem, which was shown in [10] (a proof appeared in [2]), claims that a formula A is provable in E if and only if A is valid in any E-model.

The relevant logic R and the logic S4 of “strict implication” are obtained from E by adding, respectively, the axiom schemes

C: (A→(B→C))→(B→(A→C)), and
K^{01}: \overrightarrow{A}→(B→\overrightarrow{A})

where \overrightarrow{A} is an abbreviation for A_{1}→A_{2}; and the intuitionistic logic Int is obtained from E by adding both the schemes C and K^{01} (or, equivalently, Int is obtained from R by adding the scheme K: A→(B→A)). (See, e.g., [1] and [9] for axiomatizations of these logics. The name K^{01} comes from [9], where the superscripts represent certain restrictions by “over-arrows”.) The completeness theorems for these logics were shown as follows. We define two conditions on E-models:

(Single World Condition) The set of possible worlds is a singleton.

(Hereditary Condition) If α, x ⊧ A, then α·β, x ⊧ A.

Then, the logic (R / S4 / Int) is complete with respect to the class of E-models satisfying the condition (Single World / Hereditary / both Single World and Hereditary, respectively). That is, for example, a formula A is provable in Int if and only if A is valid in any E-model that satisfies both the Single World and Hereditary Conditions.

Moreover, such completeness results were shown for other two relevant logics—called E5 and RM0 (the names come from [5] and [1]).

The logic E5 is obtained from E by adding the axiom scheme

C^{001}: (A→(B→\overrightarrow{C}))→(B→(A→\overrightarrow{C})).

(In [5] and [10], the axiom scheme B→((B→\overrightarrow{C})→\overrightarrow{C}) was adopted where this scheme and C^{001} are mutually inferable over E.) The scheme C^{001} is an instance of the scheme C, and therefore E5 is an intermediate logic between E and R. It was shown that the logic E5 is complete with respect to the class of E-models satisfying the following condition.

(Single Cluster Condition) The accessibility relation is universal, that is, xRy for any x, y ∈ W.

Note that this condition is weaker than the Single World Condition.

The logic RM0 is obtained from R by adding the axiom scheme

M: A→(A→A).

This scheme is an instance of the scheme K, and therefore RM0 is an intermediate logic between R and Int. It was shown that the logic RM0 is complete with respect to the class of E-models satisfying both the Single World Condition and the following condition.

(Mingle Condition) If α, x ⊧ A and β, x ⊧ A, then α·β, x ⊧ A.

Note that the Mingle Condition is weaker than the Hereditary Condition.

[figure: Figure 1; E; EM^{#}; S4; E5; E5M^{#}; S5I; R; RM0; Int; +M^{#}; +K^{01} (K^{01}); +C^{001}; +C; Mingle Condition; Hereditary Condition; E-models /; Linear Order E-models; Single Cluster E-models; Single World E-models]

To sum up, it has been shown that the six logics E, E5, R, RM0, Int, and S4, which are located on the edges of the diagram in Figure 1, are complete with respect to the class of E-models with the additional conditions. (See [2], [5] and [10] for the proofs.) Then, bringing the diagram to completion is a natural requirement. In other words, there are two questions: (Q1) Is there an axiom scheme A that satisfies the following?

• The logic E+A is complete with respect to the class of E-models satisfying the Mingle Condition.

• The logic E5+A is complete with respect to the class of E-models satisfying both the Single Cluster Condition and the Mingle Condition.

• The logic R+A is equivalent to RM0.

(Q2) Is the logic S5I = S4+C^{001} complete with respect to the class of E-models satisfying both the Single Cluster Condition and Hereditary Condition? (We will account for the name S5I later.)

This paper gives positive answers to these questions. (It is somewhat surprising that such a natural question has been open.) For Q1, the required scheme A is

M^{#}: (\overrightarrow{A}→B)→(\overrightarrow{A}→(B→B)),

and the logics E+M^{#} and E5+M^{#} are denoted by EM^{#} and E5M^{#}, respectively. (Note that M^{#} is an instance of the scheme

K^{01}: (\overrightarrow{A}→B)→(\overrightarrow{A}→(C→B))

while this scheme and K^{01} are mutually inferable over E; see Section 2.) Moreover we show a strong version of the completeness of E/EM^{#}/S4, which claims that these logics are complete with respect to the linear order E-models. That is, for example, a formula A is provable in S4 if and only if A is valid in any E-model in which the accessibility relation is a linear order and the Hereditary Condition holds. These complete the diagram in Figure 1, which shows a nice correspondence between simple axiom schemes and natural conditions on models.

An outline of the proof of the completeness is as follows. For each logic X = E, EM^{#}, …, we introduce two systems GX and LX. The system GX is an ordinary “sequent calculus”, and it is easy to show that a “sequent” A_{1}, …, A_{n} ↦ B is provable in GX if and only if the formula A_{1}→(⋯ →(A_{n}→B) ⋯) is provable in X. The system LX is a “labelled sequent calculus”, that is, a system to treat “labelled sequents”—sequents consisting of labelled formulas where a label reflects the structure of E-models. By a standard way, we show that LX is complete with respect to the class of E-models satisfying the additional conditions for X. In particular, if a formula A is valid in any E-model of X, then the labelled sequent “⇒ (∅, 0):A”, which consists of A and the “empty label” (∅, 0), is provable in LX. Then, the following claim completes the proof of the completeness.

If the labelled sequent ⇒ (∅, 0):A is provable in LX, then the unlabelled sequent ↦ A is provable in GX.

This is proved by showing a stronger claim:

If a labelled sequent S is provable in LX, then an unlabelled sequent T is provable in GX where T is “extracted” from S in a certain way.

Since unlabelled sequents have less expressive power than labelled sequents, this “extraction” is somewhat complicated; and proving this claim is the hardest (and the most interesting) part of the proof of the completeness theorem. There have been a lot of studies on labelled sequent calculi (e.g. see [7] and [8]). Among them, the author thinks, this paper is a good example of an application of labelled sequent calculi to solve important problems on the logics, which are independent from the labelled systems.

The completion of the diagram in Figure 1 induces further questions, for which the author does not have any nontrivial answers now: (1) There are a lot of possible conditions on E-models. Is there a corresponding axiom scheme for each condition? For example, if the models lack the condition α·α = α (idempotence), the corresponding logics might be axiomatized by deleting the scheme W: (A→(A→B))→ (A→B). Is this true for each logic in the diagram? (2) Introducing other connectives (∧, ∨, ¬, …) is an important problem. It was shown ([3], [6]) that the logic R_{→∧∨} with an extra inference rule is complete with respect to the class of models of R in which ∧ and ∨ are interpreted in a natural way. What happens for the other logics in the diagram?

If we get acceptable answers for these questions, Urquhart’s semantics will be a major paradigm of “possible worlds semantics”, while Routley-Meyer’s “ternary relation semantics” (see, e.g., [2] or [4]) is major now. The diagram in Figure 1 is a starting point.

We make remarks about the scheme M^{#} and the logic S5I. In literature (see, e.g., [1] or [4]), the axiom scheme M′: \overrightarrow{A}→(\overrightarrow{A}→\overrightarrow{A}) was suggested as a “Mingle for E”. But the author thinks the scheme M^{#} is the very axiom of “Mingle for E” because of its completeness with respect to the class of E-models satisfying the Mingle Condition. (M′ is inferable from M^{#} (by B:= \overrightarrow{A}), but the author does not know whether the converse holds.) The name S5I comes from [8]. In [8], a sequent style system for S5I was introduced, whereas the Hilbert style axiomatization S4+C^{001} did not appear. The name S5I reflects the fact that the models of this logic are considered to be the intuitionistic variants of the models for “S5 strict implication”. We will discuss this fact in Section 3.

The plan of this paper is as follows. Let X = {E, EM^{#}, S4, E5, E5M^{#}, S5I} (the six logics in the bottom and the middle rows in Figure 1). In Section 2, we introduce implicational relevant logics by Hilbert-style axiomatizations; and then we introduce six Gentzen-style sequent calculi named GX for X ∈ X. In Section 3, we define the E-models and prove that the Hilbert-style systems are sound with respect to the class of E-models with the additional conditions. In Section 4, we introduce labelled sequent calculi named LX for X ∈ X, and prove their completeness with respect to the class of E-models with the additional conditions. In Section 5, we show the “extraction” from the labelled sequent calculi LX into the unlabelled sequent calculi GX. Finally, in Section 6, we state the main results of this paper—completeness of the six logics in X.

References

[1] A. R. Anderson and N. D. Belnap Jr., Entailment: The Logic of Relevance and Necessity, Vol. 1, (Princeton 1975).

[2] A. R. Anderson, N. D. Belnap Jr. and J. M. Dunn. Entailment: The Logic of Relevance and Necessity, Vol. 2, (Princeton 1992).

[3] G. Charlwood, An axiomatic version of positive semilattice relevance logic, Journal of Symbolic Logic 46, 233-239 (1981).

[4] J. M. Dunn, Relevance Logic and Entailment, in Handbook of Philosophical Logic, Vol. III (edited by D. Gabbay and F. Guenthner) (D. Reidel 1986).

[5] K. Fine, Completeness for S5 analogue of E_{I} (abstract), Journal of Symbolic Logic 41, 559-560 (1976).

[6] K. Fine, Completeness for the semilattice semantics with disjunction and conjunction (abstract), Journal of Symbolic Logic 41, 560 (1976).

[7] D. M. Gabbay, Labelled Deductive Systems, Vol.1, (Oxford 1996).

[8] D. M. Gabbay and N. Olivetti, Algorithmic proof methods and cut elimination for implicational logics, part I, Studia Logica 61, 237-280 (1998).

[9] R. Kashima and N. Kamide, Substructural implicational logics including the relevant logic E, Studia Logica 63, 181-212, (1999).

[10] A. Urquhart, Semantics for relevant logics, Journal of Symbolic Logic 37, 159-169 (1972).