Alternatives to the relevant logic R

Ryo Kashima

                         kashima@is.titech.ac.jp

Department of Mathematical and Computing Sciences Tokyo Institute of Technology

We study two relevant logics^{∪}R_{+} and RNND, which are proper extensions of the well-known relevant logic R. The logic ^{∪}R_{+} (“semilattice relevant logic”) has connectives → (implication), ∧ (conjunction), and ∨ (disjunction), and is characterized by semilattice models in which ∧ and ∨ are interpreted in a natural way. The logic RNND (“Relevant Normal Natural Deduction”) has connectives →, ∧, ∨, and ¬ (negation), and is formulated by a natural deduction system which is quite simple and easy to understand as compared with the usual natural deduction system of R. We try to show some nice properties of ^{∪}R_{+} and RNND — decidability, variable sharing, etc.

1 Semilattice Relevant Logic

In this note, the formulas of the relevant logic R are constructed by {→, ∧, ∨, ¬}. If c is a list of connectives in {→, ∧, ∨, ¬}, then F_{c} will denote the set of formulas whose connectives are in c, and R_{c} will denote the c-fragment of R.

A semilattice model is a 4-tuple ⟨I, ·, e, ⊧⟩ that satisfies the following.

• ⟨I, ·, e⟩ is an idempotent commutative monoid (a semilattice with identity e). That is,

I is a non-empty set, · is a binary operator on I, e ∈ I. (α·β)·γ = α·(β·γ), α·β = β·α, α·α = α, α·e = α.

• ⊧ is a relation on I × F_{→∧∨} such that

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

We say that a formula A is valid in this model if e ⊧ A. (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 notion α ⊧ A is considered to be a fact “a formula A holds according to a piece α of information”.)

The “semilattice relevant logic” ^{∪}R_{+} is defined to be the set

{A ∈ F_{→∧∨} | A is valid in any semilattice model}.

Proposition 1.1 ([6]) ^{∪}R_{+} is a proper superset of the set of provable formulas in R_{→∧∨} while the →-fragment of ^{∪}R_{+} coincides with R_{→}. For example,

[(A→(B∨C))∧(B→D)]→(A→(D∨C)) ∈ ^{∪}R_{+}, ∉ R_{→∧∨}.

If α is a finite set of natural numbers and A is a formula, then the expression α:A is called a labelled formula (α is called a label). If Γ and Δ are finite multisets of labelled formulas, then the expression Γ ⇒ Δ is called a labelled sequent. A labelled sequent calculus L^{∪}R_{+} is defined as follows.

[Axioms]

Γ , α:A ⇒ α:A, Δ

[Inference rules]

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

(Label Condition) The natural number a does not appear in the labels of the lower sequent.

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

Proposition 1.2 ([4](cf.[5])) A ∈ ^{∪}R_{+} if and only if L^{∪}R_{+} ⊢ ⇒ ∅:A.

The system L^{∪}R′_{+} is obtained from L^{∪}R_{+} by replacing “→ left” rule by

\begin{matrix}Γ ⇒ β:A & Γ , α∪β:B ⇒ Δ \\ Γ , α:A→B ⇒ Δ. \end{matrix} (→ left′)

We can (probably) prove: Theorem 1.3 L^{∪}R_{+} and L^{∪}R′_{+} are equivalent with respect to provable labelled sequents. By using this theorem, now I attack the following problems.

• Give a simple proof of the completeness of a Hilbert style axiomatization of ^{∪}R_{+}. (A Hilbert style axiomatization of ^{∪}R_{+} was given by Charlwood ([2]), but the proof is somewhat complicated, and I cannot follow the detail.)

• Decision problem of ^{∪}R_{+}. (I try to make a decision procedure for R_{→} using the →-fragment of L^{∪}R_{+}. This and the above Theorem 1.3 may offer a decision procedure for ^{∪}R_{+}.)

• Prove (or disprove) the variable sharing (and the interpolation) property for ^{∪}R_{+}. Remark

• A decision procedure for “contractionless ^{∪}R_{+}” was given by Giambrone and Kron ([3]).

• Giambrone and Urquhart ([4]) introduced a natural deduction system and “proved” that the system is equivalent to L^{∪}R_{+}. However, the proof seems to be wrong—(A∨B)_{a} ⊢ A_{a}, B_{a} is (probably) a counterexample to Fact 6 in [4].

2 Relevant Normal Natural Deduction

The natural deduction system of R_{→} is quite simple:

\begin{matrix}A→B & A \\ B \end{matrix} (→E)  [A] ; ⋮ . ; B ; A→B (→I) with a condition:

(Relevant Condition) We must cancel at least one occurrence of the assumption A.

But introducing other connectives makes the situation problematic. For example, an irrelevant formula B→(A→A) is provable by the proof

\begin{matrix}[A]^{1} & [B]^{2} \\ A∧B \end{matrix} ; A ; A→A ; 1 ; B→(A→A) 2

which satisfies the Relevant Condition. To avoid such a situation, Yoshiura and Yonezaki ([7]) introduced a natural deduction system in which only “normal proofs” are permitted. This is a nice idea, but Yoshiura and Yonezaki’s system is not elegant in the treatment of negation. Here we combine Yoshiura and Yonezaki’s idea with Andou’s “regular and normal proofs” ([1]), and we make an elegant natural deduction system of a relevant logic.

Remark

• The above proof of B→(A→A) is not normal, and the normal form of it violates the Relevant Condition.

• Usually natural deduction systems of R have a restriction on ∧I rule—two premises must have the same assumption set. This excludes the above proof of B→(A→A).

Andou’s regular NK for F_{→∧∨¬}

[A] ; ⋮ . ; B ; A→B (→I)  \begin{matrix}A→B & A \\ B \end{matrix} (→E)  \begin{matrix}A & B \\ A∧B \end{matrix} (∧I)  {A∧B \atop A} (∧E)  {A∧B \atop B} (∧E)

{A \atop A∨B} (∨I)  {B \atop A∨B} (∨I)  \begin{aligned}A∨B & [A] ; ⋮ . ; C & [B] ; ⋮ . ; C \\ & C \end{aligned} (∨E)  [A] ; ⋮ . ; ⊥ ; ¬A (¬I)  \begin{matrix}¬A & A \\ ⊥ \end{matrix} (¬E)

\begin{matrix}[¬A] & ⋮ . ; A \\ ⊥ \end{matrix} ; ⋮ . ; ⊥ ; A ; (⊥C)

The ⊥C rule means that an assumption which is cancelled by ⊥C must be the major premise of a ¬E.

Let ⟨X_{1}, ⋯, X_{n}⟩ be a path in a proof of regular NK (X_{1} is an assumption and X_{n} is the last formula), and ⟨Y_{1}, ⋯, Y_{m}⟩ be a subsequence of it (i.e., ⟨Y_{1}, ⋯, Y_{m}⟩ = ⟨X_{i_{1}}, ⋯, X_{i_{m}}⟩ where i_{1} < ⋯ < i_{m}). We say that the sequence ⟨Y_{1}, ⋯, Y_{m}⟩ is redundant if it satisfies the following conditions.

• Y_{1} is the conclusion of an “introduction rule” (→I, ∧I, ∨I, or ¬I).

• The position of Y_{k} and Y_{k+1} is one of the following.

\begin{aligned}⋮ . ; A∨B & [A] ; ⋮ . ; Y_{k} & [B] ; ⋮ . ; C \\ & Y_{k+1} \end{aligned} (∨E) ; ⋮ .  \begin{aligned}⋮ . ; A∨B & [A] ; ⋮ . ; C & [B] ; ⋮ . ; Y_{k} \\ & Y_{k+1} \end{aligned} (∨E) ; ⋮ .  \begin{matrix}[¬A] & ⋮ . ; Y_{k} \\ ⊥ \end{matrix} ; ⋮ . ; ⊥ ; Y_{k+1} ; (⊥C) ; ⋮ .

• Y_{m} is the major premise of an “elimination rule” (→E, ∧E, ∨E, or ¬E).

A proof is said to be normal if it contains no redundant sequence, and to be relevant if the Relevant Condition on cancelling assumptions holds (i.e., in the applications of the rules →I, ∨E, ¬I, and ⊥C, there must be an occurrence of each cancelled assumption indicated by [A], [B], and [¬A] in the above list of the rules).

The logic RNND (Relevant Normal Natural Deduction) is defined by relevant normal proofs; that is, a formula A is said to be a theorem of RNND if there is a regular NK proof of A which is relevant and normal.

Now I attack the problem to show the following nice properties of RNND. (For Yoshiura and Yonezaki’s system, these have been shown by [7], [8] and [9].)

• Variable sharing (and interpolation).

• Decidability.

• RNND is strictly stronger than R. (There are some “natural” formulas which are provable in RNND and not provable in R; e.g., A→(B→(A∧B)). On the other hand, I do not know whether the following holds: If R ⊢ A then RNND ⊢ A. This is a nontrivial problem because RNND is not closed under modus ponens.)

References

[1] Y. Andou, A normalization-procedure for the first order classical natural deduction with full logical symbols, Tsukuba Journal of Mathematics 19, 153-162, (1995).

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

[3] S. Giambrone and A. Kron, Four relevant Gentzen systems, Studia Logica 46, 54-71 (1987).

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

[5] R. Kashima, Completeness of implicational relevant logics, Logic Journal of the Interest Group in Pure and Applied Logics 8, 761-785 (2000).

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

[7] N. Yoshiura and N. Yonezaki, Relevant logic ER with extended provability (in Japanese), Journal of Japanese Society for Artificial Intelligence 13, 981-989, (1998). (吉浦紀晃, 米崎直樹: 証明力を拡張した適切さの論理 ER，人工知能学会誌)

[8] N. Yoshiura and N. Yonezaki, Decidability of relevant logic ER (in Japanese), Journal of Japanese Society for Artificial Intelligence 14, 819-827, (1999). (吉浦紀晃, 米崎直樹: 適切さの論理 ER の決定可能性，人工知能学会誌)

[9] N. Yoshiura and N. Yonezaki, Comparison of relevant logic R and ER (in Japanese), Journal of Japanese Society for Artificial Intelligence 14, 1088-1099, (1999). (吉浦紀晃, 米崎直樹: 適切さの論理 R と ER の証明力の比較，人工知能学会誌)