Semantics and Cut-free Provability of Modal Substructural Logics

Takafumi SAKURAI

                      sakurai@math.s.chiba-u.ac.jp

Department of Mathematics and Informatics Chiba University

In this paper, we study the model of modal propositional Lambek logics. We give the model similar to the phase space and demonstrate its usefulness by showing the cut-free provability theorem and giving the Kripke semantics.

1 Preliminaries

For the definitions of Lambek logic FL_{σ}, FL_{σ}-algebra, so_{σ}-monoid, modal Lambek logic FL_{σ}^{m}, and modal FL_{σ}-algebra, we refer Ono [3].

2 Construction by Filter

We can construct so_{σ}-monoid from FL_{σ}-algebra and vice versa by Ono and Komori [4]’s method.

Definition 2.1 Let A be an FL-algebra. SOM(A) is a structure ⟨𝔽^{−}(A), ∩, ·, ϵ, ω⟩ where ∩ is the set

intersection, x · y =^{def} F{a ⋆ b | a ∈ x, b ∈ y}, ϵ =^{def} 1↑, ω =^{def} A, 𝔽^{−}(A) =^{def} {x | x ∈ 𝔽(A), x · ϵ = ϵ · x = x}.

Theorem 2.2 If A is an FL_{σ}-algebra, SOM(A) is an so_{σ}-monoid.

Definition 2.3 Let D be an so-monoid. FLA(D) is a structure ⟨𝔽(D), →, ∪, ∩, ⋆, 1, 0, ⊤, ⊥⟩ where a → b =^{def} {y ∈ D | for all x ∈ a, y · x ∈ b}, ∩ is the set intersection, a ∪ b =^{def} F(a ∪ b) where ∪ in the

righthand is the set union, a ⋆ b =^{def} F{x · y | x ∈ a, y ∈ b}, ⊤ =^{def} D, ⊥ =^{def} {ω}, 1 =^{def} ϵ↑, 0 =^{def} ⊥ (if w ∈ σ)

or any filter (otherwise).

Theorem 2.4 If D is an so_{σ}-monoid, FLA(D) is an FL_{σ}-algebra.

Definition 2.5 Let A ≡ ⟨A, →, ∪, ∩, ⋆, 1, 0, ⊤, ⊥⟩ be an FL-algebra. A^{s} is a structure ⟨A, ∪, ⋆, 1, ⊥⟩.

Theorem 2.6 If A is an FL_{σ}-algebra, A^{s} is an so_{σ}-monoid. (The order induced in A^{s} is the opposite order of the order of A.)

3 Modality

Definition 3.1 Let D be an so_{σ}-monoid ⟨D, ∩, ·, ϵ, ω⟩. Cent(D) denotes the set {x ∈ D | ϵ ≤ x, x · x ≤ x, for all y ∈ D, x · y = y · x}. ⟨FLA(D), I, ¿, 0⟩ is a modal so_{σ} phase structure iff I is a submonoid of Cent(D), 0 ∈ FLA(D), and ¿ is an operation on D that satisfies

1. ¿x ≤ x, ¿x ≤ ¿¿x for x ∈ D

2. ¿(x · y) ≤ x · ¿y for x ∈ I and y ∈ D

3. if x ∈ 0, then ¿x ∈ 0 A modal so_{σ} phase structure has operations ! and ? on 𝔽(D) which are defined as follows.

!a =^{def} F(I ∩ a) ?a =^{def} F(0 ∪ ¿a) where ¿a =^{def} {¿x | x ∈ a}

Theorem 3.2 A modal so_{σ} phase structure is a modal FL_{σ}-algebra.

Proposition 3.3 Let A be a modal FL_{σ}-algebra and put D = SOM(A), I =^{def} {(!u)↑ | u ∈ A}, ¿x =^{def} F{?u | u ∈ x}, and 0 =^{def} (0_{A}↑)↑ (0_{A} is 0 in A). Then, ⟨FLA(D), I, ¿, 0⟩ is a modal so_{σ} phase structure.

Proposition 3.4 Let A be a modal FL_{σ}-algebra and put I =^{def} {!a | a ∈ A} and 0 =^{def} 0_{A^{s}}↑ (0_{A^{s}}↑ is a filter generated using the order of A^{s}, therefore, 0 = {a | a ≤_{A} 0_{A}} where ≤_{A} is the order in A.) Then, ⟨FLA(A^{s}), I,?, 0⟩ is a modal so_{σ} phase structure.

Theorem 3.5 Let A be a modal FL_{σ}-algebra.

1. Let B be ⟨FLA(D), I, ¿, 0⟩ given in Prop. 3.3. Then, a map from A to B defined by a ↦ (a↑)↑ is an embedding of modal FL_{σ}-algebra.

2. Let B be ⟨FLA(A^{s}), I,?, 0⟩ given in Prop. 3.4. Then, a map from A to B defined by a ↦ a↑ is an embedding of modal FL_{σ}-algebra.

Theorem 3.6 FL_{σ}^{m} is complete with respect to the class of all modal so_{σ} phase structures.

Remark: FL_{ewc}^{m} is equivalent to the constructive modal logic CS4 which consists of intuitionistic propositional logic, necessitation rule, and following axioms.

□K: □(A → B) → (□A → □B)  ◇K: □(A → B) → (◇A → ◇B)
□T: □A → A  ◇T: A → ◇A
□4: □A → □□A  ◇4: ◇◇A → ◇A
◇⊥E: ◇⊥ → A

(□ and ◇ are to be replaced by ! and ? respectively.) Therefore, ! and ? in so_{ewc}-modal phase structure can be used to interpret □ and ◇ in CS4.

Remark: (Girard’s modal op for classical phase space [1]) Let (P, ·) be a commutative monoid, O ⊆ P, and C(a) =^{def} (a → O) → O for a ⊆ P. Operations ! and ? are defined on {a | C(a) = a}.

!a =^{def} ((I ∩ a) → O) → O ?a =^{def} (I ∩ (a → O)) → O

4 Cut-Free Provability

In this section, we show the cut-free provability theorem for some FL_{σ} by using modal so_{σ} phase structure.

Lemma 4.1 In FL_{σ}^{m}, if Γ_{1}, α ∨ β, Γ_{2} ⊢ θ is cut-free provable, then Γ_{1}, α, Γ_{2} ⊢ θ and Γ_{1}, β, Γ_{2} ⊢ θ are cut-free provable.

Lemma 4.2 In FL_{σ}^{m} (c ∉ σ or e ∈ σ), if Γ_{1}, α ⋆ β, Γ_{2} ⊢ θ is cut-free provable, then Γ_{1}, α, β, Γ_{2} ⊢ θ is cut-free provable.

We define the preorder ≤ on formulas of FL_{σ}^{m} as follows:

α ≤ β iff, for every Γ_{1}, Γ_{2}, θ, if Γ_{1}, α, Γ_{2} ⊢ θ is cut-free provable, then Γ_{1}, β, Γ_{2} ⊢ θ is cut-free provable.

Let ∼ be the equivalence relation defined by α ∼ β iff α ≤ β and β ≤ α, [α] be the equivalence class to which a formula α belongs, and L_{σ} be the quotient set. Then, a partial order ≤ on L_{σ} is induced. We define the operations ∩ and · on L_{σ} as follows: [α] ∩ [β] =^{def} [α ∨ β], [α] · [β] =^{def} [α ⋆ β]. The definition of ∩ does not depend on the choice of the representative by Lemma 4.1 and, in the case of FL_{σ}^{m} (c ∉ σ or e ∈ σ), the definition of · does not depend on the choice of the representative by Lemma 4.2. Therefore, if c ∉ σ or e ∈ σ, operations ∩ and · are well-defined and we can check that L_{σ} =^{def} ⟨L_{σ}, ∩, ·, [1], [⊥]⟩ is an so_{σ}-monoid. Note that the order induced from ∩ coincides with ≤, that is, [α] ∩ [β] = [α] iff [α] ≤ [β].

Put I =^{def} {[!α_{1} ⋆ ⋯ ⋆ !α_{n}]} and ¿[α] =^{def} [?α]. Let ||α|| =^{def} {[γ] | γ ⊢ α is cut free provable} and put 0 =^{def} ||0_{σ}|| (0_{σ} is a formula 0 in FL_{σ}^{m}). Then, P_{σ} =^{def} ⟨FLA(L_{σ}), I, ¿, 0⟩ is a modal so_{σ} phase structure.

Let [[α]] be the valuation of α on P_{σ} where we put [[p]] = ||p|| for propositional variable p.

Theorem 4.3 In P_{σ} (c ∉ σ or e ∈ σ), [α] ∈ [[α]] ⊆ ||α||.

Corollary 4.4 In FL_{σ}^{m} (c ∉ σ or e ∈ σ), if Γ ⊢ θ is provable with cuts, then Γ ⊢ θ is provable without cuts. Proof. If Γ ≡ α_{1}, …, α_{n}, we write Γ^{⋆} for α_{1} ⋆ … ⋆ α_{n}. (Γ^{⋆} ≡ 1 if n = 0.) If Γ ⊢ θ is provable, then Γ^{⋆} ⊢ θ is provable. By Th. 4.3, [Γ^{⋆}] ∈ [[Γ^{⋆}]] ≤ [[θ]] ⊆ ||θ||. Therefore, Γ^{⋆} ⊢ θ is cut-free provable. By Lemma 4.2, Γ ⊢ θ is cut-free provable. □

Fortunately(?), the cut-elimination theorem does not hold either in FL_{c} or FL_{cw}.

Remark: The idea of using ||α|| and proving the theorem of the form Th. 4.3 comes from [2]. In [2], the cut-free provability and the cut-elimination theorems for intuitionistic and classical linear logics with modality are proved. In [5], the cut-elimination theorems for the predicate logic FLs (but not for the modal FLs) are proved.

5 Kripke Semantics

5.1 Kripke Semantics by Filter

In [3, 4], Kripke semantics of FL_{σ} is defined as follows.

Definition 5.1 (Kripke model) ⟨D, 0, g⟩ is a Kripke model of FL_{σ} iff D is a so_{σ}-monoid, 0 ∈ 𝔽(D) where 0 = {ω} if w ∈ σ, and g is a map from propositional variables to 𝔽(D). The valuation relation x ⊧ α for x ∈ D and a formula α is defined by the following clauses.

1. x ⊧ p iff x ∈ g(p), if p is a propositional variable

2. x ⊧ 1 iff ϵ ≤ x,

3. x ⊧ 0 iff x ∈ 0,

4. x ⊧ ⊤, for every x,

5. x ⊧ ⊥ iff x = ω,

6. x ⊧ α → β iff, for every y and z, y ⊧ α and x · y ≤ z implies z ⊧ β,

7. x ⊧ α ∨ β iff, there exist y and z such that y ∩ z ≤ x, y ⊧ α and z ⊧ β,

8. x ⊧ α ∧ β iff x ⊧ α and x ⊧ β,

9. x ⊧ α ⋆ β iff, there exist y and z such that y · z ≤ x, y ⊧ α and z ⊧ β.

This Kripke semantics is shown to be sound by Th. 2.4, that is, by reading x ⊧ α as x ∈ [[α]]. We will give the Kripke semantics for FL_{σ}^{m} by paraphrasing the filter generation in the definition of modal operations of Th. 3.2.

Definition 5.2 A binary relation R is a filter relation if it satisfies the following.

1. if x ≤ y and x R z, then there exists z′ such that y R z′ and z ≤ z′

2. if x_{1} R y_{1} and x_{2} R y_{2}, then x_{1} ∩ x_{2} R y_{1} ∩ y_{2}

Definition 5.3 ⟨D, R, S, 0, g⟩ is a Kripke model of FL_{σ}^{m} iff ⟨D, 0, g⟩ is a Kripke model of FL_{σ}, R is a transitive relation on D, S is a reflexive and transitive relation on D, and the following conditions are satisfied.

1. R and S are filter relations

2. if x R y, then x ≥ y, y R y, and y ∈ Cent(D)

3. if x_{1} R y_{1} and x_{2} R y_{2}, then x_{1} · x_{2} R y_{1} · y_{2}

4. if x_{1} R y_{1} and x_{2} S y_{2}, then x_{1} · x_{2} S y_{1} · y_{2}

5. if z ∈ 0 and x S z, then x ∈ 0 The valuation relation x ⊧ α is defined by the clauses 1 – 9 in Def. 5.1 and the following clauses.

10. x ⊧ !α iff, there exists y such that x R y and y ⊧ α,

11. x ⊧ ?α iff, there exists y such that x S y and y ⊧ α.

Theorem 5.4 Let ⟨D, R, S, 0, g⟩ be a Kripke model of FL_{σ}^{m} and ! and ? be the following operations on 𝔽(D).

!a =^{def} {x | ∃y(x R y ∧ y ∈ a)} ?a =^{def} {x | ∃y(x S y ∧ y ∈ a)}

Then, FLA(D) with ! and ? is a modal FL_{σ}-algebra.

Proposition 5.5 Let ⟨FLA(D), I, ¿, 0⟩ be a modal so_{σ} phase structure that satisfies (¿ω)↑ ≥ 0. Put

Î =^{def} {x_{1} ∩ ⋯ ∩ x_{n} | x_{i} ∈ I, n ≥ 1} and define the relations R and S on D by x R y =^{def} x ≥ y ∧ y ∈ Î

and x S y =^{def} x ≥ ¿y. Then, ⟨D, R, S, 0, g⟩ is a Kripke model of FL_{σ}^{m} and it holds that x ∈ [[α]] in ⟨FLA(D), I, ¿, 0⟩ (where [[p]] = g(p) for a propositional variable p) iff x ⊧ α in ⟨D, R, S, 0, g⟩.

Theorem 5.6 FL_{σ}^{m} is complete with respect to the class of all Kripke models.

5.2 Traditional Kripke Semantics

Usually, □ of the intuitionistic modal logic is interpreted using universal quantifier, that is, in the simplest case, □ is interpreted like this: (□) x ⊧ □α iff, for every z, x R_{□} z implies z ⊧ α. Here, we consider the following clause. (dom(R) =^{def} {x | ∃y(x R y)}.)

(!) x ⊧ !α iff, there exists y ≤ x such that y ∈ dom(R_{!}) and for every y R_{!} z, z ⊧ α. We do not list the conditions R_{!} should satisfy (R_{!} is transitive, and so on), but just remark that the clause 10 in Def. 5.3 and the clause (!) have the common instance that is obtained by putting x R y =^{def} x ≥ y ∧ y ∈ R_{0} in 10 and y R_{!} z =^{def} y ∈ R_{0} ∧ y ≤ z in (!). If we can take y independently of α in (!), we write the y as r_{x} and have the clause of the form (□) by putting x R_{□} z =^{def} r_{x} R_{!} z. In the case of σ = ewc, we have an example.

Proposition 5.7 Let A be a modal FL_{ewc}-algebra and put D = SOM(A), r_{x} =^{def} F{u | !u ∈ x},

¿x =^{def} F{?u | u ∈ x}, and 0 =^{def} (0_{A}↑)↑ (0_{A} is 0 in A). Then, ⟨FLA(D), 0, g⟩ with x R z =^{def} r_{x} ≤ z and

x S z =^{def} x ≥ ¿z is a model of FL_{ewc}^{m} defined by the clauses 1 – 9 in Def. 5.1, the clause 11 in Def. 5.3, and 10’. x ⊧ !α iff, for every z, x R z implies z ⊧ α.

References

[1] J.-Y. Girard. Linear logc: its syntax and semantics. In Girard, Lafont, and Regnier, editors, Advances in Linear Logic. Cambridge Univ. Press, 1995.

[2] M. Okada. Phase semantics for higher order completeness, cut-elimination and normalization proofs (extended abstract). Electronic Notes in Theoretical Computer Science, 3, 1996.

   http://www.elsevier.nl/locate/entcs/volume3.html.

[3] H. Ono. Semantics for substructural logics. In K. Došen and P. Schroeder-Heister, editors, Substructural Logics, pages 259–291. Oxford Univ. Press, 1993.

[4] H. Ono and Y. Komori. Logics without the contraction rule. Journal of Symbolic Logic, 50:169–201, 1985.

[5] B. Surarso and H. Ono. Cut elimination in noncommutative substructural logics. Reports on Mathematical Logic, 30:13–29, 1996.

A Preliminaries

Definition A.1 (Lambek logic) FL initial sequents:

\begin{matrix}α ⊢ α & ⊢ 1 & 0 ⊢ \\ Γ ⊢ ⊤ & Γ, ⊥, Δ ⊢ θ \end{matrix}

rules for logical constants:

{Γ, Δ ⊢ θ \atop Γ, 1, Δ ⊢ θ} (1w)  {Γ ⊢ \atop Γ ⊢ 0} (0w)

cut and logical rules:

\begin{matrix}Γ ⊢ α & Δ, α, Σ ⊢ θ \\ Δ, Γ, Σ ⊢ θ \end{matrix} (cut)
\begin{matrix}Γ, α, Δ ⊢ θ & Γ, β, Δ ⊢ θ \\ Γ, α ∨ β, Δ ⊢ θ \end{matrix} (∨ ⊢)  {Γ ⊢ α \atop Γ ⊢ α ∨ β} (⊢ ∨1)  {Γ ⊢ β \atop Γ ⊢ α ∨ β} (⊢ ∨2)
{Γ, α, Σ ⊢ θ \atop Γ, α ∧ β, Σ ⊢ θ} (∧1 ⊢)  {Γ, β, Σ ⊢ θ \atop Γ, α ∧ β, Σ ⊢ θ} (∧2 ⊢)  \begin{matrix}Γ ⊢ α & Γ ⊢ β \\ Γ ⊢ α ∧ β \end{matrix} (⊢ ∧)
{Γ, α, β, Σ ⊢ θ \atop Γ, α ⋆ β, Σ ⊢ θ} (⋆ ⊢)  \begin{matrix}Γ ⊢ α & Δ ⊢ β \\ Γ, Δ ⊢ α ⋆ β \end{matrix} (⊢ ⋆)
\begin{matrix}Γ ⊢ α & Δ, β, Σ ⊢ θ \\ Δ, α → β, Γ, Σ ⊢ θ \end{matrix} (→⊢)  {Γ, α ⊢ β \atop Γ ⊢ α → β} (⊢→)

structural rules (optional): FL_{e} = FL +(e ⊢), FL_{c} = FL +(c ⊢), FL_{w} = FL +(w ⊢) + (⊢ w), FL_{ec} = FL_{e} + FL_{c}, ...

{Γ, α, β, Σ ⊢ θ \atop Γ, β, α, Σ ⊢ θ} (e ⊢)  {Γ, α, α, Σ ⊢ θ \atop Γ, α, Σ ⊢ θ} (c ⊢)  {Γ, Σ ⊢ θ \atop Γ, α, Σ ⊢ θ} (w ⊢)  {Γ ⊢ \atop Γ ⊢ θ} (⊢ w)

Definition A.2 (FL-algebra) A ≡ ⟨A, →, ∪, ∩, ⋆, 1, 0, ⊤, ⊥⟩ is an FL-algebra iff

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

2. ⟨A, ⋆, 1⟩ is a monoid with the identity 1,

3. c ⋆ (a ∪ b) ⋆ d = (c ⋆ a ⋆ d) ∪ (c ⋆ b ⋆ d), for every a, b, c, d ∈ A,

4. a ⋆ b ≤ c iff a ≤ b → c, for every a, b, c ∈ A,

5. 0 ∈ A.

(1) A is an FL_{e}-algebra iff ⟨A, ⋆, 1⟩ is a commutative monoid, (2) A is an FL_{w}-algebra iff (i) 0 = ⊥ and (ii) for every a, b ∈ A, both a ⋆ b ≤ a and a ⋆ b ≤ b hold, (3) A is an FL_{c}-algebra iff for every a ∈ A, a ≤ a ⋆ a holds.

Definition A.3 (so-monoid) D ≡ ⟨D, ∩, ·, ϵ, ω⟩ is an so-monoid iff

1. ⟨D, ∩⟩ is a meet-semilattice with the greatest element ω,

2. ⟨D, ·, ϵ⟩ is a monoid with the identity ϵ that satisfies x · ω = ω for x ∈ D,

3. z · (x ∩ y) · w = (z · x · w) ∩ (z · y · w), for every x, y, z, w ∈ D.

(1) D is an so_{e}-monoid iff ⟨D, ·, ϵ⟩ is a commutative monoid, (2) D is an so_{w}-monoid iff for every x, y ∈ D, both x ≤ x · y and y ≤ x · y hold, (3) D is an so_{c}-monoid iff for every x ∈ D, x · x ≤ x holds.

Definition A.4 (filter on meet-semilattice) Let L be a meet-semilattice with the greatest element ⊤. A subset F of L is a filter of L iff ⊤ ∈ F and for every x, y ∈ F and every z ∈ L, x ∩ y ≤ z implies z ∈ F. 𝔽(L) denotes the set of all filters on L, FU denotes the filter generated from the set U, and

x↑ =^{def} F{x}.

Definition A.5 (modal Lambek logic) FL_{σ}^{m} = FL_{σ} + the following rules

{Γ, α, Δ ⊢ θ \atop Γ,!α, Δ ⊢ θ} (! ⊢)  {!Γ ⊢ α \atop !Γ ⊢ !α} (⊢ !)
{Γ, Δ ⊢ θ \atop Γ,!α, Δ ⊢ θ} (!w)  {Γ,!α,!α, Δ ⊢ θ \atop Γ,!α, Δ ⊢ θ} (!c)  {Γ,!α, β, Δ ⊢ θ \atop Γ, β,!α, Δ ⊢ θ} (!e)  {Γ, β,!α, Δ ⊢ θ \atop Γ,!α, β, Δ ⊢ θ} (!e)
{!Γ, α,!Δ ⊢ ?θ \atop !Γ,?α,!Δ ⊢ ?θ} (? ⊢)  {Γ ⊢ α \atop Γ ⊢ ?α} (⊢ ?)  {Γ ⊢ \atop Γ ⊢ ?α} (?w)

Definition A.6 (modal FL_{σ}-algebra) FL_{σ}-algebra with additional unary operations ! and ? satisfying:

1. !a ≤ a  2. !1 = 1  3. !a ≤ !!a
4. !(a ∩ b) = !a ⋆!b  5. !a ⋆ b = b ⋆!a  6. !(a → b) ≤ ?a → ?b
7. a ≤ ?a  8. ?0 = 0  9. ??a ≤ ?a

10. 0 ≤ ?a

Lemma A.7

1. !a ≤ 1  2. !a ≤ !a ⋆!a
3. a ≤ b implies !a ≤ !b  4. a ≤ b implies ?a ≤ ?b

5. !a ⋆?b ≤ ?(a ⋆ b)