PUBLICATIONS DE L’INSTITUT MATHÉMATIQUE Nouvelle série, tome 82(96) (2007), 55–78 DOI 102298/PIM0796055I

THEOREM PROVERS FOR SUBSTRUCTURAL LOGICS

Mirjana Isaković Ilić

Abstract. We describe theorem provers for some decidable propositional substructural logics.

1. Introduction

Sequent systems for intuitionistic and classical predicate logic, namely LJ and LK, were introduced by Gentzen in [2]. The basic expression of those systems is a ‘sequent’ Γ ⊢ Δ, where Γ and Δ are finite sequences of formulae. Γ is the antecedent and Δ is the succedent of Γ ⊢ Δ. If Δ is a single or an empty sequence, then Γ ⊢ Δ is a single-conclusion sequent, otherwise, it is a multiple-conclusion sequent.

Each rule in LJ and LK is either an operational rule or a structural rule. Operational rules introduce new logical connectives to the left-, or to the right-hand side of the turnstile ⊢. On the other hand, structural rules refer to the structure of the sequents and they do not involve any logical symbol, of the language to which belong sequent-formulae, in their formulation. Gentzen’s structural rules are:

Weakening:  Contraction:
\frac{Γ ⊢ Δ}{α, Γ ⊢ Δ} , \frac{Γ ⊢ Δ}{Γ ⊢ Δ, α};  \frac{α, α, Γ ⊢ Δ}{α, Γ ⊢ Δ} , \frac{Γ ⊢ Δ, α, α}{Γ ⊢ Δ, α};
Permutation:  Cut:
\frac{Γ_{1}, α, β, Γ_{2} ⊢ Δ}{Γ_{1}, β, α, Γ_{2} ⊢ Δ} , \frac{Γ ⊢ Δ_{1}, α, β, Δ_{2}}{Γ ⊢ Δ_{1}, β, α, Δ_{2}} ;  \frac{Γ_{1} ⊢ Δ_{1}, α  α, Γ_{2} ⊢ Δ_{2}}{Γ_{1}, Γ_{2} ⊢ Δ_{1}, Δ_{2}} .

Substructural logics are logics whose sequent formulations can be obtained from Gentzen’s system LK by rejecting or restricting some of Gentzen’s structural rules.

2000 Mathematics Subject Classification: Primary 03F05; Secondary 03F52.

Key words and phrases: Substructural logics; Automated deduction.

We shall consider both, single- and multiple-conclusion sequent systems^{1} for BCK, relevant^{2}, linear^{3}, Lambek and Lambek logic with weakening. Furthermore, we shall mention sequent systems for intuitionistic logic^{4} and classical logic.

A sequent system for BCK logic can be obtained from the sequent system for classical logic by rejecting contraction, for relevant logic, by rejecting thinning and, for linear logic, by rejecting both thinning and contraction. Since in the presence of permutation, the position of a formula within Γ and within Δ in Γ ⊢ Δ is irrelevant, we use multisets Γ and Δ, to define a sequent Γ ⊢ Δ, in the above systems.

A sequent system for Lambek logic is without any structural rules, other than cut.^{5} We use sequences of formulae Γ and Δ to define Γ ⊢ Δ in sequent systems for both Lambek logic and Lambek logic with weakening.

In sequent systems for intuitionistic and classical logics (i.e., in the presence of all Gentzen’s structural rules), Γ and Δ in Γ ⊢ Δ are sets of formulae.

In the absence of some (or all) of Gentzen’s structural rules, classically equivalent connectives and constants split into nonequivalent dual pairs. Therefore, the rejection of contraction and/or weakening, produces two conjunctions: additive (∧) and multiplicative one (·). (We may have two implications, also: multiplicative (→) and additive (↪) one; however, in our sequent systems additive implication is definable, therefore it is not considered.) Only in multiple-conclusion sequent systems, we also have two disjunctions: additive (∨) and multiplicative one (+). Furthermore, in the absence of permutation, we have two multiplicative implications: → and ← (and accordingly, two definable negations: ∼α = α → 0 and ¬α = 0 ← α).

In sequent systems without weakening, we have two units, 1 and ⊤ (1 replaces the empty collection of formulae on the left-hand side of ⊢) and two zeros, also, 0 and ⊥ (0 replaces the empty collection of formulae on the right-hand side of ⊢). Algebraically, 1 and 0 behave like units for the multiplicatives · and +, respectively; ⊤ and ⊥ behave like greatest and least element in a lattice.

Cut is the only rule of Gentzen-like systems, that allows a formula which appears in premisses to disappear in a conclusion. The formula that disappears (the formula α in the formulation of cut) is called the ‘cut formula’. If the cut is an admissible rule in a sequent system (can be added to the system without increasing the stock of provable sequents) and if the application of contraction is controlled, a decision procedure for deciding of a sequent, whether or not it is provable, can be formulated.

1We shall say that a logic is a single-conclusion logic, if in its sequent formulation, starting with single-conclusion sequents, only single-conclusion sequents can be derived; a logic is a multiple-conclusion logic, if in its sequent formulation, multiple-conclusion sequents can be derived.

2By relevant logic we mean relevant logic without distribution.

3By linear logic we mean pure (i.e., without exponentials) linear logic.

4Intuitionistic logic may be considered as substructural logic, also: its sequent formulation may be obtained from LK by restricting thinning on the right, see [4]. Gentzen formulated a sequent system for intuitionistic logic, namely LJ, by restricting the language to single-conclusion sequents.

5Abrusci [1] investigated Lambek logic from the point of view of linear logic: Lambek logic is pure (i.e., without exponentials), non-commutative linear propositional logic.

Therefore, the cut-elimination theorem is the fundamental theorem of sequent systems.

Theorem 0 (Cut-Elimination Theorem). Every derivation in a sequent system GS, can be transformed into a derivation in GS, with the same endsequent and in which no cut occurs.

Unfortunately it does not hold for multiple-conclusion sequent system for both Lambek logic and Lambek logic with weakening. This means that there are sequents, which are derivable with, but not without cut. However, applications of cut in these two systems can be controlled, enabling the establishing of the decision procedure (see [3]).

We shall illustrate our tableau-based proof procedure for linear, BCK and relevant logic. First we give their sequent systems and prove soundness and completeness results with respect to corresponding algebraic structures (Section 2).

Tableau systems make the third section. In Section 4, we give the algorithm for automated theorem proving.

2. Sequent systems for linear, BCK and relevat logic

Let L be the language of the propositional calculus with the propositional constants ⊥, ⊤, 1 and 0 and binary connectives →, ←, ·, +, ∧ and ∨. Formulae of L are defined inductively, as usual. We use α, β, γ, φ, …, α_{1}, … as schematic letters for formulae of L. As usual, ∼ α is defined as an abbreviation of α → 0 and ¬α as an abbreviation of 0 ← α. The vocabulary of L plus the comma and the turnstile ⊢, makes the vocabulary of the sequent language G. Our sequent systems will be formulated in G.

CBC is the multiple-conclusion sequent system for linear logic, with the following postulates (on the left- and on the right-hand side of ⊢ are multisets of formulae):

axioms:  structural rule (cut):
α ⊢ α  (Id)
⊢ 1  (1 r)  Γ ⊢ ⊤, Δ  (⊤)
0 ⊢  (0 l)  Γ, ⊥ ⊢ Δ  (⊥)

\frac{Γ_{1} ⊢ Δ_{1}, α, Δ_{2} Γ_{2}, α, Γ_{3} ⊢ Δ_{3}}{Γ_{2}, Γ_{1}, Γ_{3} ⊢ Δ_{1}, Δ_{3}, Δ_{2}} (cut)

rules for propositional constants and connectives:

\frac{Γ_{1} ⊢ α, Δ_{1}  Γ_{2}, β ⊢ Δ_{2}}{Γ_{1}, Γ_{2}, α → β ⊢ Δ_{1}, Δ_{2}} (→ l)  \frac{Γ, α ⊢ β, Δ}{Γ ⊢ α → β, Δ} (→ r)

\frac{Γ ⊢ Δ}{Γ, 1 ⊢ Δ} (1 l)  \frac{Γ ⊢ Δ}{Γ ⊢ 0, Δ} (0 r)

\frac{Γ, α, β ⊢ Δ}{Γ, α · β ⊢ Δ} (· l)  \frac{Γ_{1} ⊢ α, Δ_{1}  Γ_{2} ⊢ β, Δ_{2}}{Γ_{1}, Γ_{2} ⊢ α · β, Δ_{1}, Δ_{2}} (· r)
\frac{Γ_{1}, α ⊢ Δ_{1}  Γ_{2}, β ⊢ Δ_{2}}{Γ_{1}, Γ_{2}, α + β ⊢ Δ_{1}, Δ_{2}} (+ l)  \frac{Γ ⊢ α, β, Δ}{Γ ⊢ α + β, Δ} (+ r)
\frac{Γ, α ⊢ Δ}{Γ, α ∧ β ⊢ Δ}  \frac{Γ, β ⊢ Δ}{Γ, α ∧ β ⊢ Δ} (∧ l)  \frac{Γ ⊢ α, Δ  Γ ⊢ β, Δ}{Γ ⊢ α ∧ β, Δ} (∧ r)
\frac{Γ, α ⊢ Δ  Γ, β ⊢ Δ}{Γ, α ∨ β ⊢ Δ} (∨ l)  \frac{Γ ⊢ α, Δ}{Γ ⊢ α ∨ β, Δ}  \frac{Γ ⊢ β, Δ}{Γ ⊢ α ∨ β, Δ} (∨ r)

The postulates of CBC_{K^{c}}, which is the multiple-conclusion sequent system for BCK logic, is obtained when we add the structural rules of weakening, i.e., the rules

from the set K^{c} = \{ \frac{Γ ⊢ Δ}{Γ, α ⊢ Δ} (k l), \frac{Γ ⊢ Δ}{Γ ⊢ α, Δ} (k r)\} to CBC. However, in the presence

of weakening, 1 ⊢ ⊤, ⊤ ⊢ 1, 0 ⊢ ⊥ and ⊥ ⊢ 0 are derivable sequents, therefore ⊤ and ⊥, together with the axioms (⊤) and (⊥), may be omitted in CBC_{K^{c}}.

The postulates of CBC_{W^{c}}, which is the multiple-conclusion sequent system for relevant logic, is obtained when we add the structural rules of contraction, i.e., the

rules from the set W^{c} =\{ \frac{Γ, α, α ⊢ Δ}{Γ, α ⊢ Δ} (w l), \frac{Γ ⊢ α, α, Δ}{Γ ⊢ α, Δ} (w r)\} to CBC.

Single-conclusion sequent systems for linear, BCK and relevant logic are obtained from the above sequent systems by the restriction to at most one formula in the succedent (note that these systems are without the connective +).

We shall prove the completeness and soundness results with respect to following algebras.

Definition 1. A structure A = ⟨A, →, ·, +, ∧, ∨, 1, 0, ⊤, ⊥⟩ is a CBC-algebra iff the set A is closed under the binary operation → and:

1. ⟨A, ∧, ∨, ⊤, ⊥⟩ is a lattice with the least element ⊥ and the greatest element ⊤ for which ⊤ = ⊥ → ⊥,

2. ⟨A, ·, 1⟩ and ⟨A, +, 0⟩ are commutative monoids with the identities 1 and 0, respectively,

3. x · (y ∨ z) = x · y ∨ x · z, x + (y ∧ z) = x + y ∧ x + z, (x ∨ y) · z = x · z ∨ y · z, (x ∧ y) + z = x + z ∧ y + z, for every x, y, z ∈A,

4. y · x ⩽ z + t iff x ⩽ y → z + t, for every x, y, z, t ∈ A, where a ⩽ b is an abbreviation for a = a ∧ b.

A CBC-algebra A satisfying x · y ⩽ x, y · x ⩽ x, x ⩽ x + y, and y ⩽ x + y, for every x, y ∈ A, is a CBC_{K^{c}}-algebra. A CBC-algebra A satisfying x ⩽ x · x and x + x ⩽ x, for every x ∈ A, is a CBC_{W^{c}}-algebra.

It is easy to show that ⩽ is a partial order on A.

Algebraic models are defined as follows.

Definition 2. Let V be the set of propositional variables of L and let F be the set of formulae of L. For a CBC-algebra A = ⟨A, →, ·, +, ∧, ∨, 1, 0, ⊤, ⊥⟩ and a basic valuation v_{0} : V → A, we define the valuation v, as follows:

1. for every α ∈ F, we define v(α) ∈ A, as follows:

v(p) = v_{0}(p), p ∈ V  v(α → β) = v(α) → v(β)
v(α · β) = v(α) · v(β)  v(α + β) = v(α) + v(β)
v(α ∨ β) = v(α) ∨ v(β)  v(α ∧ β) = v(α) ∧ v(β)
v(1) = 1  v(0) = 0
v(⊤) = ⊤  v(⊥) = ⊥

2. for every Γ ⊢ Δ, we define v(Γ ⊢ Δ) as follows (n ⩾ 1, m ⩾ 1):

v(γ_{1}, …, γ_{n} ⊢ δ_{1}, …, δ_{m}) is v(γ_{1} · . . . · γ_{n}) ⩽ v(δ_{1} + ⋯ + δ_{m})
v(γ_{1}, …, γ_{n} ⊢) is v(γ_{1} · . . . · γ_{n}) ⩽ 0
v(⊢ δ_{1}, …, δ_{m}) is 1 ⩽ v(δ_{1} + ⋯ + δ_{m})
v(⊢) is 1 ⩽ 0.

Definition 3. A CBC-model is ⟨A, v⟩, where A is a CBC-algebra and v is a valuation.

By induction on the length of proof of Γ ⊢ Δ in CBC, we can prove the following soundness lemma for CBC:

Lemma 1. If Γ ⊢ Δ is provable in CBC, then v(Γ ⊢ Δ) holds in every CBCmodel.

Proof. Let ⟨A, v⟩ be a CBC-model and let the length of proof of Γ ⊢ Δ in CBC be 1. Then Γ ⊢ Δ is an axiom. If it is of the form γ_{1}, …, γ_{n}, ⊥ ⊢ δ_{1}, …, δ_{m}, where n ⩾ 1 and m ⩾ 1, and if v(γ_{i}) = a_{i}, for every i ∈ {1, …, n}, and v(δ_{j}) = b_{j}, for every j ∈ {1, …, m}, then we wish to show that a_{1} · . . . · a_{n} · ⊥ ⩽ b_{1} + ⋯ + b_{m} holds in A. However, for a_{1} · . . . · a_{n} = a ∈ A and b_{1} + ⋯ + b_{m} = b ∈ A we have a ⩽ ⊥ → ⊥, i.e., ⊥ · a ⩽ ⊥ and a · ⊥ ⩽ ⊥ (since · is commutative) and ⊥ ⩽ b, therefore a · ⊥ ⩽ b (since ⩽ is transitive). We proceed analogously when n = 0 and/or m = 0 and also, when Γ ⊢ Δ is any other axiom in CBC.

Suppose the length of proof of Γ ⊢ Δ in CBC is greater than 1. Then Γ ⊢ Δ is the lower sequent of an inference rule, in our proof. If Γ ⊢ Δ is the lower

sequent of the rule (1 l): \frac{Γ_{1} ⊢ Δ}{Γ_{1}, 1 ⊢ Δ} (1 l), then, for Γ_{1} = γ_{1}, …, γ_{n}, n ⩾ 1 and

Δ = δ_{1}, …, δ_{m}, m ⩾ 1, and v(γ_{i}) = a_{i}, for every i ∈ {1, …, n}, and v(δ_{j}) = b_{j}, for every j ∈ {1, …, m}, we wish to show that a_{1} · . . . · a_{n} · 1 ⩽ b_{1} + ⋯ + b_{m}. However, by the induction hypothesis it follows that a_{1} · . . . · a_{n} ⩽ b_{1} + ⋯ + b_{m}. Now, since ⟨A, ·, 1⟩ is a commutative monoid and a_{1} · . . . ·a_{n} = a ∈ A and b_{1} +⋯+b_{m} = b ∈ A, we have a · 1 ⩽ b. We proceed analogously when n = 0 and/or m = 0 and also, when, in our proof, Γ ⊢ Δ is the lower sequent of any other inference rule. □

The completeness result for CBC will be proved with respect to the Lindenbaum algebra of CBC, as follows. Let |α| = {β : α ⊢ β and β ⊢ α are provable in CBC} and let |α| ∗ |β| = |α ∗ β|, for every ∗ ∈ {→, ·, +, ∨, ∧}. Note that the set |α ∗ β|, where ∗ ∈ {→, ·, +, ∨, ∧}, does not depend on the representatives of |α| and |β|. We define |α| ⩽ |β| as |α| = |α| ∧ |β|.

Let £C = {|α| : α ∈ F }. The set £C is closed under the set operations →, ·, +, ∨ and ∧ (|α| ∗ |β| = |α ∗ β| ∈ £C, for every ∗ ∈ {→, ·, +, ∨, ∧}).

Lemma 2. α ⊢ β is provable in CBC iff |α| ⩽ |β| in £C.

Proof. α ⊢ β iff

1. α ⊢ α ∧ β and α ∧ β ⊢ α (applications of (∧ l), (∧ r) and cut)
2. |α| = |α ∧ β|  (1)
3. |α ∧ β| = |α| ∧ |β|  (definition)
4. |α| = |α| ∧ |β|  (2 and 3)
5. |α| ⩽ |β|  (4, definition)
□

Definition 4. LindC = ⟨£C, →, ·, +, ∨, ∧, |1|, |0|, |⊤|, |⊥|⟩ is the Lindenbaum algebra of CBC.

Lemma 3. The Lindenbaum algebra of CBC is a CBC-algebra.

Proof. The set £C is closed under →, ·, +, ∨ and ∧, |1| ∈ £C and |0| ∈ £C, therefore it is sufficient to prove that LindC satisfies the axioms of a CBC-algebra. For example:

|α| ⩽ |β| → |γ| + |δ| iff 1. |α| ⩽ |β → γ + δ| (definition)
2. α ⊢ β → γ + δ  (1, Lemma 2)
3. β · α ⊢ γ + δ  (2, definition)
4. |β · α| ⩽ |γ + δ| (3, Lemma 2)
5. |β| · |α| ⩽ |γ| + |δ| (4, definition).

We proceed analogously for all other axioms of a CBC-algebra. □

Now, we can prove the completeness lemma for CBC.

Lemma 4. If v(Γ ⊢ Δ) is valid in every CBC-model, then Γ ⊢ Δ is provable in CBC.

Proof. Let v(Γ ⊢ Δ) be valid in every CBC-model. Noting that a Lindenbaum algebra of CBC is a CBC-algebra, we define the mapping v as follows:

v(α) = |α|, for every α ∈ F
v(γ_{1}, …, γ_{n} ⊢ δ_{1}, …, δ_{m}) is |γ_{1} · . . . · γ_{n}| ⩽ |δ_{1} + ⋯ + δ_{m}|
v(γ_{1}, …, γ_{n} ⊢) is |γ_{1} · . . . · γ_{n}| ⩽ |0|
v(⊢ δ_{1}, …, δ_{m}) is |1| ⩽ |δ_{1} + ⋯ + δ_{m}|
v(⊢) is |1| ⩽ |0|.

The mapping v is well defined and it is a valuation, since it satisfies every condition from the definition of the valuation. Therefore, ⟨LindC, v⟩ is a CBCmodel.

We show that if v(γ_{1}, …, γ_{n} ⊢ δ_{1}, …, δ_{m}), for n ⩾ 1 and m ⩾ 1, is valid in ⟨LindC, v⟩, then γ_{1}, …, γ_{n} ⊢ δ_{1}, …, δ_{m} is provable in CBC.

Suppose that v(γ_{1}, …, γ_{n} ⊢ δ_{1}, …, δ_{m}) is valid in ⟨LindC, v⟩. Then:

1. |γ_{1} · . . . · γ_{n}| ⩽ |δ_{1} + ⋯ + δ_{m}|  (definition)
2. |γ_{1} · . . . · γ_{n}| = |γ_{1} · . . . · γ_{n}| ∧ |δ_{1} + ⋯ + δ_{m}|  (1)
3. |γ_{1} · . . . · γ_{n}| = |(γ_{1} · . . . · γ_{n}) ∧ (δ_{1} + ⋯ + δ_{m})|  (2)

4. γ_{1} · . . . · γ_{n} ⊢ (γ_{1} · . . . · γ_{n}) ∧ (δ_{1} + ⋯ + δ_{m}) and

(γ_{1} · . . . · γ_{n}) ∧ (δ_{1} + ⋯ + δ_{m}) ⊢ γ_{1} · . . . · γ_{n}  (3, Lemma 2)
5. γ_{1} · . . . · γ_{n} ⊢ δ_{1} + ⋯ + δ_{m}  (4)
6. γ_{1}, …, γ_{n} ⊢ δ_{1}, …, δ_{m}  (5, cut).

We proceed analogously when v(Γ ⊢) is valid in ⟨LindC, v⟩, where Γ is a nonempty multiset, or when v(⊢ Δ) is valid in ⟨LindC, v⟩, where Δ is a non-empty multiset (note that v(⊢) is not valid in ⟨LindC, v⟩). □

We prove the soundness and completeness results for any other sequent system in a perfectly analogous way.

Cut is an admissible rule in CBC, CBC_{K^{c}}, CBC_{W^{c}} and in their single-conclu-sion variants. (In the absence of contraction, to show that every proof with a single cut, which is the last rule of the proof, can be transformed, in the same system, to a proof with the same endsequent without cuts, we proceed by induction on ⟨d, ρ⟩, lexicographically ordered, where d is the degree and ρ is the rank of our cut; in CBC_{W^{c}}, instead of cut, we eliminate mix, as above, similarly as in [2].) Therefore, in our systems, every sequent which is derivable with, is also derivable without cut. We shall use this fact in formulating corresponding tableau systems.

Permutation is only implicit rule in CBC, CBC_{K^{c}}, CBC_{W^{c}} and in their singleconclusion variants. Next, we shall define the system CBCK (and its single conclusion variant) which is equivalent to CBC_{K^{c}}, where weakening is implicit, too.

First we shall prove the following lemma.

Lemma 5. Every proof in CBC_{K^{c}} can be transformed into a proof with the same endsequent in CBC_{K^{c}}, where the upper sequent of every weakening is either an axiom or the lower sequent of another weakening.

Proof. Let S be the initial segment of a proof in CBC_{K^{c}}, with the single application of weakening, which is the last rule in S. By a straightforward induction on the length of S we can prove that S can be transformed into the proof with the same endsequent in CBC_{K^{c}}, where none application of weakening is immediately preceded either by a rule for a connective or by a rule for a constant. For example, if weakening is immediately preceded by a rule (→ r) in S, we shall use the following reduction step:

\frac{\frac{{π \atop α, Γ ⊢ β, Δ}}{Γ ⊢ α → β, Δ} (→ r)}{Γ ⊢ α → β, Δ, φ} (k r) ↦ \frac{\frac{{π \atop α, Γ ⊢ β, Δ}}{α, Γ ⊢ β, Δ, φ} (k r)}{Γ ⊢ α → β, Δ, φ} (→ r)

We proceed similarly when the upper sequent of weakening is the lower sequent of either any other rule for a connective or a rule for a constant in CBC_{K^{c}}. □

Definition 5. CBCK is the multiple-conclusion sequent system for BCK logic, whose postulates are the following axioms:

Γ, α ⊢ α, Δ (Id)
Γ ⊢ 1, Δ  (1 r)
Γ, 0 ⊢ Δ  (0 l)

together with the rules for constants and the rules for connectives of the system CBC.

Directly from Lemma 5 and the Cut-Elimination Theorem for CBC_{K^{c}} it follows that CBC_{K^{c}} and CBCK are equivalent systems (and their single conclusion variants, also). Furthermore we note that every upward derivation of Γ ⊢ Δ (where we start from Γ ⊢ Δ and apply the rules of the sequent system from the bottom up) is finite and the total number of them is finite. Therefore CBCK, CBC and their single-conclusion variants, are decidable systems: Γ ⊢ Δ is provable iff at least one of the attempted upward derivations is the proof. We should note that the same decision procedure can be applied to every cut-free, contractionless sequent system, à la Gentzen, which is either without permutation or the permutation is implicit in it.

Now we shall define the system CBCW, which is equivalent to CBC_{W^{c}}, where contraction is implicit (as well as permutation) and we shall show that CBCW is decidable. First, we shall limit applications of contraction (preserving soundness and completeness of CBC_{W^{c}}) according to Kripke’s idea [5] to allow a contraction of the conclusion of a rule, only if the same sequent could not be obtained by contracting the premises only.

We shall use limCBC_{W^{c}} to denote the system CBC_{W^{c}}, where contraction is limited as above. To show that limCBC_{W^{c}} is decidable system, we shall use techniques from [6], where the Kripke’s idea has been exploited in formulating the decision procedure for a single-conclusion sequent system for relevant logic.

It is easy to show that every sequent which is derivable in CBC_{W^{c}} is also derivable in limCBC_{W^{c}}, and vice versa. Therefore these two systems are equivalent.

It will be illustrative to see how some (upward) derivations in limCBC_{W^{c}} look like. For example, we construct the proof of α → (α → β) ⊢ α → β in limCBC_{W^{c}}, as follows:

\frac{α ⊢ α  \frac{α ⊢ α  β ⊢ β}{α, α → β ⊢ β} (→ l)}{\frac{\frac{α, α, α → (α → β) ⊢ β}{α, α → (α → β) ⊢ β} (w l)}{α → (α → β) ⊢ α → β}_{(→ r)}} (→ l)

On the other hand, we can prove (using only a finite number of steps in every upward derivation) that α · α ⊢ α ∧ α is not provable in limCBC_{W^{c}}.

α · α ⊢ α ∧ α may be:

1. the conclusion of the rule (· l), of the form: \frac{α, α ⊢ α ∧ α}{α · α ⊢ α ∧ α} (· l)

2. the conclusion of the contraction of the form: _{\frac{α · α, α, α ⊢ α ∧ α}{\frac{α · α, α · α ⊢ α ∧ α}{α · α ⊢ α ∧ α} (w l)}} (· l)

3. the conclusion of the rule (∧ r), of the form: \frac{α · α ⊢ α α · α ⊢ α}{α · α ⊢ α ∧ α} (∧ r)

4. the conclusion of the contraction of the form: _{\frac{α · α ⊢ α, α ∧ α α · α ⊢ α, α ∧ α}{\frac{α · α ⊢ α ∧ α, α ∧ α}{α · α ⊢ α ∧ α} (w r)}} (∧ r).

The derivation 1, may be continued as follows:

1.1. _{\frac{α, α ⊢ α  α, α ⊢ α}{\frac{α, α ⊢ α ∧ α}{α · α ⊢ α ∧ α} (· l)}}(∧ r)  1.2. _{\frac{α, α ⊢ α, α ∧ α  α, α ⊢ α, α ∧ α}{\frac{α, α ⊢ α ∧ α, α ∧ α}{\frac{α, α ⊢ α ∧ α}{α · α ⊢ α ∧ α} (· l)}_{(w r)}}} (∧ r)

Since α, α ⊢ α in 1.1, cannot be the lower sequent of either any rule for a constant or any rule for a connective in limCBC_{W^{c}} (for α ≠ 1) and since it is not an axiom, the derivation at 1.1 is finished. α · α ⊢ α ∧ α is not proved.

In the derivation 1.2, α, α ⊢ α, α ∧ α can only be the lower sequent of the

rule (∧ r), of the form: \frac{α, α ⊢ α, α α, α ⊢ α, α}{α, α ⊢ α, α ∧ α} (∧ r) (in limCBC_{W^{c}} it cannot be the

endsequent of the derivation: _{\frac{α, α ⊢ α, α, α ∧ α α, α ⊢ α, α, α ∧ α}{\frac{α, α ⊢ α, α ∧ α, α ∧ α}{α, α ⊢ α, α ∧ α} (w r)}} (∧ r)), therefore the

derivation 1.2 cannot be the endsegment of any proof.

We saw that every derivation in limCBC_{W^{c}} which begins like 1, finishes (after the finite number of steps) without giving the proof. We proceed analogously in all other cases.

Now we shall show that every cut-free derivation in limCBC_{W^{c}} finishes after the finite number of steps, and that there is only the finite number of them, i.e., we shall show that limCBC_{W^{c}} is decidable.

We shall say that Γ′ ⊢ Δ′ and Γ ⊢ Δ, where Γ′, Δ′, Γ and Δ are multisets of formulae, are cognate iff exactly the same formulae occur in Γ and Γ′, and exactly the same formulae occur in Δ and Δ′ (for example, α ⊢ β, α, α ⊢ β and α ⊢ β, β are three different, cognate sequents). We shall call the class of all sequents cognate with a given sequent, a cognation class.

First we note that limCBC_{W^{c}} has the subformula property, saying that for any provable sequent Γ ⊢ Δ, there is a proof of Γ ⊢ Δ in limCBC_{W^{c}} (a cut-free proof), such that all formulae occurring in this proof are subformulae of formulae from Γ ⊢ Δ. Therefore, for every provable sequent, there is a proof (at least one cut-free proof) where only the finite number of cognation classes occur. Now it is clear that if we want to show that every upward derivation in limCBC_{W^{c}} is finite, it is enough to show that only the finite number of sequents from each cognation class, can be derived in every branch. Therefore, it is enough to prove the following lemma.

Lemma 6. Let σ = S_{0}, S_{1}, … be the sequence of cognate sequents. If σ is W -normal in the sense: for no i < j, S_{i} is the contraction of S_{j}, then σ is finite.

Proof. Let σ = S_{0}, S_{1}, … be the W -normal sequence of cognate sequents, and let γ_{1}, γ_{2}, …, γ_{s} be all formulae which occur in σ. Let σ′ = S′_{0}, S′_{1}, … be the sequence of sequents, which is obtained when we rename the formulae from σ, as follows: every appearance of γ_{1}, in the antecedent of a sequent, is substituted for α_{1}, and in the succedent of a sequent, for β_{1}; we proceed similarly for γ_{2}, …, γ_{s}. We note that all formulae, which occur in σ′ are α_{1}, … α_{l}, β_{1}, …, β_{d}, l + d = n ⩽ 2s.

σ′ is the W -normal sequence of cognate sequents. We wish to prove that σ′ is finite. We proceed by the induction on n (n is the number of different formulae occurring in σ′). Let n = 1. Then the claim is immediate, since the number of sequents, which belong to a W -normal sequence and which are built of repeated occurrences of only one formula, is finite.

Let n > 1 and let φ be any formula from σ′. Let σ′′(φ) = D_{0}, D_{2}, … be the sequence of sequents from σ′, which is defined as follows. Let S′_{k} be the first sequent from the left in σ′ that contains φ. Then D_{0} = S′_{k}; if D_{m} is defined and if D_{m} = S′_{j}, then D_{m+1} is the first sequent from the left in S′_{j+1}, S′_{j+2}, …, in which the number of occurrences of φ is greater than or equal to the number of occurrences of φ in D_{m}. (For example, if σ′ is the sequence of sequents: α_{1}, α_{1}, α_{2} ⊢ β_{1}, β_{2}, β_{2}, α_{1}, α_{2}, α_{2} ⊢ β_{1}, β_{1}, β_{2}, α_{1}, α_{2}, α_{2} ⊢ β_{1}, β_{2}, β_{2}, then σ′′(α_{1}) = α_{1}, α_{1}, α_{2} ⊢ β_{1}, β_{2}, β_{2}; σ′′(α_{2}) = σ′.)

We wish to prove that σ′′(φ) is finite. Let σ′′_{φ} be the sequence of sequents which is obtained by deleting all occurrences of φ in σ′′(φ). Since σ′′_{φ} is the W - normal sequence of cognate sequents (σ′ is W -normal), by the induction hypothesis it follows that σ′′_{φ} is finite. Therefore, σ′′(φ) is finite, and so is σ′. □

We should note that this algorithm could not be applied to sequent systems with contraction in the absence of permutation, since the subformula property does not hold there (cut is not an admissible rule there).

Now we give the postulates of the system CBCW, whose derivations are defined from the bottom up. We shall use Θ^{1} to denote the multiset of formulae from Θ, which appear exactly once in Θ.

Axioms of CBCW are the axioms of the system CBC.

Rules for propositional constants and connectives in CBCW are:

\frac{Γ ⊢ Δ}{Γ, 1 ⊢ Δ} (1 l)  \frac{Γ ⊢ Δ}{Γ ⊢ 0, Δ} (0 r)
\frac{Θ_{1} ⊢ α, Λ_{1}  Θ_{2}, β ⊢ Λ_{2}}{Θ, α → β ⊢ Λ} (→ l)  \frac{Γ, α ⊢ β, Ω_{1}}{Γ ⊢ α → β, Ω} (→ r)
\frac{Ω_{1}, α, β ⊢ Δ}{Ω, α · β ⊢ Δ} (· l)  \frac{Λ_{1} ⊢ α, Θ_{1}  Λ_{2} ⊢ β, Θ_{2}}{Λ ⊢ α · β, Θ} (· r)
\frac{Θ_{1}, α ⊢ Λ_{1}  Θ_{2}, β ⊢ Λ_{2}}{Θ, α + β ⊢ Λ} (+ l)  \frac{Γ ⊢ α, β, Ω_{1}}{Γ ⊢ α + β, Ω} (+ r)
\frac{Ω_{1}, α ⊢ Δ}{Ω, α ∧ β ⊢ Δ}  \frac{Ω_{1}, β ⊢ Δ}{Ω, α ∧ β ⊢ Δ} (∧ l)  \frac{Γ ⊢ α, Ω_{1}  Γ ⊢ β, Ω_{1}}{Γ ⊢ α ∧ β, Ω} (∧ r)

\frac{Ω_{1}, α ⊢ Δ  Ω_{1}, β ⊢ Δ}{Ω, α ∨ β ⊢ Δ} (∨ l)  \frac{Γ ⊢ α, Ω_{1}}{Γ ⊢ α ∨ β, Ω}  \frac{Γ ⊢ β, Ω_{1}}{Γ ⊢ α ∨ β, Ω} (∨ r)
− Θ_{1}, Θ_{2} = Θ
− Θ_{1} = Σ, Θ′, Θ_{2} = Σ, Θ′′,

Θ = Σ, Θ′, Θ′′, Σ ⊆ Θ^{1}

− Θ_{1}, Θ_{2} = Θ, α ∗ β,

provided that α ∗ β doesn’t appear in Θ

− Θ_{1} = Σ, Θ′, Θ_{2} = Σ, Θ′′,

Θ, α ∗ β = Σ, Θ′, Θ′′, Σ ⊆ Θ^{1},

provided that α ∗ β doesn’t appear in Θ

− Θ_{1} = α ∗ β, Σ, Θ′, Θ_{2} = α ∗ β, Σ, Θ′′,

Θ = Σ, Θ′, Θ′′, Σ ⊆ Θ^{1},

provided that α ∗ β doesn’t appear in Θ

− Λ_{1}, Λ_{2} = Λ
− Λ_{1} = Σ, Λ′, Λ_{2} = Σ, Λ′′,

Λ = Σ, Λ′, Λ′′, Σ ⊆ Λ^{1}

− Ω_{1} = Ω
− Ω_{1} = Ω, α ∗ β, provided that

α ∗ β doesn’t appear in Ω

∗ = \{ \begin{matrix}→, & in (→ l) and (→ r) \\ ·, & in (· l) and (· r) \\ +, & in (+ l) and (+ r) \\ ∧, & in (∧ l) and (∧ r) \\ ∨, & in (∨ l) and (∨ r) \end{matrix}

A derivation in CBCW is called W -normal if every branch of that derivation contains no Γ ⊢ Δ below Γ′ ⊢ Δ′, such that Γ ⊢ Δ is a contraction of Γ′ ⊢ Δ′.

Directly from the above consideration it follows that every W -normal derivation in CBCW is finite. Furthermore, the total number of them for any sequent Γ ⊢ Δ, is finite. Therefore, CBCW is decidable.

We should mention that in every upward derivation of any contractionless system, every (appearance of a) formula is allowed to be used at most once. From this point of view, contractionless logics can be looked upon as resource sensitive logics.

3. Tableaux for linear, BCK and relevant logic

For determining provability, we also formulate tableau systems for linear, BCK and relevant logic. The basic configuration of our tableau systems will be a finite tree whose nodes, which are not leaves, have either one or two successor nodes. Each tree will have exactly one root, which we call the initial node of a tree and at least one leaf, which we call the end node of a tree. The nodes of a tree which have exactly two successor nodes, will be called the branching nodes.

A complete branch of a tree is the sequence of tree-nodes whose initial node is the initial node of a tree, whose end node is the end node of a tree and whose every node (with the exception of exactly one: the end node of a branch) immediately precedes the tree-node which is the next node in the branch. Furthermore, we say that a sequence of tree-nodes is a branch, if it is the initial segment of some complete branch.

The section of a tree is the sequence of tree-nodes N_{1}, …, N_{s}, such that:

1. N_{1}, …, N_{s} are consecutive nodes from a branch of a tree,

2. N_{1} is either the root of the tree or an immediate successor node of a branching node,

3. N_{s} is either the end node of a tree or a branching node,

4. N_{1}, …, N_{s−1} are non-branching nodes.

Let τ be a tree. The initial section of τ, begins with the root of τ; its end section, ends with a leaf of τ.

Every section of a tree is associated with an o-sequence, which consists of (possible several) occurrences of 1 and/or 2, as follows:

1. 1 is the o-sequence of the initial section of a tree;

2. if o_{1}o_{2} … o_{n} is an o-sequence of a section, which is not the end section of a tree (the end node of our section is a branching node, then), then its left successor section is associated with o_{1}o_{2} … o_{n}1 (obtained by concatenating o_{1}o_{2} … o_{n} and 1) and its right successor section is associated with o_{1}o_{2} … o_{n}2.

Let τ be a tree and let S be a section in τ. Since there exists only one branch in τ, whose end section is S, every branch in τ is uniquely determined by its end section. Therefore, with every branch of a tree, we associate the o-sequence of its end section. Furthermore, with every subtree of a tree, we associate the o-sequence of its initial section. An empty branch and an empty tree are associated with ∅.

We also define a part of a tree as follows. Let t be an o-sequence of a section in τ. Then a part t of τ is the tree which is obtained when the initial segment of a subtree t is substituted for the branch t.

For example, in the following tree (o-sequences of corresponding sections are given within parentheses):

{N_{1} \atop N_{2}} (1)

⧸⧹

(11) {N_{3} \atop N_{4}} N_{5} (12)

⧸⧹

(111) N_{6} {N_{7} \atop N_{8}} (112)

the section 11 consists of the nodes N_{3} and N_{4}, the branch 11 consists of N_{1}, N_{2}, N_{3} and N_{4}, the subtree 11 consists of N_{3}, N_{4}, N_{6}, N_{7} and N_{8} and the part 11 consists of N_{1}, N_{2}, N_{3}, N_{4}, N_{6}, N_{7} and N_{8}.

Let φ be a propositional formula. Then s φ, where s ∈ {+, −} is a signed formula: + φ is positive and − φ is negative.

Tableaux will be defined as trees to whose nodes t-formulae have been assigned. A t-formula of a tableau τ is of the form sφz, where sφ is a signed formula and z is either an o-sequence of a section in τ or ∅, with the following meaning: the signed formula sφ is not allowed to be developed in the part z of τ.

We shall use Σ, Σ_{1}, …, Π, …, Φ, …, to denote finite sequences of t-formulae. A sequence Σ, Π is obtained by concatenating Σ and Π.

We say that a sequence of signed formulae s_{1}α_{1}, …, s_{n}α_{n} corresponds to a sequence of t-formulae F_{1}, …, F_{n}, and vice versa, iff F_{i} = s_{i}α_{i}z_{i}, for every i ∈ {1, …, n}. We shall use S(Σ) to denote a sequence of signed formulae which corresponds to Σ.

Let S be a sequence of signed formulae. We shall use Perm(S) to denote a sequence of signed formulae which is obtained by permuting the elements of S.

Furthermore, we shall use Perm(Σ) to denote a sequence of t-formulae which is obtained by permuting the elements of Σ.

Tableau systems consist of tableau rules. Every tableau rule is either a branch

closure rule, which is of the form \frac{Σ}{−} (used) or an expansion rule (which is either a

rule for a constant or a rule for a connective), which has one of the following forms:

\frac{Σ}{−} (used), when the rule generates no new nodes, or \frac{Σ}{Σ_{1}} (used), when the rule

generates some new nodes, enlarging the end section of some complete branch with

Σ_{1}, or \frac{Σ}{Σ_{1}|Σ_{2}} (used), when the rule generates some new nodes, branching some

complete branch, such that Σ_{1} belongs to its left successor section and Σ_{2} belongs to its right successor section. The meaning of ‘used’ will be given later.

Now we define tableaux as follows.

Definition 6. Let TS be a tableau system and let S = s_{1} α_{1}, …, s_{n} α_{n} be a sequence of signed formulae. Let t be either an o-sequence or ∅. We define a tableau of S in TS as follows.

s_{1} α_{1} z_{1} ; ⋮ ; s_{n} α_{n} z_{n}

where z_{i} ≠ in(t) for at least one i ∈ {1, …, n}, is a tableau of S in TS. If z_{i} = ∅, for every i ∈ {1, ⋯, n}, then we call it the initial tableau of S.

If τ is a tableau of S in TS, then another tableau of S in TS is generated when a rule of TS is applied at the end node N of a complete branch in τ, to some node(s) from the same branch (to N or/and to some node(s) above N). We apply rules of TS until either a branch closure rule has been applied to every complete branch of our tableau, or until a tableau, where none of the rules from TS can be applied, has been derived. (It should be emphasized that after the application of a branch closure rule no further construction can take place in that branch.)

Instead of a ‘node’, above, we may also say a t-formula.

A node at which we apply a rule is called the marked node. Remember that we always apply a rule at the end node of a complete branch. We note that after

the application of a rule which is of the form \frac{Σ}{−} (used), no new nodes have been

generated, therefore some nodes may be marked more than once.

Let t be a complete branch of a tableau τ. We shall say that t is finished in a tableau system TS, if none of the rules from TS can be applied to any node from t.

If a branch closure rule has been applied to some node(s) in a complete branch t, then t is closed. If every complete branch of a tableau τ is closed, then τ is closed.

Let t be an o-sequence of a section in a tableau τ. We shall say that a branch t (which is not necessary complete) in τ closes if:

1. t is a closed complete branch in τ, or

2. every complete branch of the part t of τ is closed, or

3. there is a derivation from τ to a tableau τ′, such that every complete branch of the part t of τ′ is closed.

A closed tableau of a sequence of signed formulae S in TS is the proof of S in TS. We shall say that a tableau τ closes in TS if either τ is closed in TS or there is a derivation in TS from τ to a closed tableau.

The leftmost complete branch of a tableau, which is not closed, will be called the current branch of a tableau derivation. In our tableau derivations, we shall always apply the rule at the end node of the current branch of a tableau.

A node (a t-formula) to which we apply a rule, is called the principal node (the principal t-formula) of that rule. When a rule is applied to a t-formula F from a complete branch t of a tableau τ, we say that the signed formula of F is used in the branch t. Since linear and BCK are resource sensitive logics, this signed formula is not allowed to be used again, either in the branch t, or in every subtree t, which could be generated in a further derivation (i.e., it cannot be used in the part t of τ and in the part t of any other tableau generated from τ in any further derivation). Therefore, when we apply a rule to a t-formula F = s φ z from a complete branch t, we set z to t (and possible z_{i} of some other t-formulae s_{i} φ_{i} z_{i} from the branch t), to denote that the signed formula of F cannot be used again in the part t of the current and any further tableau of that derivation. Settings are given in ‘used’, (see above) which is either empty or is of one of the following forms (t and g are o-sequences):

– t, which means: set z of the principal t-formula(e) to t,

– t^{g}, which means: set z_{i} of every t-formulae s_{i} φ_{i} z_{i} from the branch g to t. We shall say that a t-formula is unused in a tableau τ if it is of the form s φ ∅. Let p be an o-sequence. We shall use in(p) to denote the initial subsequence of

p (note that ∅ is not the initial subsequence of any o-sequence).

A t-formula F = s φ z, which belongs to the section g of a tableau τ, cannot be used anywhere in τ, if either z = g or z = g2 … 2. This is clear for z = g, since then F belongs to the part g of τ, where it cannot be used. On the other hand, z may be set to g2 … 2 only when a branch g2 … 2 is the current branch of our tableau derivation. Therefore, before the application of the rule, which sets z to g2 … 2, F belongs only to the current branch g2 … 2, of our tableau. After the application of that rule, it cannot be used there (and in the part g2 … 2 of any tableau generated in a further derivation) any more. Therefore, s φ z, where z = g or z = g2 … 2, will be called invisible in τ (although invisible nodes can be deleted, we keep them to avoid empty sections; however in the program implementation, we delete those nodes and change o-sequences of some sections, if necessary). A t-formula which is not invisible in τ, is called a visible t-formula.

We shall use Σ^{vis} (Σ^{invis}) to denote the sequence of visible (invisible) t-formulae from Σ, and Σ_{t} to denote all t-formulae from a branch t of a tableau.

We now give the postulates of the tableau system for BCK logic, namely TCBCK:

A complete branch t closure rules, z_{1} ≠ in(t), z_{2} ≠ in(t), z ≠ in(t):

(− 1) : \frac{\begin{matrix}Σ \\ − 1 z \\ Π \end{matrix}}{−} (t^{t})  (+ 0) :  \frac{\begin{matrix}Σ \\ + 0 z \\ Π \end{matrix}}{−} (t^{t})

(− ⊤) : \frac{\begin{matrix}Σ \\ − ⊤ z \\ Π \end{matrix}}{−} (t^{t})  (+ ⊥) :  \frac{\begin{matrix}Σ \\ + ⊥ z \\ Π \end{matrix}}{−} (t^{t})

(+α,−α) : \frac{\begin{matrix}Σ \\ s α z_{1} \\ Φ \\ \overline{s} α z_{2} \\ Π \end{matrix}}{−} (t^{t})  \overline{s} = \begin{cases}+, & if s = − \\ −, & if s = + \end{cases}

Rules for constants, t is the current branch, z ≠ in(t):

(+ 1) :  \frac{\begin{matrix}Σ \\ + 1 z \\ Π \end{matrix}}{−} (t)  (− 0) :  \frac{\begin{matrix}Σ \\ − 0 z \\ Π \end{matrix}}{−} (t)

Rules for connectives (t is the current branch, z ≠ in(t); t1 (t2) is the osequence obtained by concatenating t and 1 (2); Φ_{1} and Φ_{2} are sequences of unused t-formulae, which are formulated as follows: for every visible t-formula (s φ z) from the branch t, we formulate another unused t-formula (s φ ∅) which belongs either to Φ_{1} (i.e., to the branch t1), or to Φ_{2} (i.e., to the branch t2)):

(+ →) :  \frac{\begin{matrix}Σ \\ + α → β z \\ Π \end{matrix}}{\begin{matrix}Φ_{1} \\ − α ∅ \end{matrix} | \begin{matrix}Φ_{2} \\ + β ∅ \end{matrix}} (t^{t})  (− →) :  \frac{\begin{matrix}Σ \\ − α → β z \\ Π \end{matrix}}{\begin{matrix}+ α ∅ \\ − β ∅ \end{matrix}} (t)

(+ ·) :  \frac{\begin{matrix}Σ \\ + α · β z \\ Π \end{matrix}}{\begin{matrix}+ α ∅ \\ + β ∅ \end{matrix}} (t)  (− ·) :  \frac{\begin{matrix}Σ \\ − α · β z \\ Π \end{matrix}}{\begin{matrix}Φ_{1} \\ − α ∅ \end{matrix} | \begin{matrix}Φ_{2} \\ − β ∅ \end{matrix}} (t^{t})

(+ +) :  \frac{\begin{matrix}Σ \\ + α + β z \\ Π \end{matrix}}{\begin{matrix}Φ_{1} \\ + α ∅ \end{matrix} | \begin{matrix}Φ_{2} \\ + β ∅ \end{matrix}} (t^{t})  (− +) :  \frac{\begin{matrix}Σ \\ − α + β z \\ Π \end{matrix}}{\begin{matrix}− α ∅ \\ − β ∅ \end{matrix}} (t)

(+ ∧) :  \frac{\begin{matrix}Σ \\ + α ∧ β z \\ Π \end{matrix}}{+ α ∅} (t), \frac{\begin{matrix}Σ \\ + α ∧ β z \\ Π \end{matrix}}{+ β ∅} (t)  (− ∧) : \frac{\begin{matrix}Σ \\ − α ∧ β z \\ Π \end{matrix}}{− α ∅ | − β ∅} (t)

(+ ∨) : \frac{\begin{matrix}Σ \\ + α ∨ β z \\ Π \end{matrix}}{+ α ∅ | + β ∅} (t)  (− ∨) : \frac{\begin{matrix}Σ \\ − α ∨ β z \\ Π \end{matrix}}{− α ∅} (t), \frac{\begin{matrix}Σ \\ − α ∨ β z \\ Π \end{matrix}}{− β ∅} (t)

We note that after the application of a rule for a constant, no new nodes of a tableau have been generated, therefore a marked node of our tableau, at which we apply a rule for a constant is also a node at which we apply the next rule of our tableau derivation, i.e., this node is marked more than once.

We also note that the branch closure rules for 1 and 0 coincide with the rules for ⊤ and ⊥, respectively. It is expected, since 1 and ⊤ and 0 and ⊥ are equivalent in BCK logic. Therefore, we can exclude both ⊤ and ⊥, together with the rules for ⊤ and ⊥ from TCBCK. However in their presence, a tableau system for linear logic (where 1 differs from ⊤ and 0 from ⊥), TCBC, can be defined: TCBC, has the postulates of TCBCK above, satisfying ((Σ, Φ, Π)_{t})^{vis} in (+α,−α) and ((Σ, Π)_{t})^{vis} in (− 1) and (+ 0) are empty.

Furthermore, we define a tableau system for relevant logic, TCBCW, from TCBC, as follows. The axioms and the rules for constants in TCBCW are the same as in TCBC. We change the rules for connectives in TCBC, to allow applications of contraction as discussed in the previous section. We shall use Σ^{1} to denote the sequence of all t-formulae from Σ, whose corresponding signed formulae appear exactly once in S(Σ).

We note that in the rules (+ →), (− ·) and (+ +), in TCBC (and TCBCK), Φ_{1} and Φ_{2} are such that:

1. S((Σ, Π)^{vis}) = Perm(S(Φ_{1}, Φ_{2})).

In TCBCW, we also allow Φ_{1} and Φ_{2} to be as follows (we use F to denote the principal t-formula of the rule):

2. S(Φ_{1}) = S(Ω, Δ_{1}), S(Φ_{2}) = S(Ω, Δ_{2}), Ω ⊆ ((Σ, Π)^{vis})^{1} and Perm(Ω, Δ_{1}, Δ_{2}) = (Σ, Π)^{vis}.

3. S(Φ_{1}, Φ_{2}) = Perm(S(F, (Σ, Π)^{vis})), provided that S(F) does not appear in S((Σ, Π)^{vis}).

4. S(Φ_{1}) = S(Ω, Δ_{1}), S(Φ_{2}) = S(Ω, Δ_{2}), Ω ⊆ ((Σ, Π)^{vis})^{1} and Perm(Ω, Δ_{1}, Δ_{2}) = Perm(F, (Σ, Π)^{vis}), provided that S(F) does not appear in S((Σ, Π)^{vis}).

5. S(Φ_{1}) = S(F, Ω, Δ_{1}), S(Φ_{2}) = S(F, Ω, Δ_{2}), where Ω ⊆ ((Σ, Π)^{vis})^{1} and Perm(Ω, Δ_{1}, Δ_{2}) = (Σ, Π)^{vis}, provided that S(F) does not appear in S((Σ, Π)^{vis}).

The ‘used’ in the rules (+ →), (− ·) and (+ +) of TCBCW is the same as in TCBC.

In all other rules, we alow ’used’ to be either (t) (as in TCBC) or empty, provided that S(F) does not appear in S((Σ, Π)^{vis}).

Our tableaux are very closely related to upward sequent derivations. In the proof of the following theorem, we shall see how the upward derivation of a sequent γ_{1}, …, γ_{n} ⊢ δ_{1}, …, δ_{m} in CBCK can be transformed into the tableau derivation of the sequence +γ_{1}, …, +γ_{n}, −δ_{1}, …, −δ_{m} in TCBCK, and vice versa.

We shall say that in a tableau τ, a node N_{1} is the predecessor node of a node N_{2} iff there is a branch in τ which contains both N_{1} and N_{2}, such that N_{1} is above N_{2} (we also say that N_{2} is the successor node to N_{1}, then).

Let τ be a tableau of S in TCBCK and let N be a marked node in τ, which is marked k ⩾ 1 times. Let t be a branch of τ (which is not necessarily complete) whose end node is N. Let Σ = F_{1}, …, F_{m} be the sequence of all t-formulae from t (F_{m} is assigned to N) and let S(Σ) = f_{1}, …, f_{m} (remember that S(Σ) is the sequence of signed formulae which corresponds to Σ). Then, for every j ∈ {1, …, k}, we define the sequence of signed formulae Unused_{j}(N), as follows: Unused_{j}(N) is the sequence of signed formulae from f_{1}, …, f_{m} which are unused in t until the moment we mark N for the j-th time.

For example:

N_{1} : − (α · β. · γ) · 1 → α 1  Unused_{1}(N_{1}) = − (α · β. · γ) · 1 → α
N_{2} : + (α · β. · γ) · 1 1
N_{3} : − α 1  Unused_{1}(N_{3}) = + (α · β. · γ) · 1, − α
N_{4} : + α · β. · γ 1
N_{5} : + 1 1  Unused_{1}(N_{5}) = − α, + α · β. · γ, + 1
N_{6} : + α · β 1
N_{7} : + γ 1  Unused_{1}(N_{7}) = − α, + 1, + α · β, + γ
Unused_{2}(N_{7}) = − α, + α · β, + γ
N_{8} : + α 1
N_{9} : + β 1  Unused_{1}(N_{9}) = − α, + γ, + α, + β

At the end of our derivation, a branch closure rule has been applied to − α ∅ and + α ∅ at + β ∅.

Let S be a sequence of signed formulae. If +α_{1}, …, +α_{m} are all positive and if −β_{1}, …, −β_{n} are all negative signed formulae from S, then Sequent(S) (a sequent of S) is α_{1}, …, α_{m} ⊢ β_{1}, …, β_{n}, where α_{1}, …, α_{m} and β_{1}, …, β_{n} are multisets of formulae (each of them may be empty).

We now show that CBCK and TCBCK are equivalent systems. Namely, we shall prove the following theorem:

Theorem 1. The sequent γ_{1}, …, γ_{n} ⊢ δ_{1}, …, δ_{m} is provable in CBCK iff there is a proof of +γ_{1}, …, +γ_{n}, −δ_{1}, …, −δ_{m} in TCBCK.

For the proof we shall use the following lemma:

Lemma 7. Let τ be a closed tableau of S in TCBCK and let N be a marked node in τ. If N is marked m ⩾ 1 times in τ, then for every j ∈ {1, …, m}, a sequent Sequent(Unused_{j}(N)) is provable in CBCK.

Proof. Let N be a marked node in a closed tableau τ of S in TCBCK. We proceed by induction on n, where n is the number of marked nodes which succeed N in τ. First we note that if N is marked m > 1 times, then rules for constants have been applied m − 1 times to N, before a rule for a connective or a branch closure rule has been applied to N. Since every Sequent(Unused_{i}(N)) can be derived from Sequent(Unused_{i+1}(N)) by the application of either (1 l) or (0 r), for every i ∈ {1, …, m − 1}, it is enough to prove that Sequent(Unused_{m}(N)) is provable in CBCK.

Let n = 0 (note that N is the end node of τ, then). If N is marked m ⩾ 1 times, then the m-th applied rule at N is a branch closure rule. We have the following cases. If the m-th applied rule at N is (+α, −α), then Sequent(Unused_{m}(N)) is of the form Γ, α ⊢ α, Δ, i.e., it is the axiom of CBCK, therefore it is provable. We proceed analogously when any other branch closure rule has been applied at N.

Let n > 0 and let N be marked m ⩾ 1 times. Then we have the following cases. Let the m-th applied rule at N be (+ →) and let it be applied to a node M to which + α → β z is assigned. M is either N or the predecessor node of N. Then we wish to show that Sequent(Unused_{m}(N)) is provable in CBCK.

A node N_{1}, to which a t-formula − α ∅ is assigned, immediately after the application of the rule (+ →) at N to M, is our next marked node in the branch t1 (see the formulation of rule (+ →) in TCBCK). Let the m_{1}-th, m_{1} ⩾ 1, applied rule at N_{1} be a rule which is not not a rule for a constant. Since N_{1} is followed by less than n succeeding marked nodes, by the induction hypothesis Sequent(Unused_{m_{1}}(N_{1})) is provable in CBCK. We proceed analogously to show that Sequent(Unused_{m_{2}}(N_{2})) is provable in CBCK, where N_{2} is a node, to which a t-formula + β ∅ is assigned immediately after the application of the rule (+ →) at N to M and where m_{2} ⩾ 1 is such that the m_{2}-th applied rule at N_{2} is not a rule for a constant.

If Sequent(Unused_{m_{1}}(N_{1})) = Γ_{1} ⊢ α, Δ_{1} and if Sequent(Unused_{m_{2}}(N_{2})) = Γ_{2}, β ⊢ Δ_{2}, then Sequent(Unused_{m}(N)) = Γ, α → β ⊢ Δ, where Γ = Γ_{1}, Γ_{2}, Σ, such that Σ is either an empty multiset or a multiset which consists of repeated occurrences of 1 only, and Δ = Δ_{1}, Δ_{2}, Π, such that Π is either an empty multiset or a multiset which consists of repeated occurrences of 0 only. Now it is clear that our sequent Sequent(Unused_{m}(N)) is provable in CBCK:

\frac{{π_{1} \atop Γ_{1} ⊢ α, Δ_{1}}}{⋯}

possible applications of the rules (1 l) and (0 r)

Γ_{1}, Σ_{1} ⊢ α, Δ_{1}, Π_{1}

\frac{{π_{2} \atop Γ_{2}, β ⊢ Δ_{2}}}{⋯}

possible applications of the rules (1 l) and (0 r)

Γ_{2}, β, Σ_{2} ⊢ Δ_{2}, Π_{2}

Γ_{1}, Γ_{2}, Σ, α → β ⊢ Δ_{1}, Δ_{2}, Π (→ l)

where Σ_{1}, Σ_{2} = Σ and Π_{1}, Π_{2} = Π.

We proceed analogously in all other cases. □

Proof of Theorem 1. Let D be the proof of γ_{1}, …, γ_{n} ⊢ δ_{1}, …, δ_{m} in CBCK (γ_{1}, …, γ_{n} and δ_{1}, …, δ_{m} are multisets of formulae). We formulate the initial tableau of S = +γ_{1}, …, +γ_{n}, −δ_{1}, …, −δ_{m} in TCBCK:

+ γ_{1} ∅
⋮
+ γ_{n} ∅
− δ_{1} ∅
⋮
− δ_{m} ∅

By induction on n, where n is the length of D (n is the total number of sequents in D), we wish to show that this closes in TCBCK.

Let n = 1. Then our sequent is an axiom. We proceed as follows. If our sequent is an axiom Γ, α ⊢ α, Δ (Id), then a tableau which begins with +α_{1}z_{1}, …, +α_{n−1}z_{n−1}, +αz_{n}, −αz′_{1}, −β_{2}z′_{2}, …, −β_{m}z′_{m}, where z_{i} ≠ in(t) for every i={1, ..., n} and z′_{j} ≠ in(t) for every j = {1, …, m}, for either t = ∅ or any o-sequence t, is closed by the application of the rule (+α,−α) to +αz_{n} and −αz′_{1}. We proceed analogously when our sequent is one of the axioms (1 r) or (0 l) ( (⊤ r) or (⊥ l)).

Suppose n > 1. Then our sequent is the lower sequent of an inference rule in CBCK. We have the following cases.

Let D be of the following form:

\frac{{π_{1} \atop γ_{1}, …, γ_{i−1} ⊢ α, δ_{1}, …, δ_{j}}  {π_{2} \atop γ_{i}, …, γ_{n}, β ⊢ δ_{j+1}, …, δ_{m}}}{γ_{1}, …, γ_{n}, α → β ⊢ δ_{1}, …, δ_{m}} (→ l)

Then we consider the tableau that begins with:

\begin{matrix}Σ \\ + α → β z \\ Π \end{matrix}

such that S((Σ, Π)_{t}^{vis}) = Perm(+γ_{1}, …, +γ_{n}, −δ_{1}, …, −δ_{m}) and z ≠ in(t), for either t = ∅ or any o-sequence t. We wish to show that this tableau closes. We apply the rule (+ →) to + α → β z:

\frac{\begin{matrix}Σ \\ + α → β z \\ Π \end{matrix}}{+ γ_{1} ∅ ; ⋮ ; + γ_{i−1} ∅ ; − δ_{1} ∅ ; ⋮ ; − δ_{j} ∅ ; − α ∅ | + γ_{i} ∅ ; ⋮ ; + γ_{n} ∅ ; − δ_{j+1} ∅ ; ⋮ ; − δ_{m} ∅ ; + β ∅} (t^{t})

On inductive hypothesis, our tableau closes.

We proceed analogously when D ends with any other inference rule of CBCK. Conversely, we wish to show that if there is a closed tableau τ of S = +γ_{1}, …,

…, +γ_{n}, −δ_{1}, …, −δ_{m}, in TCBCK, then there is a proof of γ_{1}, …, γ_{n} ⊢ δ_{1}, …, δ_{m} in CBCK. We should note that the first marked node in our tableau is the node N_{1} to which the t-formula −δ_{m}z is assigned (z = ∅ in the initial tableau of S). However, directly from Lemma 7 it follows that a sequent Sequent(Unused_{1}(N_{1})) = γ_{1}, …, γ_{n} ⊢ δ_{1}, …, δ_{m} is provable in CBCK. □

A tableau system for classical logic, TCBCKW, consists of the axioms of TCBCK, together with the rules for constants and the rules for connectives of TCBCW. Tableau systems for single-conclusion logics are without the connective + and they satisfy the following condition: at any moment of a derivation, every complete branch of a tableau contains at most one negative visible t-formula.

4. The general algorithm

We shall describe the algorithm which can be used for determining provability in any of our logics. We shall use it for designing two theorem provers: the first one, P_{1}, searches for the proof in single- and multiple-conclusion Lambek logic and in single- and multiple conclusion Lambek logic with weakening; the other one, P_{2} searches for the proof in single- and multiple-conclusion linear, BCK and relevant logic, intuitionistic and classical logic. Here we shall describe P_{2}, only.

We should mention that our prover is not the most efficient one: for every logic, it is possible to formulate more efficient proof search. However, the advantage of our approach is that, for a given input, we always get, as an output, the list of structural rules, whose presence is necessary in the proof, if the given input is a theorem of at least one of our logics (otherwise, the program exits either with the message about syntactic incorrectness of our input, or with the message that our input is a formula which is not a theorem in any of our logics).

The specific feature of our subtructural logics is the nondeterminism of their derivations. Namely, for tableaux τ and τ′, in a tableau system TS, where τ′ is obtained from τ by an application of a rule from TS, it is possible that τ closes and τ′ doesn’t (except when TS is a tableau system for either intuitionistic or classical logic). This means that if the application of a rule to a t-formula in the current branch leads to a closed tableau, then the application of a rule to some other t-formula in the current branch need not. Furthermore, even when a tableau of S closes in the presence of some structural rules or when it closes in a multipleconclusion logic, the derivation is not finished: we still wish to know if there is a closed tableau of S, in the presence of some other structural rules or without any of them or if there is a closed tableau of S in some single-conclusion logic. Therefore, the use of backtracking is necessary, in designing the prover.

The structure that supports backtracking is MOGUCI. A node of the type MOGUCI contains information about the tableau at the moment when the derivation becomes nondeterministic (i.e., it contains the tableau at the moment we chose one possibility to continue the derivation, when at least two of them are available; furthermore, all structural rules that have been used in the derivation until then, together with the information whether the derivation has been in a single- or in a multipleconclusion logic, form the closure condition which we save in the closure fields; algorithm uses several closure fields; closure fields of a node of the type MOGUCI are some of them).

Our program (P_{2}) always searches for a proof with the minimal closure condition. Our minimal logic, where a given formula can be a theorem is the singleconclusion linear logic. The minimal closure condition is defined as follows.

Definition 7. Let C_{1} and C_{2} be two closure conditions. If C_{1} gives the proof in a single-conclusion logic and if C_{2} gives the proof in a multiple-conclusion logic, then C_{1} is less than C_{2}. Furthermore, if both C_{1} and C_{2} give the proof either in a single- or in a multiple-conclusion logic, then C_{1} is less than C_{2} if either C_{1} is with permutation only, or C_{2} is with permutation, weakening and contraction.

Our prover uses the system TCBCKW. However, if there is a proof of −φ in TCBCKW, where every complete branch is closed using the axioms of TCBCW (TCBC) only, and where at least one rule for a connective, which is not also the rule for a connective in TCBC, is used, then −φ is the theorem in a multiple-conclusion logic, in the presence of permutation and contraction, only, i.e., in TCBCW. On the other hand, if there is a proof of −φ in TCBCKW, where at least one branch is closed using an axiom of TCBCK, which is not the axiom of TCBC, also, and where every applied rule for a connective is from TCBC only, then −φ is the theorem in a multiple-conclusion logic, in the presence of permutation and weakening only, i.e., in TCBCK. Furthermore, if there is a proof of −φ in TCBCKW, where every complete branch is closed using the axioms of TCBCW (TCBC) only, and where every applied rule for a connective is from TCBC only, then −φ is the theorem in a multiple-conclusion logic, in the presence of permutation only, i.e., in TCBC. Finally, if φ is without + and if every complete branch generated in the proof has at most one visible negative t-formula, then our formula is provable in a singleconclusion logic with permutation and/or weakening and/or contraction, due to the above consideration.

Now we give the general algorithm. Our input gets the minus sign as prefix and if it is syntactically correct, the associated binary tree of a given signed formula −φ is produced. From the root of this tree, the initial tableau is generated. A proof search procedure proceeds as follows.

1. If the current branch is closed, set the appropriate values in the closure fields. If the current branch is closed and finished, then go to 7, else go to 2.

2. If the current branch is finished, but not closed, or empty, then go to 4, else go to 3.

3. Pick up a t-formula to which we wish to apply a rule and form a new node of the list moguci, containing the information about the rest of t-formulae that could be picked up instead. If the rule can be applied to a picked up t-formula on several equally applicable possibilities, we chose one, and form another node of the list moguci, containing the information about the others. We apply the rule, then go to 1.

4. If the list moguci is empty, then exit with the message “the formula φ is not a theorem in any of corresponding logics”, else go to 5.

5. If all possibilities for deriving the tableau in the first node of the list moguci, are exhausted, then go to 6, else generate another new current state based on the information from that node and go to 1.

6. Delete the first node of the list moguci. If the tableau of the deleted node of the list moguci didn’t close in any of earlier derivations, then go to 4, else, set the appropriate values in the closure fields and go to 7.

7. If the list moguci is empty, then go to 8, else go to 9.

8. If every complete branch of our tableau is closed, then exit with the message “the formula φ is a theorem”, and give all structural rules needed in the proof, else generate another current state and go to 1.

9. If the tableau from the first node of the list moguci, closes, then go to 10, else take its leftmost open branch for the current branch and go to 1.

10. If all possibilities for deriving the tableau from the first node of the list moguci are exhausted, then delete that node from the list, set the appropriate values in the closure fields and go to 7, else form another current state based on the information from that node and go to 1.

We shall illustrate our proof search procedure with the following simple example. Namely, we shall prove the theorem: (α → β) → α. → α.

At the beginning the initial tableau of − (α → β) → α. → α is produced:

τ_{1} : − (α → β) → α. → α ∅

Here, only one rule can be applied, the rule (− →) to − (α → β) → α. → α ∅:

τ_{2} : \begin{matrix}− (α → β) → α. → α 1 \\ + (α → β) → α ∅ \\ − α ∅ \end{matrix}

Here, we can apply only one rule again, the rule (+ →) to + (α → β) → α ∅. However it can be applied in several different ways. We chose one of them to derive a tableau τ_{3} and we generate the first node of the list moguci to remember the other possibilities.

τ_{3} :  \begin{matrix}− (α → β) → α. → α 1 \\ + (α → β) → α 1 \\ − α 1 \end{matrix} ; − α → β ∅ | \begin{matrix}+ α ∅ \\ − α ∅ \end{matrix}

After the application of the rule (− →) to − α → β ∅, the tableau τ_{4} is produced, whose every branch is finished, but the leftmost one is not closed, therefore it is not the proof of our formula:

τ_{4} :  \begin{matrix}− (α → β) → α. → α 1 \\ + (α → β) → α 1 \\ − α 1 \end{matrix} ; \begin{matrix}− α → β 11 \\ + α ∅ \\ − β ∅ \end{matrix} | \begin{matrix}+ α ∅ \\ − α ∅ \end{matrix}

Since the list moguci is not empty, we generate another tableau τ_{3}, keeping the remaining possibilities in the list moguci:

τ_{3} :  \begin{matrix}− (α → β) → α. → α 1 \\ + (α → β) → α 1 \\ − α 1 \end{matrix} ; \begin{matrix}− α ∅ \\ − α → β ∅ \end{matrix} | + α ∅

Then we apply the rule (− →) to generate τ_{4}:

τ_{4} :  \begin{matrix}− (α → β) → α. → α 1 \\ + (α → β) → α 1 \\ − α 1 \end{matrix} ; \begin{matrix}− α ∅ \\ − α → β 11 \\ + α ∅ \\ − β ∅ \end{matrix} | + α ∅

The current branch (the leftmost one) is closed in the multiple-conclusion logic with weakening. However the other one is finished, but it is not closed. Therefore our tableau, again, is not a proof of our formula. Once more, we pick the (last) information from the list moguci to generate another tableau τ_{3}:

τ_{3} :  \begin{matrix}− (α → β) → α. → α 1 \\ + (α → β) → α 1 \\ − α 1 \end{matrix} ; \begin{matrix}− α ∅ \\ − α → β ∅ \end{matrix} | \begin{matrix}− α ∅ \\ + α ∅ \end{matrix}

We note that the above tableau is derived in the presence of contraction and we keep that information in the corresponding closure fields. Then again we apply the rule (− →) to − α → β ∅ to generate the final tableau of our derivation:

τ_{4} :  \begin{matrix}− (α → β) → α. → α 1 \\ + (α → β) → α 1 \\ − α 1 \end{matrix} ; \begin{matrix}− α ∅ \\ − α → β 11 \\ +α ∅ \\ − β ∅ \end{matrix} | \begin{matrix}− α ∅ \\ + α ∅ \end{matrix}

The leftmost branch is closed in the multiple-conclusion logic with weakening; the other one is closed unconditionally. Since the list moguci is empty, our derivation is finished: our formula is a theorem in a multiple-conclusion logic with permutation, contraction and weakening (i.e., in classical logic, only).

Acknowledgements. I would like to express my gratitude to Professors Zoran Petrić and Miodrag Kapetanović for many useful suggestions. Furthermore, I am grateful to the referees for very helpful comments.

References

[1] V. M. Abrusci, Phase semantics and sequent calculus for pure noncomutative classical linear propositional logic, J. Symbolic Logic 56:4 (1991), 1403–1451.

[2] G. Gentzen, Investigations into logical deduction; in: M. E. Szabo (Ed.), The Collected Papers of Gerhard Gentzen, North-Holland, Amsterdam, 1969, pp. 68–131

[3] M. Isaković Ilić, Cut elimination and decidability for classical Lambek logic, Journal of Logic and Computation 2007; DOI:10.1093/logcom/exm063

[4] P. Schroeder-Heister and K. Došen (Eds.), Substructural Logics, Oxford, Oxford University Press, 1993.

[5] S. Kripke, The problem of entailment, abstract, J. Symbolic Logic 24 (1959), 234.

[6] G. Restall, An intruduction to Substructural Logics, Routledge, London, 2000.

Šumarski fakultet Kneza Višeslava 1 11000 Beograd Serbia

    isakm@yubc.net