Proof Theoretical Studies on Semilattice Relevant Logics

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

                         kashima@is.titech.ac.jp

This is the first section of the Research Report (No. C-157, Department of Mathematical and Computing Sciences, Tokyo Institute of Technology):

           http://www.is.titech.ac.jp/research/research-report/C/C-157.ps.gz

1 Introduction

Relevant logics which are defined by “semilattice models” are called semilattice relevant logics; they have been studied in the literature, e.g., [3, 4, 5, 8, 9]. A typical semilattice relevant logic ^{∪}R is defined to be the set of formulas that are valid in any ^{∪}R-models, where a ^{∪}R-model ⟨I, ·, e⟩ is a semilattice with identity e (i.e., ⟨I, ·, e⟩ is an idempotent commutative monoid). This structure can be 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. The notion “α ⊧ A” (a formula A holds according to a piece α of information) is inductively defined in a natural way:

α ⊧ A→B ⟺ ∀β ∈ I [(β ⊧ A) ⇒ (α·β ⊧ B)].
α ⊧ A∧B ⟺ (α ⊧ A) and (α ⊧ B).
α ⊧ A∨B ⟺ (α ⊧ A) or (α ⊧ B).

(In this paper, formulas are constructed by the connectives → (implication), ∧ (conjunction) and ∨ (disjunction).) We say that a formula A is valid in the model if and only if e ⊧ A.

In addition to ^{∪}R, the semilattice relevant logics ^{∪}T, ^{∪}RW, and ^{∪}TW appear in this paper, where they are obtained by modifying the definition of ^{∪}R-model and/or the definition of “⊧” as follows. The definition of “α ⊧ A→B” in ^{∪}T/^{∪}TW-models is described as

∀β ⪰ α [(β ⊧ A) ⇒ (α·β ⊧ B)]

where ⪰ is a binary relation on I, and ^{∪}RW/^{∪}TW-models are commutative monoids without the idempotence postulate: α·α = α.

A point of semilattice models is that “α ⊧ A ⇒ α·β ⊧ A” is not always true, which reflects the principle of relevant logics—adding an irrelevant assumption (β) makes a fall of truth value. This excludes “paradoxical” formulas, e.g., A→(B→A), while acceptable formulas such as A→A, (A∧B)→A, A→(A∨B) and (A∧(B∨C))→((A∧B)∨C) are valid in any semilattice models. Moreover, there are some marginal formulas that correspond to some postulates on models. For example, the formula (A→(A→B))→(A→B) corresponds to the idempotence postulate: this formula is not in ^{∪}RW or ^{∪}TW while it is in ^{∪}R and ^{∪}T. (Since this formula is called contraction, the logics ^{∪}RW and ^{∪}TW are also called contractionless logics.) These examples show an advantage of semilattice models: various features of relevant logics are represented by simple devices of models.

The “orthodox” relevant logics (see, e.g., [1, 2]) and the semilattice relevant logics coincide in the {→, ∧}-fragments, but they have a slight difference if the connective ∨ exists. For example, it is known ([9]) that R_{→∧∨} ⊊ ^{∪}R where R_{→∧∨} is the set of provable formulas in the {→, ∧, ∨}-fragment of the well-known relevant logic R. The orthodox relevant logics are usually defined by their proof systems, and models of them are relatively complicated. On the other hand semilattice relevant logics are defined by simple models; then development of proof theoretical studies is a natural requirement for semilattice relevant logics. This paper is a study in such a direction.

The results of this paper are summarized as follows.

1. Equivalence between the LK-style and LJ-style labelled sequent calculi. For the logic ∪R, there is a cut-free labelled sequent calculus, called LK^{∪}R, where the labels α, β, … are finite sets, and the both sides of a sequent are multisets of labelled formulas.

Axioms of LK^{∪}R: α:A ⇒ α:A

Inference rules of LK^{∪}R:

• The weakening/contraction rules for both side. For example:

\begin{matrix}Γ ⇒ Δ \\ α:A, Γ ⇒ Δ \end{matrix} (weakening left) \begin{matrix}Γ ⇒ Δ, α:A, α:A \\ Γ ⇒ Δ, α:A \end{matrix} (contraction right)

• Rules for →:

\begin{matrix}Γ ⇒ Δ, β:A & α∪β:B, Π ⇒ Σ \\ α:A→B, Γ, Π ⇒ Δ, Σ \end{matrix} (→ left) \begin{matrix}\{a\}:A, Γ ⇒ Δ, α∪\{a\}:B \\ Γ ⇒ Δ, α:A→B \end{matrix} (→ right)

where a does not appear in the lower sequent of “→ right”.

• Rules for ∧ and ∨. For example,

\begin{matrix}α:A, Γ ⇒ Δ & α:B, Γ ⇒ Δ \\ α:A∨B, Γ ⇒ Δ \end{matrix} (∨ left) \begin{matrix}Γ ⇒ Δ, α:A \\ Γ ⇒ Δ, α:A∨B \end{matrix} (∨ right)

(Rules for ∧ are the dual forms of the ones for ∨.)

This system is known to be complete in the following sense: A ∈ ^{∪}R if and only if LK^{∪}R ⊢ ⇒ ∅:A (i.e., the sequent ⇒ ∅:A is provable in LK^{∪}R). On the other hand, there is another labelled sequent calculus, called LJ^{∪}R, that is defined from LK^{∪}R by imposing the restriction that the right-hand side of each sequent is a singleton. (The names LK^{∪}R and LJ^{∪}R come from the well-known sequent calculi LK for the classical logic and LJ for the intuitionistic logic, where LK and LJ are equivalent to the label-free parts of LK^{∪}R and LJ^{∪}R, respectively.) In this paper, we prove that LK^{∪}R is a conservative extension of LJ^{∪}R (although LK is not a conservative extension of LJ); therefore the following three conditions are shown to be equivalent: (1) A ∈ ^{∪}R. (2) LK^{∪}R ⊢ ⇒ ∅:A. (3) LJ^{∪}R ⊢ ⇒ ∅:A. Moreover, similar results for ^{∪}T, ^{∪}RW, and ^{∪}TW are proved. These are shown with a delicate transformation of sequent-proofs. Note that these results were already stated in [5], but the proof there was wrong (see the beginning of Section 3).

2. Hilbert-style axiomatization of ^{∪}R/^{∪}T. We prove that Hilbert-style systems for ^{∪}R and ∪T are obtained from the orthodox systems R and T by adding an extra inference rule. In [3], such a result for ^{∪}R has been proved where the extra rule is slightly different from this paper. Our extra rule corresponds to the “∨ left” rule of LJ^{∪}R, and our proof method is “translation of LJ^{∪}R(^{∪}T)- sequents into formulas”, which is clearer than the method of [3]. For ^{∪}T, no other completeness proof for Hilbert-style systems has been known. Unfortunately we do not yet get such a result for ^{∪}RW/^{∪}TW.

3. Equivalence between the commutative monoid semantics and the distributive semilattice semantics for ^{∪}RW/^{∪}TW. In [4, 5, 8], two kinds of models are introduced for ^{∪}RW/^{∪}TW: one is “commutative monoid” and the other is “distributive semilattice”. In this paper we introduce labelled sequent calculi for both semantics. Then, by the analysis of these systems, we show the equivalence of the two semantics in the sense that a formula A is valid in any commutative monoid models if and only if A is valid in any distributive semilattice models. This equivalence for ^{∪}RW and for the {→, ∧}-fragment of ∪TW have been proved in [4, 8] (where the proof methods are different from this paper), but the result for ^{∪}TW with the connective ∨ has not been proved so far.

Thus our results are classified into three, where the first one is a fundamental result on the proof theory of the semilattice relevant logics and the second and third ones solve some open problems, making good use of the first result. We hope that some more important property on the semilattice relevant logics will be shown by virtue of the fundamental result; for example, a decision procedure for ^{∪}R(^{∪}T) with the cut-free system LJ^{∪}R(^{∪}T) is an attractive goal. (It is open whether they are decidable or not.) We also hope to extend these results to other relevant logics, for example, E and the neighbors appearing in [6].

The structure of this paper is as follows. In Section 2, we present the definitions of the semilattice relevant logics ^{∪}R and ^{∪}T with the semilattice models. Then we introduce the labelled sequent calculi LK^{∪}R and LK^{∪}T, and we prove the completeness of them. In Section 3, we introduce the labelled sequent calculi LJ^{∪}R and LJ^{∪}T, and we prove that LK^{∪}R (or LK^{∪}T) is a conservative extension of LJ^{∪}R (or LJ^{∪}T, respectively). In Section 4, we show that LJ^{∪}R and LJ^{∪}T can be changed into systems without the “weakening” rule. These systems are called LI^{∪}R and LI^{∪}T, which are proved, in Section 5, to be sound with respect to the semilattice models. The results of Sections 2–5 imply the Main Theorem 5.4, which claims the equivalence between the conditions: A ∈ X, LKX ⊢ ⇒ ∅:A, LJX ⊢ ⇒ ∅:A, and LIX ⊢ ⇒ ∅:A, for X ∈ {^{∪}R,^{∪}T}. In Section 6, we present Hilbert-style systems for ^{∪}R and ^{∪}T, and we show the soundness and completeness of them. In Section 7, we investigate the logics ^{∪}RW and ^{∪}TW. We introduce two kinds of labelled sequent calculi which reflect the two kinds of models (commutative monoid and distributive semilattice). All the results of Sections 2–5 are translated for ^{∪}RW/^{∪}TW, and then we obtain the equivalence between the two semantics.

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] S. Giambrone, R. K. Meyer and A. Urquhart, A contractionless semilattice semantics, Journal of Symbolic Logic 52, 526-529, (1987).

[5] S. Giambrone and A. Urquhart, Proof theories for semilattice logics, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 33, 433-439, (1987).

[6] R. Kashima, Completeness of Implicational Relevant Logics, Logic Journal of the Interest Group in Pure and Applied Logics 8 761-785, (2000).

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

[8] R. K. Meyer, S. Giambrone, A. Urquhart and E. P. Martin, Further results on proof theories for semilattice logics, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 34, 301-304, (1988).

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