Cut-free Sequent Calculi for Visser’s Propositional Logics

Kentaro KIKUCHI

                           kentaro@jaist.ac.jp

School of Information Science, JAIST

1 Introduction

Visser [5] introduced Basic Propositional Logic (BPL) and Formal Propositional Logic (FPL) in the form of natural deduction systems which are complete with respect to transitive models and finite irreflexive transitive models, respectively. A sequent style formulation of BPL can be found in [1], but it is not satisfactory because it does not enjoy the subformula property. Here we introduce another sequent calculus for BPL as well as one for FPL, and show the admissibility of the cut rule through semantical completeness. These are extensions of systems in [2].

2 A sequent calculus for BPL

Definition 2.1 Formulas are constructed from {→, ∧, ∨, ⊥} and the set V of propositional variables. A sequent is an expression of the form Γ ⇒ Δ where Γ and Δ are finite sets of formulas. As far as sequents are concerned, we write A_{1}, ..., A_{n} for {A_{1}, ..., A_{n}}, and A, Γ for {A} ∪ Γ, etc.

Definition 2.2 A (transitive) model is a triple ⟨W, R, V ⟩ where W is a non-empty set, R is a transitive relation on W, and V is a mapping from V to 2^{W} such that x ∈ V (p) and xRy imply y ∈ V (p). If W is a finite set, we say that a model ⟨W, R, V ⟩ is finite. Given a model M = ⟨W, R, V ⟩, the truth-relation ⊧ is defined as follows:

(M, x) ⊧ p  iff x ∈ V (p) for each propositional variable p,
(M, x) |̸= ⊥,
(M, x) ⊧ A ∧ B iff (M, x) ⊧ A and (M, x) ⊧ B,
(M, x) ⊧ A ∨ B iff (M, x) ⊧ A or (M, x) ⊧ B,
(M, x) ⊧ A→B iff ∀y ∈ W [xRy and (M, y) ⊧ A imply (M, y) ⊧ B].

We say that a formula A is true in M if (M, x) ⊧ A for every x ∈ W. The truth-relation for sequents is defined by

(M, x) ⊧ Γ ⇒ Δ iff ∀A ∈ Γ[(M, x) ⊧ A] implies ∃A ∈ Δ[(M, x) ⊧ A].

We say that a sequent Γ ⇒ Δ is true in M if (M, x) ⊧ Γ ⇒ Δ for every x ∈ W.

Definition 2.3 The system LBP consists of the following initial sequents

\begin{matrix}A ⇒ A, \\ ⊥ ⇒ \end{matrix}

and the following rules of inference:

{Γ ⇒ Δ \atop A, Γ ⇒ Δ} (weakening left)  {Γ ⇒ Δ \atop Γ ⇒ Δ, A} (weakening right)

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

\begin{matrix}A, Γ ⇒ Δ & B, Γ ⇒ Δ \\ A ∨ B, Γ ⇒ Δ \end{matrix} (∨left)  {Γ ⇒ Δ, A, B \atop Γ ⇒ Δ, A ∨ B} (∨right)
Δ_{1}, Σ, A ⇒ B, Γ_{1} Δ_{2}, Σ, A ⇒ B, Γ_{2} ⋯ Δ_{2^{n}}, Σ, A ⇒ B, Γ_{2^{n}}

Σ, C_{1}→D_{1}, ..., C_{n}→D_{n} ⇒ A→B (→)

where n ≥ 0, Γ_{i} = {C_{j} | j ∈ γ(i)}, Δ_{i} = {D_{j} | j ∈ δ(i)}, and the sets γ(i) and δ(i) of natural numbers are defined as follows. Enumerate all the “partitions” of {1, ..., n}:

\begin{matrix}⟨\{\}, \{1, ..., n\}⟩, ⟨\{1\}, \{2, ..., n\}⟩, ⟨\{2\}, \{1, 3, ..., n\}⟩, ..., \\ ⟨\{1, 2\}, \{3, ..., n\}⟩, ⟨\{2, 3\}, \{1, 4, ..., n\}⟩, ..., ⟨\{1, ..., n\}, \{\}⟩. \end{matrix}

The number of the partitions is 2^{n}, and ⟨δ(i), γ(i)⟩ is defined to be the i-th partition. For example, when n = 0, 1, 2, the rule (→) is of the forms

{Σ, A ⇒ B \atop Σ ⇒ A→B} (→), \begin{matrix}Σ, A ⇒ B, C_{1} & D_{1}, Σ, A ⇒ B \\ Σ, C_{1}→D_{1} ⇒ A→B \end{matrix} (→),

\begin{aligned}Σ, A ⇒ B, C_{1}, C_{2} & D_{1}, Σ, A ⇒ B, C_{2} & D_{2}, Σ, A ⇒ B, C_{1} & D_{1}, D_{2}, Σ, A ⇒ B \\ & Σ, C_{1}→D_{1}, C_{2}→D_{2} ⇒ A→B \end{aligned} (→).

Theorem 2.4 (Soundness) If Γ ⇒ Δ is provable in LBP, then Γ ⇒ Δ is true in any model.

To prove the completeness theorem, we need the following notion.

Definition 2.5 A sequent Γ ⇒ Δ is said to be saturated if, for all formulas A, B,

A ∧ B ∈ Γ implies A ∈ Γ and B ∈ Γ,
A ∧ B ∈ Δ implies A ∈ Δ or B ∈ Δ,
A ∨ B ∈ Γ implies A ∈ Γ or B ∈ Γ,
A ∨ B ∈ Δ implies A ∈ Δ and B ∈ Δ.

Given a finite set Λ of formulas, S(Λ) is defined to be the set of all sequents Γ ⇒ Δ satisfying the following conditions:

• Γ ⇒ Δ is saturated,

• Γ ⇒ Δ is not provable in LBP,

• Γ ∪ Δ ⊆ Sub(Λ), where Sub(Λ) is the set of all the subformulas in Λ.

Lemma 2.6 If a sequent Γ ⇒ Δ is not provable in LBP, then there is a sequent Γ′ ⇒ Δ′ in S(Γ ∪ Δ) such that Γ ⊆ Γ′ and Δ ⊆ Δ′.

Theorem 2.7 (Completeness) Γ ⇒ Δ is provable in LBP if and only if Γ ⇒ Δ is true in any model.

(Sketch of proof) Suppose that Γ ⇒ Δ is not provable in LBP. Then by Lemma 2.6, there is a sequent Γ′ ⇒ Δ′ in S(Γ ∪ Δ) such that Γ ⊆ Γ′ and Δ ⊆ Δ′. Now define a model M = ⟨W, R, V ⟩ as follows:

• W = S(Γ ∪ Δ),

• (Σ ⇒ Θ)R(Φ ⇒ Ψ) iff Σ ⊆ Φ and ∀(A→B) ∈ Σ[A ∈ Ψ or B ∈ Φ],

• V (p) = {Σ ⇒ Θ ∈ W | p ∈ Σ}.

We can verify that R is transitive and that Σ ⇒ Θ ∈ V (p) and (Σ ⇒ Θ)R(Φ ⇒ Ψ) imply Φ ⇒ Ψ ∈ V (p). To see that Γ ⇒ Δ is not true in M because of (M, Γ′ ⇒ Δ′) |̸= Γ ⇒ Δ, it suffices to show that, for any sequent Σ ⇒ Θ ∈ W, ∀A ∈ Σ[(M, Σ ⇒ Θ) ⊧ A] and ∀A ∈ Θ[(M, Σ ⇒ Θ) |̸= A]. □

The above proof provides the model M based on the finite set W = S(Γ ∪ Δ). So we have Theorem 2.8 (Finite model property) If Γ ⇒ Δ is not provable in LBP, then there is a finite model in which Γ ⇒ Δ is not true.

As a consequence of the completeness theorem, we derive

Corollary 2.9 The rule

\begin{matrix}Γ ⇒ Δ, A & A, Γ ⇒ Δ \\ Γ ⇒ Δ \end{matrix} (cut)

is admissible in LBP.

3 A sequent calculus for FPL

Definition 3.1 An irreflexive model is a model ⟨W, R, V ⟩ in which R is irreflexive, i.e., there is no x ∈ W such that xRx.

Definition 3.2 The system LFP is obtained from LBP by providing the left hand side of each upper sequent in the rule (→) with the formula A→B. Then, the rule (→) of LFP is of the form

Δ_{1}, Σ, A→B, A ⇒ B, Γ_{1} Δ_{2}, Σ, A→B, A ⇒ B, Γ_{2} ⋯ Δ_{2^{n}}, Σ, A→B, A ⇒ B, Γ_{2^{n}}

Σ, C_{1}→D_{1}, ..., C_{n}→D_{n} ⇒ A→B (→)

where n ≥ 0, and Γ_{i} and Δ_{i} are as in the rule (→) of LBP.

Theorem 3.3 (Soundness) If Γ ⇒ Δ is provable in LFP, then Γ ⇒ Δ is true in any finite irreflexive model.

Theorem 3.4 (Completeness) Γ ⇒ Δ is provable in LFP if and only if Γ ⇒ Δ is true in any finite irreflexive model.

(Sketch of proof) We construct a model M = ⟨W, R, V ⟩ similar to that in the proof of Theorem 2.7 except that R is defined by

• (Σ ⇒ Θ)R(Φ ⇒ Ψ) iff Σ ⊊ Φ and ∀(A→B) ∈ Σ[A ∈ Ψ or B ∈ Φ].

We can verify that M defines a finite irreflexive model. The rest of the proof is similar to that of Theorem 2.7. □

Corollary 3.5 The rule

\begin{matrix}Γ ⇒ Δ, A & A, Γ ⇒ Δ \\ Γ ⇒ Δ \end{matrix} (cut)

is admissible in LFP.

4 Relationships with other systems

Definition 4.1 We define ⋀ Γ (⋁ Γ) as the conjunction (the disjunction) of all formulas in Γ if Γ is non-empty, as ⊥ → ⊥ (⊥, respectively) if Γ empty.

Definition 4.2 The Hilbert-style system HB [4] consists of the following axiom schemes and inference rule:

\begin{matrix}A → A & (A → B) ∧ (B → C) → (A → C) \\ A ∧ B → A & A ∧ B → B \\ (A → B) ∧ (A → C) → (A → B ∧ C) & A → A ∨ B \\ B → A ∨ B & (A → C) ∧ (B → C) → (A ∨ B → C) \\ A ∧ (B ∨ C) → (A ∧ B) ∨ (A ∧ C) & ⊥ → A \\ A → (B → A) & A → (B → A ∧ B) \end{matrix}

\begin{aligned}A & A → B \\ & B \end{aligned} (modus ponens).

Lemma 4.3 If A is provable in HB, then ⇒ A is provable in LBP.

Lemma 4.4 If Γ ⇒ Δ is provable in LBP, then ⋀ Γ → ⋁ Δ is provable in HB.

Combining Lemmas 4.3 and 4.4 with Theorem 2.7, we derive

Theorem 4.5 (Completeness of HB) A is provable in HB if and only if A is true in any model.

Definition 4.6 Sequents of the system GVPL^{+} [3] consist of finite sequences of formulas which are possibly of the form (A → B)^{+} where A and B are ordinary ones. The system GVPL^{+} consists of the following initial sequents

\begin{matrix}A ⇒ A, \\ ⊥ ⇒ \end{matrix}

and the following rules of inference:

\begin{matrix}Γ ⇒ A & Γ ⇒ B \\ Γ ⇒ A ∧ B \end{matrix} (⇒ ∧)  {A, Γ ⇒ Δ \atop A ∧ B, Γ ⇒ Δ} (∧ ⇒_{1})  {B, Γ ⇒ Δ \atop A ∧ B, Γ ⇒ Δ} (∧ ⇒_{2})
{Γ ⇒ A \atop Γ ⇒ A ∨ B} (⇒ ∨_{1})  {Γ ⇒ B \atop Γ ⇒ A ∨ B} (⇒ ∨_{2})  \begin{matrix}A, Γ ⇒ Δ & B, Γ ⇒ Δ \\ A ∨ B, Γ ⇒ Δ \end{matrix} (∨ ⇒)
{A, Γ^{+} ⇒ B \atop Γ ⇒ A → B} (⇒→)  {A, Γ ⇒ B \atop Γ ⇒ (A → B)^{+}} (⇒→^{+})  \begin{matrix}Γ ⇒ A & B, Π ⇒ Δ \\ (A → B)^{+}, Γ, Π ⇒ Δ \end{matrix} (→^{+}⇒)
{Γ ⇒ \atop Γ ⇒ D} (⇒ T)  {Γ ⇒ Δ \atop D, Γ ⇒ Δ} (T ⇒)  {D, D, Γ ⇒ Δ \atop D, Γ ⇒ Δ} (C ⇒)
{Γ, C, D, Π ⇒ Δ \atop Γ, D, C, Π ⇒ Δ} (I ⇒)  \begin{matrix}Γ ⇒ D & D, Π ⇒ Δ \\ Γ, Π ⇒ Δ \end{matrix} (cut)

where Δ is the empty sequence or a formula, and Γ^{+} is obtained from Γ by replacing every C → D with (C → D)^{+}.

In the following, we let Γ denote both a finite set of ordinary formulas and a finite sequence of them, and let A denote an ordinary formula.

Lemma 4.7 If Γ ⇒ Δ is provable in LBP, then Γ ⇒ ⋁ Δ is provable in GVPL^{+}.

Lemma 4.8 If Γ, Σ ⇒ A is provable in GVPL^{+}, then Σ^{−} ⇒ ⋀ Γ → A is provable in LBP, where Σ^{−} is obtained from Σ by replacing every (C → D)^{+} with C → D.

Theorem 4.9 Γ ⇒ A is provable in LBP if and only if Γ ⇒ A is provable in GVPL^{+}.

Definition 4.10 The system GFPL^{+} [3] is obtained from GVPL^{+} by replacing (⇒→) with

{A, A → B, Γ^{+} ⇒ B \atop Γ ⇒ A → B} (⇒→_{f}).

Lemmas 4.7, 4.8, and Theorem 4.9 hold also between LFP and GFPL^{+}.

References

[1] M. Ardeshir. Aspects of Basic Logic. PhD thesis, Marquette University, Milwaukee, 1995.

[2] R. Kashima. Sequent calculi for strict implications. manuscript, 1997.

[3] K. Sasaki. Cut-elimination theorem for Visser’s propositional logic and formal propositional logic. submitted, 1998.

[4] Y. Suzuki and H. Ono. Hilbert style proof system for BPL. Research Report IS-RR-97-0040F, JAIST, 1997.

[5] A. Visser. A propositional logic with explicit fixed points. Studia Logica, 40:155–175, 1981.