Sequent calculi and interpolation for non-normal modal and deonticlogics

Eugenio Orlandelli

arXiv:1903.11342·math.LO·February 20, 2020

Sequent calculi and interpolation for non-normal modal and deonticlogics

Eugenio Orlandelli

PDF

TL;DR

This paper develops sequent calculi for non-normal modal and deontic logics, proving key properties like cut admissibility and subformula property, and establishing their soundness, completeness, and interpolation results.

Contribution

It introduces G3-style sequent calculi for these logics, demonstrating their admissibility, decidability, and equivalence to axiomatic systems, with new interpolation proofs.

Findings

01

Calculi are sound and complete with respect to neighbourhood semantics

02

Weakening and contraction are height-preserving admissible

03

Decidability is in PSPACE

Abstract

G3-style sequent calculi for the logics in the cube of non-normal modal logics and for their deontic extensions are studied. For each calculus we prove that weakening and contraction are height-preserving admissible, and we give a syntactic proof of the admissibility of cut. This implies that the subformula property holds and that derivability can be decided by a terminating proof search whose complexity is in PSPACE. These calculi are shown to be equivalent to the axiomatic ones and, therefore, they are sound and complete with respect to neighbourhood semantics. Finally, it is given a Maehara-style proof of Craig's interpolation theorem for most of the logics considered.

Tables3

Table 1. Table 1: Rules of inference

$\begin{matrix} A \leftrightarrow B & 𝑅𝐸 \\ \overline{□ A \leftrightarrow □ B} \end{matrix}$		$\begin{matrix} A \supset B & 𝑅𝑀 \\ \overline{□ A \supset □ B} \end{matrix}$
$\begin{matrix} (A_{1} \land \dots \land A_{n}) \supset B & 𝑅𝑅, n \geq 1 \\ \overline{(□ A_{1} \land \dots \land □ A_{n}) \supset □ B} \end{matrix}$		$\begin{matrix} (A_{1} \land \dots \land A_{n}) \supset B & 𝑅𝐾, n \geq 0 \\ \overline{(□ A_{1} \land \dots \land □ A_{n}) \supset □ B} \end{matrix}$

Table 2. Table 2: Axioms

$M$ )	$□ (A \land B) \supset (□ A \land □ B)$	$C$ )	$(□ A \land □ B) \supset □ (A \land B)$
$N$ )	$□ ⊤$	$D^{⊥}$ )	$\neg □ ⊥$
$D^{◇}$ )	$□ A \supset ◇ A$

Table 3. Table 3: The sequent calculus G3cp

Initial sequents:	$p_{n}, Γ ⟹ Δ, p_{n}$	$p_{n}$ propositional variable
Propositional rules:	$\begin{matrix} A, B, Γ ⟹ Δ & L \land \\ \overline{A \land B, Γ ⟹ Δ} \end{matrix}$	$\begin{matrix} Γ ⟹ Δ, A Γ ⟹ Δ, B & R \land \\ \overline{Γ ⟹ Δ, A \land B} \end{matrix}$
$\begin{matrix} L ⊥ \\ \overline{⊥, Γ ⟹ Δ} \end{matrix}$	$\begin{matrix} A, Γ ⟹ Δ B, Γ ⟹ Δ & L \lor \\ \overline{A \lor B, Γ ⟹ Δ} \end{matrix}$	$\begin{matrix} Γ ⟹ Δ, A, B & R \lor \\ \overline{Γ ⟹ Δ, A \lor B} \end{matrix}$
	$\begin{matrix} Γ ⟹ Δ, A B, Γ ⟹ Δ & L \supset \\ \overline{A \supset B, Γ ⟹ Δ} \end{matrix}$	$\begin{matrix} A, Γ ⟹ Δ, B & R \supset \\ \overline{Γ ⟹ Δ, A \supset B} \end{matrix}$

Equations158

□ A, □ B, Γ ⟹ Δ \lx@proof@logical@and A, B ⟹ (⟹ A, B)

□ A, □ B, Γ ⟹ Δ \lx@proof@logical@and A, B ⟹ (⟹ A, B)

⟹ \neg □ ⊥ □ ⊥ ⟹ \lx@proof@logical@and ⟹ □ ⊤ ⟹ ⊤ □ ⊤, □ ⊥ ⟹ \lx@proof@logical@and ⊥, ⊤ ⟹⟹ ⊥, ⊤

⟹ \neg □ ⊥ □ ⊥ ⟹ \lx@proof@logical@and ⟹ □ ⊤ ⟹ ⊤ □ ⊤, □ ⊥ ⟹ \lx@proof@logical@and ⊥, ⊤ ⟹⟹ ⊥, ⊤

A ::= p_{n} ∣ ⊥ ∣ A \land A ∣ A \lor A ∣ A \supset A ∣ □ A

A ::= p_{n} ∣ ⊥ ∣ A \land A ∣ A \lor A ∣ A \supset A ∣ □ A

⊨_{w}^{M} □ A iff ∣∣ A ∣ ∣^{M} \in N (w)

⊨_{w}^{M} □ A iff ∣∣ A ∣ ∣^{M} \in N (w)

□ B, Γ ⟹ Δ, □ B B ⟹ B

□ B, Γ ⟹ Δ, □ B B ⟹ B

A, Γ ⟹ ΔΓ ⟹ Δ Γ ⟹ Δ, A Γ ⟹ Δ

A, Γ ⟹ ΔΓ ⟹ Δ Γ ⟹ Δ, A Γ ⟹ Δ

□ B, Γ ⟹ Δ, □ C \lx@proof@logical@and B ⟹ C ⋮ D_{1} C ⟹ B ⋮ D_{2} \mbox in t o □ B, A, Γ ⟹ Δ, □ C \lx@proof@logical@and B ⟹ C ⋮ D_{1} C ⟹ B ⋮ D_{2}

□ B, Γ ⟹ Δ, □ C \lx@proof@logical@and B ⟹ C ⋮ D_{1} C ⟹ B ⋮ D_{2} \mbox in t o □ B, A, Γ ⟹ Δ, □ C \lx@proof@logical@and B ⟹ C ⋮ D_{1} C ⟹ B ⋮ D_{2}

A \supset ⊥, Γ ⟹ Δ \lx@proof@logical@and Γ ⟹ Δ, A ⊥, Γ ⟹ Δ Γ ⟹ Δ, A \supset ⊥ A, Γ ⟹ Δ, ⊥ A, Γ ⟹ Δ

A \supset ⊥, Γ ⟹ Δ \lx@proof@logical@and Γ ⟹ Δ, A ⊥, Γ ⟹ Δ Γ ⟹ Δ, A \supset ⊥ A, Γ ⟹ Δ, ⊥ A, Γ ⟹ Δ

A, Γ ⟹ Δ A, A, Γ ⟹ Δ Γ ⟹ Δ, A Γ ⟹ Δ, A, A

A, Γ ⟹ Δ A, A, Γ ⟹ Δ Γ ⟹ Δ, A Γ ⟹ Δ, A, A

□ B, Γ ⟹ Δ □ B, □ B, Γ ⟹ Δ \lx@proof@logical@and B, B ⟹ ⋮ D_{1} ⟹ B, B ⋮ D_{2} into □ B, Γ ⟹ Δ \lx@proof@logical@and B ⟹ ⋮ I H (D_{1}) ⟹ B ⋮ I H (D_{2})

□ B, Γ ⟹ Δ □ B, □ B, Γ ⟹ Δ \lx@proof@logical@and B, B ⟹ ⋮ D_{1} ⟹ B, B ⋮ D_{2} into □ B, Γ ⟹ Δ \lx@proof@logical@and B ⟹ ⋮ I H (D_{1}) ⟹ B ⋮ I H (D_{2})

□ B, Γ^{'} ⟹ Δ^{'}, A, □ C □ B, Γ^{'} ⟹ Δ^{'}, A, A, □ C B ⟹ C ⋮ D_{1} \mbox in t o □ B, Γ^{'} ⟹ Δ^{'}, A, □ C B ⟹ C ⋮ D_{1}

□ B, Γ^{'} ⟹ Δ^{'}, A, □ C □ B, Γ^{'} ⟹ Δ^{'}, A, A, □ C B ⟹ C ⋮ D_{1} \mbox in t o □ B, Γ^{'} ⟹ Δ^{'}, A, □ C B ⟹ C ⋮ D_{1}

Γ, Π ⟹ Δ, Σ \lx@proof@logical@and Γ ⟹ Δ, D ⋮ D_{1} D, Π ⟹ Σ ⋮ D_{2}

Γ, Π ⟹ Δ, Σ \lx@proof@logical@and Γ ⟹ Δ, D ⋮ D_{1} D, Π ⟹ Σ ⋮ D_{2}

□ A, Γ^{'}, Π ⟹ Δ^{'}, □ B, Σ \lx@proof@logical@and □ A, Γ^{'} ⟹ Δ^{'}, □ B, D \lx@proof@logical@and A ⟹ B ⋮ D_{11} B ⟹ A ⋮ D_{12} D, Π ⟹ Σ ⋮ D_{2} \mbox in t o □ A, Γ^{'}, Π ⟹ Δ^{'}, □ B, Σ \lx@proof@logical@and A ⟹ B ⋮ D_{11} B ⟹ A ⋮ D_{12}

□ A, Γ^{'}, Π ⟹ Δ^{'}, □ B, Σ \lx@proof@logical@and □ A, Γ^{'} ⟹ Δ^{'}, □ B, D \lx@proof@logical@and A ⟹ B ⋮ D_{11} B ⟹ A ⋮ D_{12} D, Π ⟹ Σ ⋮ D_{2} \mbox in t o □ A, Γ^{'}, Π ⟹ Δ^{'}, □ B, Σ \lx@proof@logical@and A ⟹ B ⋮ D_{11} B ⟹ A ⋮ D_{12}

□ A, Γ^{'}, Π ⟹ Δ, Σ \lx@proof@logical@and □ A, Γ^{'} ⟹ Δ, D A ⟹ ⋮ D_{11} D, Π ⟹ Σ ⋮ D_{2} \mbox in t o □ A, Γ^{'}, Π ⟹ Δ, Σ A ⟹ ⋮ D_{11}

□ A, Γ^{'}, Π ⟹ Δ, Σ \lx@proof@logical@and □ A, Γ^{'} ⟹ Δ, D A ⟹ ⋮ D_{11} D, Π ⟹ Σ ⋮ D_{2} \mbox in t o □ A, Γ^{'}, Π ⟹ Δ, Σ A ⟹ ⋮ D_{11}

□ A, Γ^{'}, Π ⟹ Δ, Σ^{'}, □ B \lx@proof@logical@and □ A, Γ^{'} ⟹ Δ, □ C \lx@proof@logical@and A ⟹ C ⋮ D_{11} C ⟹ A ⋮ D_{12} □ C, Π ⟹ Σ^{'}, □ B \lx@proof@logical@and C ⟹ B ⋮ D_{21} B ⟹ C ⋮ D_{22}

□ A, Γ^{'}, Π ⟹ Δ, Σ^{'}, □ B \lx@proof@logical@and □ A, Γ^{'} ⟹ Δ, □ C \lx@proof@logical@and A ⟹ C ⋮ D_{11} C ⟹ A ⋮ D_{12} □ C, Π ⟹ Σ^{'}, □ B \lx@proof@logical@and C ⟹ B ⋮ D_{21} B ⟹ C ⋮ D_{22}

□ A, Γ^{'}, Π ⟹ Δ, Σ^{'}, □ B \lx@proof@logical@and A ⟹ B \lx@proof@logical@and A ⟹ C ⋮ D_{11} C ⟹ B ⋮ D_{21} B ⟹ A \lx@proof@logical@and B ⟹ C ⋮ D_{22} C ⟹ A ⋮ D_{12}

□ A, Γ^{'}, Π ⟹ Δ, Σ^{'}, □ B \lx@proof@logical@and A ⟹ B \lx@proof@logical@and A ⟹ C ⋮ D_{11} C ⟹ B ⋮ D_{21} B ⟹ A \lx@proof@logical@and B ⟹ C ⋮ D_{22} C ⟹ A ⋮ D_{12}

Γ, Π ⟹ Δ, Σ^{'}, □ A \lx@proof@logical@and Γ ⟹ Δ, □ C ⟹ C ⋮ D_{11} □ C, Π ⟹ Σ^{'}, □ A \lx@proof@logical@and C ⟹ A ⋮ D_{21} A ⟹ C ⋮ D_{22} \mbox in t o Γ, Π ⟹ Δ, Σ^{'}, □ A ⟹ A \lx@proof@logical@and ⟹ C ⋮ D_{11} C ⟹ A ⋮ D_{21}

Γ, Π ⟹ Δ, Σ^{'}, □ A \lx@proof@logical@and Γ ⟹ Δ, □ C ⟹ C ⋮ D_{11} □ C, Π ⟹ Σ^{'}, □ A \lx@proof@logical@and C ⟹ A ⋮ D_{21} A ⟹ C ⋮ D_{22} \mbox in t o Γ, Π ⟹ Δ, Σ^{'}, □ A ⟹ A \lx@proof@logical@and ⟹ C ⋮ D_{11} C ⟹ A ⋮ D_{21}

□ A, Γ^{'}, Π ⟹ Δ, Σ \lx@proof@logical@and □ A, Γ^{'} ⟹ Δ, □ C \lx@proof@logical@and A ⟹ C ⋮ D_{11} C ⟹ A ⋮ D_{12} □ C, Π ⟹ Σ C ⟹ ⋮ D_{21} \mbox in t o □ A, Γ^{'}, Π ⟹ Δ, Σ A ⟹ \lx@proof@logical@and A ⟹ C ⋮ D_{11} C ⟹ ⋮ D_{21}

□ A, Γ^{'}, Π ⟹ Δ, Σ \lx@proof@logical@and □ A, Γ^{'} ⟹ Δ, □ C \lx@proof@logical@and A ⟹ C ⋮ D_{11} C ⟹ A ⋮ D_{12} □ C, Π ⟹ Σ C ⟹ ⋮ D_{21} \mbox in t o □ A, Γ^{'}, Π ⟹ Δ, Σ A ⟹ \lx@proof@logical@and A ⟹ C ⋮ D_{11} C ⟹ ⋮ D_{21}

□ A, Γ^{'}, □ Ξ, Π^{'} ⟹ Δ, Σ \lx@proof@logical@and □ A, Γ^{'} ⟹ Δ, □ C \lx@proof@logical@and A ⟹ C ⋮ D_{11} C ⟹ A ⋮ D_{12} □ C, □ Ξ, Π^{'} ⟹ Σ \lx@proof@logical@and C, Ξ ⟹ ⋮ D_{21} ⟹ C, Ξ ⋮ D_{22} into □ A, Γ^{'}, □ Ξ, Π^{'} ⟹ Δ, Σ \lx@proof@logical@and ⟹ Ξ, A \lx@proof@logical@and ⟹ Ξ, C ⋮ D_{22} C ⟹ A ⋮ D_{12} A, Ξ ⟹ \lx@proof@logical@and A ⟹ C ⋮ D_{11} C, Ξ ⟹ ⋮ D_{21}

□ A, Γ^{'}, □ Ξ, Π^{'} ⟹ Δ, Σ \lx@proof@logical@and □ A, Γ^{'} ⟹ Δ, □ C \lx@proof@logical@and A ⟹ C ⋮ D_{11} C ⟹ A ⋮ D_{12} □ C, □ Ξ, Π^{'} ⟹ Σ \lx@proof@logical@and C, Ξ ⟹ ⋮ D_{21} ⟹ C, Ξ ⋮ D_{22} into □ A, Γ^{'}, □ Ξ, Π^{'} ⟹ Δ, Σ \lx@proof@logical@and ⟹ Ξ, A \lx@proof@logical@and ⟹ Ξ, C ⋮ D_{22} C ⟹ A ⋮ D_{12} A, Ξ ⟹ \lx@proof@logical@and A ⟹ C ⋮ D_{11} C, Ξ ⟹ ⋮ D_{21}

Γ, Π ⟹ Δ, Σ \lx@proof@logical@and Γ ⟹ Δ, □ C ⟹ C ⋮ D_{11} □ C, Π ⟹ Σ C ⟹ ⋮ D_{21} \mbox in t o Γ, Π ⟹ Δ, Σ C ⟹ \lx@proof@logical@and ⟹ C ⋮ D_{11} C ⟹ ⋮ D_{21}

Γ, Π ⟹ Δ, Σ \lx@proof@logical@and Γ ⟹ Δ, □ C ⟹ C ⋮ D_{11} □ C, Π ⟹ Σ C ⟹ ⋮ D_{21} \mbox in t o Γ, Π ⟹ Δ, Σ C ⟹ \lx@proof@logical@and ⟹ C ⋮ D_{11} C ⟹ ⋮ D_{21}

□ Ξ, Γ, Π^{'} ⟹ Δ, Σ \lx@proof@logical@and Γ ⟹ Δ, □ C ⟹ C ⋮ D_{11} □ C, □ Ξ, Π^{'} ⟹ Σ \lx@proof@logical@and C, Ξ ⋮ D_{21} ⟹⟹ C, Ξ ⋮ D_{22} into □ Ξ, Γ, Π^{'} ⟹ Δ, ΣΞ ⟹ \lx@proof@logical@and ⟹ C ⋮ D_{11} C, Ξ ⟹ ⋮ D_{21}

□ Ξ, Γ, Π^{'} ⟹ Δ, Σ \lx@proof@logical@and Γ ⟹ Δ, □ C ⟹ C ⋮ D_{11} □ C, □ Ξ, Π^{'} ⟹ Σ \lx@proof@logical@and C, Ξ ⋮ D_{21} ⟹⟹ C, Ξ ⋮ D_{22} into □ Ξ, Γ, Π^{'} ⟹ Δ, ΣΞ ⟹ \lx@proof@logical@and ⟹ C ⋮ D_{11} C, Ξ ⟹ ⋮ D_{21}

□ A, Γ^{'}, Π ⟹ Δ, Σ^{'}, □ B \lx@proof@logical@and □ A, Γ^{'} ⟹ Δ, □ C A ⟹ C ⋮ D_{11} □ C, Π ⟹ Σ^{'}, □ B C ⟹ B ⋮ D_{21} \mbox in t o □ A, Γ^{'}, Π ⟹ Δ, Σ^{'}, □ B A ⟹ B \lx@proof@logical@and A ⟹ C ⋮ D_{11} C ⟹ B ⋮ D_{21}

□ A, Γ^{'}, Π ⟹ Δ, Σ^{'}, □ B \lx@proof@logical@and □ A, Γ^{'} ⟹ Δ, □ C A ⟹ C ⋮ D_{11} □ C, Π ⟹ Σ^{'}, □ B C ⟹ B ⋮ D_{21} \mbox in t o □ A, Γ^{'}, Π ⟹ Δ, Σ^{'}, □ B A ⟹ B \lx@proof@logical@and A ⟹ C ⋮ D_{11} C ⟹ B ⋮ D_{21}

□ Λ, Γ^{'}, □ Ξ, Π^{'} ⟹ Δ, Σ^{'}, □ E \lx@proof@logical@and □ Λ, Γ^{'} ⟹ Δ, □ C \lx@proof@logical@and Λ ⟹ C ⋮ D_{11} C ⟹ A_{1} ⋮ D_{A_{1}}^{\dots} C ⟹ A_{n} ⋮ D_{A_{n}} □ C, □ Ξ, Π^{'} ⟹ Σ^{'}, □ E \lx@proof@logical@and C, Ξ ⟹ E ⋮ D_{21} E ⟹ C ⋮ D_{C}^{\dots} E ⟹ B_{m} ⋮ D_{B_{m}}

□ Λ, Γ^{'}, □ Ξ, Π^{'} ⟹ Δ, Σ^{'}, □ E \lx@proof@logical@and □ Λ, Γ^{'} ⟹ Δ, □ C \lx@proof@logical@and Λ ⟹ C ⋮ D_{11} C ⟹ A_{1} ⋮ D_{A_{1}}^{\dots} C ⟹ A_{n} ⋮ D_{A_{n}} □ C, □ Ξ, Π^{'} ⟹ Σ^{'}, □ E \lx@proof@logical@and C, Ξ ⟹ E ⋮ D_{21} E ⟹ C ⋮ D_{C}^{\dots} E ⟹ B_{m} ⋮ D_{B_{m}}

□ Λ, Γ^{'}, □ Ξ, Π^{'} ⟹ Δ, Σ^{'}, □ E \lx@proof@logical@and Λ, Ξ ⟹ E \lx@proof@logical@and Λ ⟹ C ⋮ D_{11} C, Ξ ⟹ E ⋮ D_{21} E ⟹ A_{1} \lx@proof@logical@and E ⟹ C ⋮ D_{C} C ⟹ A_{1} ⋮ D_{A_{n}} E ⟹ A_{n} \lx@proof@logical@and E ⟹ C ⋮ D_{C} C ⟹ A_{n} ⋮ D_{A_{n}} E ⟹ B_{1} ⋮ D_{B_{1}}^{\dots} E ⟹ B_{m} ⋮ D_{B_{m}}

□ Λ, Γ^{'}, □ Ξ, Π^{'} ⟹ Δ, Σ^{'}, □ E \lx@proof@logical@and Λ, Ξ ⟹ E \lx@proof@logical@and Λ ⟹ C ⋮ D_{11} C, Ξ ⟹ E ⋮ D_{21} E ⟹ A_{1} \lx@proof@logical@and E ⟹ C ⋮ D_{C} C ⟹ A_{1} ⋮ D_{A_{n}} E ⟹ A_{n} \lx@proof@logical@and E ⟹ C ⋮ D_{C} C ⟹ A_{n} ⋮ D_{A_{n}} E ⟹ B_{1} ⋮ D_{B_{1}}^{\dots} E ⟹ B_{m} ⋮ D_{B_{m}}

Γ, □ A_{1}, \dots, □ A_{n}, Π^{'} ⟹ Δ, Σ^{'}, □ B \lx@proof@logical@and Γ ⟹ Δ, □ C ⟹ C ⋮ D_{11} □ C, □ A_{1}, \dots, □ A_{n}, Π^{'} ⟹ Σ^{'}, □ B \lx@proof@logical@and C, A_{1}, \dots, A_{n} ⟹ B ⋮ D_{21} B ⟹ C ⋮ D_{C}^{\dots} B ⟹ A_{n} ⋮ D_{A_{n}}

Γ, □ A_{1}, \dots, □ A_{n}, Π^{'} ⟹ Δ, Σ^{'}, □ B \lx@proof@logical@and Γ ⟹ Δ, □ C ⟹ C ⋮ D_{11} □ C, □ A_{1}, \dots, □ A_{n}, Π^{'} ⟹ Σ^{'}, □ B \lx@proof@logical@and C, A_{1}, \dots, A_{n} ⟹ B ⋮ D_{21} B ⟹ C ⋮ D_{C}^{\dots} B ⟹ A_{n} ⋮ D_{A_{n}}

Γ, □ A_{1}, \dots □ A_{n}, Π^{'} ⟹ Δ, Σ^{'}, □ B \lx@proof@logical@and A_{1}, \dots, A_{n} ⟹ B \lx@proof@logical@and ⟹ C ⋮ D_{11} C, A_{1}, \dots, A_{n} ⟹ B ⋮ D_{21} B ⟹ A_{1} ⋮ D_{A_{1}}^{\dots} B ⟹ A_{n} ⋮ D_{A_{n}}

Γ, □ A_{1}, \dots □ A_{n}, Π^{'} ⟹ Δ, Σ^{'}, □ B \lx@proof@logical@and A_{1}, \dots, A_{n} ⟹ B \lx@proof@logical@and ⟹ C ⋮ D_{11} C, A_{1}, \dots, A_{n} ⟹ B ⋮ D_{21} B ⟹ A_{1} ⋮ D_{A_{1}}^{\dots} B ⟹ A_{n} ⋮ D_{A_{n}}

Γ, Π^{'} ⟹ Δ, Σ^{'}, □ B ⟹ B \lx@proof@logical@and ⟹ C ⋮ D_{11} C ⟹ B ⋮ D_{21}

Γ, Π^{'} ⟹ Δ, Σ^{'}, □ B ⟹ B \lx@proof@logical@and ⟹ C ⋮ D_{11} C ⟹ B ⋮ D_{21}

□ Ξ, □ B_{1}, \dots, □ B_{m}, □ Λ, Γ^{'}, Π^{'} ⟹ Δ, Σ \lx@proof@logical@and □ Ξ, Γ^{'} ⟹ Δ, □ C \lx@proof@logical@and Ξ ⟹ C ⋮ D_{11} {C ⟹ A_{i} ∣ A_{i} \in Ξ} ⋮ D_{1 A_{i}} □ C, □ B_{2}, \dots, □ B_{m}, □ Λ, Π^{'} ⟹ Σ \lx@proof@logical@and Θ, Λ ⟹ ⋮ D_{21} {⟹ E, D_{j} ∣ E \in Θ and D_{j} \in Λ} ⋮ D_{Θ_{i} Λ_{j}}

□ Ξ, □ B_{1}, \dots, □ B_{m}, □ Λ, Γ^{'}, Π^{'} ⟹ Δ, Σ \lx@proof@logical@and □ Ξ, Γ^{'} ⟹ Δ, □ C \lx@proof@logical@and Ξ ⟹ C ⋮ D_{11} {C ⟹ A_{i} ∣ A_{i} \in Ξ} ⋮ D_{1 A_{i}} □ C, □ B_{2}, \dots, □ B_{m}, □ Λ, Π^{'} ⟹ Σ \lx@proof@logical@and Θ, Λ ⟹ ⋮ D_{21} {⟹ E, D_{j} ∣ E \in Θ and D_{j} \in Λ} ⋮ D_{Θ_{i} Λ_{j}}

□ Ξ, □ B_{1}, \dots, □ B_{m}, □ Λ, Γ^{'}, Π^{'} ⟹ Δ, Σ \lx@proof@logical@and Ξ, B_{2}, \dots, B_{m}, Λ ⟹ \lx@proof@logical@and Ξ ⟹ C ⋮ D_{11} C, B_{2}, \dots, B_{m}, Λ ⟹ ⋮ D_{21} {⟹ A_{i}, D_{j} ∣ A_{i} \in Ξ, D_{j} \in Λ} \lx@proof@logical@and ⟹ D_{j}, C ⋮ D_{Θ_{1}, Λ_{j}} C ⟹ A_{i} ⋮ D_{1 A_{i}} {⟹ B_{i}, D_{j} ∣ B_{i} \in Θ - C, D_{j} \in Λ} ⋮ D_{Θ_{i} Λ_{j}}

□ Ξ, □ B_{1}, \dots, □ B_{m}, □ Λ, Γ^{'}, Π^{'} ⟹ Δ, Σ \lx@proof@logical@and Ξ, B_{2}, \dots, B_{m}, Λ ⟹ \lx@proof@logical@and Ξ ⟹ C ⋮ D_{11} C, B_{2}, \dots, B_{m}, Λ ⟹ ⋮ D_{21} {⟹ A_{i}, D_{j} ∣ A_{i} \in Ξ, D_{j} \in Λ} \lx@proof@logical@and ⟹ D_{j}, C ⋮ D_{Θ_{1}, Λ_{j}} C ⟹ A_{i} ⋮ D_{1 A_{i}} {⟹ B_{i}, D_{j} ∣ B_{i} \in Θ - C, D_{j} \in Λ} ⋮ D_{Θ_{i} Λ_{j}}

□ A, □ Ξ, Γ^{'}, □ Ψ, Π^{'} ⟹ Δ, Σ^{'}, □ B \lx@proof@logical@and □ A, □ Ξ, Γ^{'} ⟹ Δ, □ C A, Ξ ⟹ C ⋮ D_{11} □ C, □ Ψ, Π^{'} ⟹ Σ^{'}, □ B C, Ψ ⟹ B ⋮ D_{21} \mbox in t o □ A, □ Ξ, Γ^{'}, □ Ψ, Π^{'} ⟹ Δ, Σ^{'}, □ B A, Ξ, Ψ ⟹ B \lx@proof@logical@and A, Ξ ⟹ C ⋮ D_{11} C, Ψ ⟹ B ⋮ D_{21}

□ A, □ Ξ, Γ^{'}, □ Ψ, Π^{'} ⟹ Δ, Σ^{'}, □ B \lx@proof@logical@and □ A, □ Ξ, Γ^{'} ⟹ Δ, □ C A, Ξ ⟹ C ⋮ D_{11} □ C, □ Ψ, Π^{'} ⟹ Σ^{'}, □ B C, Ψ ⟹ B ⋮ D_{21} \mbox in t o □ A, □ Ξ, Γ^{'}, □ Ψ, Π^{'} ⟹ Δ, Σ^{'}, □ B A, Ξ, Ψ ⟹ B \lx@proof@logical@and A, Ξ ⟹ C ⋮ D_{11} C, Ψ ⟹ B ⋮ D_{21}

Peer Reviews

No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.

Videos

No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.

Full text

11institutetext:

Sequent Calculi and Interpolation for Non-Normal Modal and Deontic Logics

Eugenio Orlandelli

Abstract

G3-style sequent calculi for the logics in the cube of non-normal modal logics and for their deontic extensions are studied. For each calculus we prove that weakening and contraction are height-preserving admissible, and we give a syntactic proof of the admissibility of cut. This implies that the subformula property holds and that derivability can be decided by a terminating proof search whose complexity is in Pspace. These calculi are shown to be equivalent to the axiomatic ones and, therefore, they are sound and complete with respect to neighbourhood semantics. Finally, it is given a Maehara-style proof of Craig’s interpolation theorem for most of the logics considered.

Keywords: Non-normal logics, deontic logics, sequent calculi, structural proof theory, interpolation, decidability.

0.1 Introduction

For many interpretations of the modal operators – e.g., for deontic, epistemic, game-theoretic, and high-probability interpretations – it is necessary to adopt logics that are weaker than the normal ones; e.g., deontic paradoxes, see [12, 15], are one of the main motivations for adopting a non-normal deontic logic. Non-normal logics, see [4] for naming conventions, are quite well understood from a semantic point of view by means of neighbourhood semantics [14, 31]. Nevertheless, until recent years their proof theory has been rather limited since it was mostly confined to Hilbert-style axiomatic systems. This situation seems to be rather unsatisfactory since it is difficult to find derivations in axiomatic systems. When the aim is to find derivations and to analyse their structural properties, sequent calculi are to be preferred to axiomatic systems. Recently different kinds of sequent calculi for non-normal logics have been proposed: Gentzen-style calculi [18, 19, 20, 29]; labelled [10, 30] and display [5] calculi based on translations into normal modal logics; labelled calculi based on the internalisation of neighbourhood [24, 26] and bi-neighbourhood [6] semantics; and, finally, linear nested sequents [21].

This paper, which extends the results presented in [29], concentrates on Gentzen-style calculi since they are better suited than labelled calculi, display calculi, and nested sequents to give decision procedures (computationally well-behaved) and constructive proofs of interpolation theorems. We consider cut- and contraction-free G3-style sequent calculi for all the logics in the cube of non-normal modalities and for their extensions with the deontic axioms $D^{\Diamond}:=\Box A\supset\Diamond A$ and $D^{\bot}:=\neg\Box\bot$ . The calculi we present have the subformula property and allow for a straightforward decision procedure by a terminating loop-free proof search. Moreover, with the exception of the calculi for EC(N) and its deontic extensions, they are standard [11] – i.e., each operator is handled by a finite number of rules with a finite number of premisses – and they admit of a Maehara-style constructive proof of Craig’s interpolation theorem.

This work improves on previous ones on Gentzen-style calculi for non-normal logics in that we prove cut admissibility for non-normal modal and deontic logics, and not only for the modal ones [20, 18, 19]. Moreover, we prove height-preserving admissibility of weakening and contraction, whereas neither weakening nor contraction is admissible in [20, 18] and weakening but not contraction is admissible in [19]. The admissibility of contraction is a major improvement since, as it is well known, contraction can be as bad as cut for proof search: we may continue to duplicate some formula forever and, therefore, we need a (computationally expensive) loop-checker to ensure termination. Proof search procedures based on contraction-free calculi terminate because the height of derivations is bounded by a number depending on the complexity of the end-sequent and, therefore, we avoid the need of loop-checkers. To illustrate, the introduction of contraction-free calculi has allowed to give computationally optimal decision procedures for propositional intuitionistic logic ( $\mathbf{IL_{p}}$ ) [16] and for the normal modal logics K and T [1, 17]. The existence of a loop-free terminating decision procedure has also allowed to give a constructive proof of uniform interpolation for $\mathbf{IL_{p}}$ [34] as well as for K and T [2]. The cut- and contraction-free calculi for non-normal logics considered here are such that the height of each derivation is bounded by the weight of its end-sequent and, therefore, we easily obtain a polynomial space upper complexity bound for proof search. This upper bound is optimal for the logics having $C$ as theorem (the satisfiability problem for non-normal modal logics without $C$ is in NP, see [39]).

Moreover, the introduction of well-behaved calculi for non-normal deontic logics is interesting since proof analysis can be applied to the deontic paradoxes [15] that are one of the central topics of deontic reasoning. We illustrate this in Section 0.4.3 by considering Forrester’s Paradox [8] and by showing that proof analysis cast doubts on the widespread opinion [15, 31, 36] that Forrester’s argument provides evidence against rule $RM$ (see Table 1). If Forrester’s argument is formalized as in [15] then it does not compel us to adopt a deontic logic weaker than KD. If, instead, it is formalised as in [36] then it forces the adoption of a logic where $RM$ fails, but the formal derivation differs substantially from Forrester’s informal argument.

It is also given a constructive proof of interpolation for all logics having a standard calculus. To our knowledge in the literature there is no other constructive study of interpolation in non-normal logics. In [7, Chap(s). 3.8 and 6.6] a constructive proof of Craig’s (and Lyndon’s) interpolation theorem is given for the modal logics K and R, and for some of their extensions, including the deontic ones, but the proof makes use of model-theoretic notions. A proof of interpolation by the Maehara-technique for KD is given in [38]. For a thorough study of interpolation in modal logics we refer the reader to [9]. A model-theoretic proof of interpolation for E is given in [14], and a coalgebraic proof of (uniform) interpolation for all the logics considered here, as well as all other rank-1 modal logics (see below), is given in [32]. As it is explained in Example 0.5.5, we have not been able to prove interpolation for calculi containing the non-standard rule $LR$ - $C$ (see Table 6) and, as far as we know, it is still an open problem whether it is possible to give a constructive proof of interpolation for these logics.

Related Work.

The modal rules of inference presented in Table 6 are obtained from the rules presented in [20] by adding weakening contexts to the conclusion of the rules. This minor modification, used also in [19, 32, 33] for several modal rules, allows us to shift from set-based sequents to multiset-based ones and to prove not only that cut is admissible, as it is done in [18, 19, 20], but also that weakening and contraction are height-preserving admissible. Given that implicit contraction is not eliminable from set-based sequents, the decision procedure for non-normal logics given in [20] is based on a model-theoretic inversion technique so that it is possible to define a procedure that outputs a derivation for all valid sequents and a finite countermodel for all invalid ones. One weakness of this decision procedure is that it does not respect the subformula property for logics without rule $RM$ (the procedure adds instances of the excluded middle).

The paper [18] considers multiset-based calculi for the non-normal logic M(N) and for its extensions with axioms $D^{\Diamond},T,4,5$ , and $B$ . Nevertheless, neither weakening nor contraction is eliminable because there are no weakening contexts in the conclusion of the modal rules. In [19] multiset-based sequent calculi for the non-normal logic E(N) and for its extensions with axioms $D^{\Diamond},T$ , 4, 5, and $B$ are given. The rules $LR$ - $E$ and $R$ - $N$ are as in Table 6, but the deontic axiom $D^{\Diamond}$ is expressed by the following rule:

[TABLE]

where the right premiss is present when we are working over $LR$ - $E$ and it has to be omitted when we work over $LR$ - $M$ . In the calculi in [18, 19] weakening and contraction are taken as primitive rules and not as admissible ones as in the present approach. Even if it is easy to show that weakening is eliminable from the calculi in [19], contraction cannot be eliminated because rule D-2 has exactly two principal formulas and, therefore, it is not possible to permute contraction up with respect to instances of rule D-2 (see Theorem 0.3.5). The presence of a non-eliminable rule of contraction makes the elimination of cut more problematic: in most cases we cannot eliminate the cut directly, but we have to consider the rule known as multicut [27, p. 88]. Moreover, cut is not eliminable from the calculus given in [19] for the deontic logic END. The formula $D^{\bot}:=\neg\Box\bot$ is a theorem of this logic, but it can be derived only with a non-eliminable instance of cut as in:

[TABLE]

Finally, it is worth noticing that all the non-normal logics we consider here are rank-1 logics in the sense of [32, 33, 35] – i.e., logics whose modal axioms are propositional combinations of formulas of shape $\Box\phi$ , where $\phi$ is purely propositional – and the calculi we give for the modal logics E, M, K and KD are explicitly considered in [32, 35]. Thus, they are part of the family of modal coalgebraic logics [32, 33, 35] and most of the results in this paper can be seen as instances of general results that hold for rank-1 (coalgebraic) logics. If, in particular, we consider cut-elimination for coalgebraic logics [33] then all our calculi absorb congruence and Theorem 0.3.5 and case 3 of Theorem 0.3.6 show that they absorb contraction and cut. Hence, [33, Thm. 5.7] entails that cut and contraction are admissible in these calculi; moreover, [33, Props. 5.8 and 5.11] entail that they are one-step cut free complete w.r.t. coalgebraic semantics. This latter result gives a semantic proof of cut admissibility in the calculi considered here. Analogously, if we consider decidability, the polynomial space upper bound we find in Section 0.4.1 coincides with that found in [35] for rank-1 modal logics.

Synopsis.

Section 0.2 summarizes the basic notions of axiomatic systems and of neighbourhood semantics for non-normal logics. Section 0.3 presents G3-style sequent calculi for these logics and then shows that weakening and contraction are height-preserving admissible and that cut is (syntactically) admissible. Section 0.4 describes a terminating proof-search decision procedure for all calculi, it shows that each calculus is equivalent to the corresponding axiomatic system, and it applies proof search to Forrester’s paradox. Finally, Section 0.5 gives a Maehara-style constructive proof of Craig’s interpolation theorem for the logics having a standard calculus.

0.2 Non-normal Logics

0.2.1 Axiomatic Systems

We introduce, following [4], the basic notions of non-normal logics. Given a countable set of propositional variables $\{p_{n}\,|\,n\in\mathbb{N}\}$ , the formulas of the modal language $\mathcal{L}$ are generated by:

[TABLE]

We remark that $\bot$ is a 0-ary logical symbol. This will be extremely important in the proof of Craig’s interpolation theorem. As usual $\neg A$ is a shorthand for $A\supset\bot$ , $\top$ for $\bot\supset\bot$ , $A\leftrightarrow B$ for $(A\supset B)\wedge(B\supset A)$ , and $\Diamond A$ for $\neg\Box\neg A$ . We follow the usual conventions for parentheses.

Let L be the logic containing all $\mathcal{L}$ -instances of propositional tautologies as axioms, and modus ponens ( $MP$ ) as inference rule. The minimal non-normal modal logic E is the logic L plus the rule $RE$ of Table 1. We will consider all the logics that are obtained by extending E with some set of axioms from Table 2. We will denote the logics according to the axioms that define them, e.g. EC is the logic E $\,\oplus\,C$ , and EMD⊥ is E $\,\oplus\,M\oplus D^{\bot}$ . By X we denote any of these logics and we write X $\vdash A$ whenever $A$ is a theorem of X. We will call modal the logics containing neither $D^{\bot}$ nor $D^{\Diamond}$ , and deontic those containing at least one of them. We have followed the usual naming conventions for the modal axioms, but we have introduced new conventions for the deontic ones: $D^{\bot}$ is usually called either $CON$ or $P$ and $D^{\Diamond}$ is usually called $D$ , cf. [3, 12, 15].

It is also possible to give an equivalent rule-based axiomatization of some of these logics. In particular, the logic EM, also called M, can be axiomatixed as L plus the rule $RM$ of Table 1. The logic EMC, also called R, can be axiomatized as L plus the rule $RR$ of Table 1. Finally, the logic EMCN, i.e. the smallest normal modal logic K, can be axiomatized as L plus the rule $RK$ of Table 1. These rule-based axiomatizations will be useful later on since they simplify the proof of the equivalence between axiomatic systems and sequent calculi (Theorem 0.4.5).

The following proposition states the well-known relations between the theorems of non-normal modal logics. For a proof the reader is referred to [4].

Proposition 0.2.1.

For any formula $A\in\mathcal{L}$ we have that E $\vdash A$ implies M $\vdash A$ ; M $\vdash A$ implies R $\vdash A$ ; R $\vdash A$ implies K $\vdash A$ . Analogously for the logics containing axiom $N$ and/or axiom $C$ .

Axiom $D^{\bot}$ is K-equivalent to $D^{\Diamond}$ , but the correctness of $D^{\Diamond}$ has been a big issue in the literature on deontic logic. This fact urges the study of logics weaker than KD, where $D^{\bot}$ and $D^{\Diamond}$ are no more equivalent [4]. The deontic formulas $D^{\bot}$ and $D^{\Diamond}$ have the following relations in the logics we are considering.

Proposition 0.2.2.

$D^{\bot}$ and $D^{\Diamond}$ are independent in E; $D^{\bot}$ is derivable from $D^{\Diamond}$ in non-normal logics containing at least one of the axioms $M$ and $N$ ; $D^{\Diamond}$ is derivable from $D^{\bot}$ in non-normal logics containing axiom $C$ .

In Figure 1 the reader finds the lattice of non-normal modal logics, see [4, p. 237], and in Figure 2 the lattice of non-normal deontic logics.

0.2.2 Semantics

The most widely known semantics for non-normal logics is neighbourhood semantics. We sketch its main tenets following [4], where neighbourhood models are called minimal models.

Definition 0.2.3.

A neighbourhood model is a triple $\mathcal{M}:=\langle W,\,N,\,P\rangle$ , where $W$ is a non-empty set of possible worlds; $N:W\longrightarrow 2^{2^{W}}$ is a neighbourhood function that associates to each possible world $w$ a set $N(w)$ of subsets of $W$ ; and $P$ gives a truth value to each propositional variable at each world.

The definition of truth of a formula $A$ at a world $w$ of a neighbourhood model $\mathcal{M}$ – $\models_{w}^{\mathcal{M}}A$ – is the standard one for the classical connectives with the addition of

[TABLE]

where $||A||^{\mathcal{M}}$ is the truth set of $A$ – i.e., $||A||^{\mathcal{M}}=\{w\,|\,\models_{w}^{\mathcal{M}}A\}$ . We say that a formula $A$ is valid in a class $\mathcal{C}$ of neighbourhood models iff it is true in every world of every $\mathcal{M}\in\mathcal{C}$ .

In order to give soundness and completeness results for non-normal modal and deontic logics with respect to (classes of) neighbourhood models, we introduce the following definition.

Definition 0.2.4.

Let $\mathcal{M}=\langle W,\,N,\,P\rangle$ be a neighbourhood model, $X,Y\in 2^{W}$ , and $w\in W$ , we say that:

•

$\mathcal{M}$ is supplemented if $X\cap Y\in N(w)$ imples $X\in N(w)$ and $Y\in N(w)$ ;

•

$\mathcal{M}$ is closed under finite intersection if $X\in N(w)$ and $Y\in N(w)$ imply $X\cap Y\in N(w)$ ;

•

$\mathcal{M}$ contains the unit if $W\in N(w)$ ;

•

$\mathcal{M}$ is non-blind if $X\in N(w)$ implies $X\neq\emptyset$ ;

•

$\mathcal{M}$ is complement-free if $X\in N(w)$ implies $W-X\not\in N(w)$ .

Proposition 0.2.5.

We have the following correspondence results between $\mathcal{L}$ -formulas and the properties of the neighbourhood function defined above:

•

Axiom $M$ corresponds to supplementation;

•

Axiom $C$ corresponds to closure under finite intersection;

•

Axiom $N$ corresponds to containment of the unit;

•

Axiom $D^{\bot}$ corresponds to non-blindness;

•

Axiom $D^{\Diamond}$ corresponds to complement-freeness.

Theorem 0.2.6.

E* is sound and complete with respect to the class of all neighbourhood models. Any logic X which is obtained by extending E with some axioms from Table 2 is sound and complete with respect to the class of all neighbourhood models which satisfies all the properties corresponding to the axioms of X.*

See [4] for the proof of Proposition 0.2.5 and of Theorem 0.2.6.

0.3 Sequent Calculi

We introduce sequent calculi for non-normal logics that extend the multiset-based sequent calculus G3cp [27, 28, 37] for classical propositional logic – see Table 6 – by adding some modal and deontic rules from Table 6. In particular, we consider the modal sequent calculi given in Table 6, which will be shown to capture the modal logics of Figure 1, and their deontic extensions given in Table 6, which will be shown to capture all deontic logics of Figure 2. We adopt the following notational conventions: we use G3X to denote a generic calculus from either Table 6 or Table 6, and we use G3Y(Z) to denote both G3Y and GRYZ. All the rules in Tables 6 and 6 but $LR$ - $C$ and $L$ - $D^{\Diamond_{C}}$ are standard rules in the sense of [11]: each of them is a single rule with a fixed number of premisses; $LR$ - $C$ and $L$ - $D^{\Diamond_{C}}$ , instead, stand for a recursively enumerable set of rules with a variable number of premisses.

For an introduction to G3cp and the relevant notions, the reader is referred to [27, Chapter 3]. We sketch here the main notions that will be used in this paper. A sequent is an expression $\Gamma\Longrightarrow\Delta$ , where $\Gamma$ and $\Delta$ are finite, possibly empty, multisets of formulas. If $\Pi$ is the (possibly empty) multiset $A_{1},\dots,A_{m}$ then $\Box\Pi$ is the (possibly empty) multiset $\Box A_{1},\dots,\Box A_{m}$ . A derivation of a sequent $\Gamma\Longrightarrow\Delta$ in G3X is an upward growing tree of sequents having $\Gamma\Longrightarrow\Delta$ as root, initial sequents or instances of rule $L\bot$ as leaves, and such that each non-initial node is the conclusion of an instance of one rule of G3X whose premisses are its children. In the rules in Tables 6 and 6, the multisets $\Gamma$ and $\Delta$ are called contexts, the other formulas occurring in the conclusion (premiss(es), resp.) are called principal (active). In a sequent the antecedent (succedent) is the multiset occurring to the left (right) of the sequent arrow $\Longrightarrow$ . As for G3cp, a sequent $\Gamma\Longrightarrow\Delta$ has the following denotational interpretation: the conjunction of the formulas in $\Gamma$ implies the disjunction of the formulas in $\Delta$ .

As measures for inductive proofs we use the weight of a formula and the height of a derivation. The weight of a formula $A$ , $w(A)$ , is defined inductively as follows: $w(\bot)=w(p_{i})=0$ ; $w(\Box A)=w(A)+1$ ; $w(A\circ B)=w(A)+w(B)+1$ (where $\circ$ is one of the binary connectives $\wedge,\,\lor,\,\supset$ ). The weight of a sequent is the sum of the weight of the formulas occurring in that sequent. The height of a derivation is the length of its longest branch minus one. A rule of inference is said to be (height-preserving) admissible in G3X if, whenever its premisses are derivable in G3X, then also its conclusion is derivable (with at most the same derivation height) in G3X. The modal depth of a formula (sequent) is the maximal number of nested modal operators occurring in it(s members).

0.3.1 Structural rules of inference

We are now going to prove that the calculi G3X have the same good structural properties of G3cp: weakening and contraction are height-preserving admissible and cut is admissible. All proofs are extension of those for G3cp, see [27, Chapter 3]; in most cases, the modal rules have to be treated differently from the propositional ones because of the presence of empty contexts in the premiss(es) of the modal ones. We adopt the following notational convention: given a derivation tree $\mathcal{D}_{k}$ , the derivation tree of the $n$ -th leftmost premiss of its last step is denoted by $\mathcal{D}_{kn}$ . We begin by showing that the restriction to atomic initial sequents, which is needed to have the propositional rules invertible, is not limitative in that initial sequents with arbitrary principal formula are derivable in G3X.

Proposition 0.3.1.

Every instance of $A,\Gamma\Longrightarrow\Delta,A$ is derivable in G3X.

Proof.

By induction on the weight of $A$ . If $w(A)=0$ – i.e., $A$ is atomic or $\bot$ – then we have an instance of an initial sequent or of a conclusion of $L\bot$ and there is nothing to prove. If $w(A)\geq 1$ , we argue by cases according to the construction of $A$ . In each case we apply, root-first, the appropriate rule(s) in order to obtain sequents where some proper subformula of $A$ occurs both in the antecedent and in the succedent. The claim then holds by the inductive hypothesis (IH). To illustrate, if $A\equiv\Box B$ and we are in G3M(ND), we have:

[TABLE]

∎

Theorem 0.3.2.

The left and right rules of weakening are height-preserving admissible in G3X

[TABLE]

Proof.

The proof is a straightforward induction on the height of the derivation $\mathcal{D}$ of $\Gamma\Longrightarrow\Delta$ . If the last step of $\mathcal{D}$ is by a propositional rule, we have to apply the same rule to the weakened premiss(es), which are derivable by IH, see [27, Thm. 2.3.4]. If it is by a modal or deontic rule, we proceed by adding $A$ to the appropriate weakening context of the conclusion of that rule instance. To illustrate, if the last rule is $LR$ - $E$ , we transform

[TABLE]

∎

Before considering contraction, we recall some facts that will be useful later on.

Lemma 0.3.3.

*In G3X the rules $\neg A,\Gamma\Longrightarrow\Delta\Gamma\Longrightarrow\Delta,A$ and $\Gamma\Longrightarrow\Delta,\neg AA,\Gamma\Longrightarrow\Delta$ are admissible. *

Proof.

We have the following derivations (the step by $RW$ is admissible thanks to Theorem 0.3.2):

[TABLE]

∎

Lemma 0.3.4.

All propositional rules are height-preserving invertible in G3X, that is the derivability of (a possible instance of) a conclusion of a propositional rule entails the derivability, with at most the same derivation height, of its premiss(es).

Proof.

We have only to extend the proof for G3cp, see [27, Thm. 3.1.1], with new cases for the modal and deontic rules. If $A\circ B$ occurs in the antecedent (succedent) of the conclusion of an instance of a modal or deontic rule then it must be a member of the weakening context $\Gamma$ ( $\Delta$ ) of this rule instance, and we have only to change the weakening context according to the rule we are inverting.∎

Theorem 0.3.5.

The left and right rules of contraction are height-preserving admissible in G3X

[TABLE]

Proof.

The proof is by simultaneous induction on the height of the derivation $\mathcal{D}$ of the premiss for left and right contraction. The base case is straightforward. For the inductive steps, we have different strategies according to whether the last step in $\mathcal{D}$ is by a propositional rule or not. If the last step in $\mathcal{D}$ is by a propositional rule, we have two subcases: if the contraction formula is not principal in that step, we apply the inductive hypothesis and then the rule. Else we start by using the height-preserving invertibility – Lemma 0.3.4 – of that rule, and then we apply the inductive hypothesis and the rule, see [27, Thm. 3.2.2] for details.

If the last step in $\mathcal{D}$ is by a modal or deontic rule, we have two subcases: either (the last step is by one of $LR$ - $C$ , $LR$ - $R$ , $LR$ - $K$ , $L$ - $D^{\Diamond_{E}}$ , $L$ - $D^{\Diamond_{M}}$ , $L$ - $D^{\Diamond_{C}}$ and $L$ - $D^{*}$ and) both occurrences of the contraction formula $A$ of $LC$ are principal in the last step or some instance of the contraction formula is introduced in the appropriate weakening context of the conclusion. In the first subcase, we apply the inductive hypothesis to the premiss and then the rule. An interesting example is when the last step in $\mathcal{D}$ is by $L$ - $D^{\Diamond_{E}}$ . We transform

[TABLE]

where $IH(\mathcal{D}_{1})$ is obtained by applying the inductive hypothesis for the left rule of contraction to $\mathcal{D}_{1}$ and $IH(\mathcal{D}_{2})$ is obtained by applying the inductive hypothesis for the right rule of contraction to $\mathcal{D}_{2}$ .

In the second subcase, we apply an instance of the same modal or deontic rule which introduces one less occurrence of $A$ in the appropriate context of the conclusion. Let’s consider $RC$ . If the last step is by $LR$ - $M$ and no instance of $A$ is principal in the last rule, we transform

[TABLE]

∎

Theorem 0.3.6.

The rule of cut is admissible in G3X

[TABLE]

Proof.

We consider an uppermost application of $Cut$ and we show that either it is eliminable, or it can be permuted upward in the derivation until we reach sequents where it is eliminable. The proofs, one for each calculus, are by induction on the weight of the cut formula $D$ with a sub-induction on the sum of the heights of the derivations of the two premisses (cut-height for shortness). The proof can be organized in 3 exhaustive cases:

At least one of the premisses of cut is an initial sequent or a conclusion of $L\bot$ ; 2. 2.

The cut formula in not principal in the last step of at least one of the two premisses; 3. 3.

The cut formula is principal in both premisses.

**• Case (1). ** Same as for G3cp, see [27, Thm. 3.2.3] for the details.

**• Case (2). ** We have many subcases according to the last rule applied in the derivation ( $\mathcal{D}^{\star}$ ) of the premiss where the cut formula is not principal. For the propositional rules, we refer the reader to [27, Thm. 3.2.3], where it is given a procedure that allows to reduce the cut-height. If the last rule applied in $\mathcal{D}^{\star}$ is a modal or deontic one, we can transform the derivation into a cut-free one because the conclusion of Cut is derivable by replacing the last step of $\mathcal{D}^{\star}$ with the appropriate instance of the same modal or deontic rule. We present explicitly only the cases where the last step of the left premiss is by $LR$ - $E$ and $L$ - $D^{\bot}$ and the cut formula is not principal in it, all other transformations being similar.

$\mathbf{LR\textrm{-}E}:\quad$ If the left premiss is by rule $LR$ - $E$ (and $\Gamma\equiv\Box A,\Gamma^{\prime}$ and $\Delta\equiv\Delta^{\prime},\Box B$ ), we transform

[TABLE]

$\mathbf{L}$ - $\mathbf{D^{\bot}}:\quad$ If the left premiss is by rule $L$ - $D^{\bot}$ , we transform

[TABLE]

**• Case (3). ** If the cut formula $D$ is principal in both premisses, we have cases according to the principal operator of $D$ . In each case we have a procedure that allows to reduce the weight of the cut formula, possibly increasing the cut-height. For the propositional cases, which are the same for all the logics considered here, see [27, Thm. 3.2.3].

If $D\equiv\Box C$ , we consider the different logics one by one, without repeating the common cases.

• **G3E(ND). ** Both premisses are by rule $LR$ - $E$ , we have

[TABLE]

and we transform it into the following derivation that has two cuts with cut formulas of lesser weight, which are admissible by IH.

[TABLE]

• **G3EN(D). ** Left premiss by $R$ - $N$ and right one by $LR$ - $E$ . We transform

[TABLE]

• **G3E(N)D⊥. ** Left premiss is by $LR$ - $E$ , and right one by $L$ - $D^{\bot}$ . We transform

[TABLE]

• **G3E(N)D◇. ** Left premiss is by $LR$ - $E$ , and right one by $L$ - $D^{\Diamond_{E}}$ . We transform ( $|\Xi|\leq 1$ )

[TABLE]

• **G3E(N)D. ** Left premiss by $LR$ - $E$ and right one by $L$ - $D^{\bot}$ or $L$ - $D^{\Diamond_{E}}$ . Same as above.

• **G3END⊥. ** Left premiss by $R$ - $N$ and right one by $L$ - $D^{\bot}$ . We transform

[TABLE]

• **G3END. ** Left premiss by $R$ - $N$ and right one by $L$ - $D^{\Diamond_{E}}$ . We transform ( $|\Xi|\leq 1$ )

[TABLE]

where $(\star)$ is an instance of $L$ - $D^{\bot}$ if $|\Xi|=1$ , else ( $|\Xi|=0$ and) it is some instances of $LW$ and $RW$ .

• **G3M(ND). ** Both premisses are by rule $LR$ - $M$ , we transform

[TABLE]

• **G3MN(D). ** Left premiss by $R$ - $N$ and right one by $LR$ - $M$ . Similar to the case with left premiss by $R$ - $N$ and right one by $LR$ - $E$ .

• G3M(N)D⊥ and **G3M(N)D. ** Left premiss is by $LR$ - $M$ , and right one by $L$ - $D^{\bot}$ or $L$ - $D^{\Diamond_{M}}$ . Similar to the case with left premiss by $LR$ - $E$ and right by $L$ - $D^{\bot}$ or $L$ - $D^{\Diamond_{E}}$ , respectively.

• G3MND⊥ and **G3MND. ** The cases with left premiss by $R$ - $N$ and right one by a deontic rule are like the analogous ones we have already considered.

• G3C(ND). Both premisses are by rule $LR$ - $C$ . Let us agree to use $\Lambda$ to denote the non-empty multiset $A_{1},\dots,A_{n}$ , and $\Xi$ for the (possibly empty) multiset $B_{2},\dots B_{m}$ . The derivation

[TABLE]

is transformed into the following derivation having $n+1$ cuts on formulas of lesser weight

$\Box\Lambda,\Gamma^{\prime},\Box\Xi,\Pi^{\prime}\Longrightarrow\Delta,\Sigma^{\prime},\Box E\lx@proof@logical@and\Lambda,\Xi\Longrightarrow E\lx@proof@logical@and\Lambda\Longrightarrow C\vdots\>\mathcal{D}_{11}C,\Xi\Longrightarrow E\vdots\;\mathcal{D}_{21}E\Longrightarrow A_{1}\lx@proof@logical@and E\Longrightarrow C\vdots\>\mathcal{D}_{C}C\Longrightarrow A_{1}\vdots\;\mathcal{D}_{A_{n}}E\Longrightarrow A_{n}\lx@proof@logical@and E\Longrightarrow C\vdots\>\mathcal{D}_{C}C\Longrightarrow A_{n}\vdots\;\mathcal{D}_{A_{n}}E\Longrightarrow B_{1}\vdots\;\mathcal{D}_{B_{1}}{}^{\dots}E\Longrightarrow B_{m}\vdots\;\mathcal{D}_{B_{m}}$

• G3CN(D). Left premiss by $R$ - $N$ and right premiss by $LR$ - $C$ . We have

[TABLE]

where $A_{1},\dots,A_{n}$ (and thus also $\Box A_{1},\dots,\Box A_{n}$ ) may or may not be the empty multiset. If $A_{1},\dots,A_{n}$ is not empty, we transform it into the following derivation having one cut with cut formula of lesser weigh

[TABLE]

If, instead, $A_{1},\dots,A_{n}$ is empty, we transform it into

[TABLE]

• G3CD◇.** Left premiss by $LR$ - $C$ and right premiss by $L$ - $D^{\Diamond_{C}}$ . We transform (we assume $\Xi=A_{1},\dots A_{k}$ , $\Theta=C,B_{2},\dots,B_{m}$ and $\Lambda=D_{1},\dots,D_{n}$ )

[TABLE]

into the following derivation having $1+(k\times n)$ cuts on formulas of lesser weight

[TABLE]

• **G3C(N)D. ** Left premiss by $LR$ - $C$ and right one by $L$ - $D^{*}$ . It is straightforward to transform the derivation into another one having one cut with cut formula of lesser weight.

• **G3R(D). ** Both premisses are by rule $LR$ - $R$ , we transform

[TABLE]

• **G3RD⋆. **Left premiss is by $LR$ - $R$ , and right one by $L$ - $D^{\star}$ , we transform

[TABLE]

• **G3K(D). ** The new cases with respect to G3R(D) are those with left premiss by an instance of $LR$ - $K$ that has no principal formula in the antecedent. These cases can be treated like cases with left premiss by $R$ - $N$ .∎

0.4 Decidability and syntactic completeness

0.4.1 Decision procedure for G3X

Each calculus G3X has the strong subformula property since all active formulas of each rule in Tables 6 and 6 are proper subformulas of the the principal formulas and no formula disappears in moving from premiss(es) to conclusion. As usual, this gives us a syntactic proof of consistency.

Proposition 0.4.1.

Each premiss of each rule of G3X has smaller weight than its conclusion; 2. 2.

Each premiss of each modal or deontic rule of G3X has smaller modal depth than its conclusion; 3. 3.

The calculus G3X has the subformula property: a G3X-derivation of a sequent $\mathcal{S}$ contains only sequents composed of subformulas of $\mathcal{S}$ ; 4. 4.

The empty sequent is not G3X-derivable.

We also have an effective method to decide the derivability of a sequent in G3X: we start from the desired sequent $\Gamma\Longrightarrow\Delta$ and we construct all possible G3X-derivation trees until either we find a tree where each leaf is an initial sequent or a conclusion of $L\bot$ – we have found a G3X-derivation of $\Gamma\Longrightarrow\Delta$ – or we have checked all possible G3X-derivations and we have found none – $\Gamma\Longrightarrow\Delta$ is not G3X-derivable.

More in details, we present a depth-first procedure that tests G3X-derivability in polynomial space. As it is usual in decision procedures involving non-invertible rules, we have trees involving two kinds of branching. Application of a rule with more than one premiss produce an AND-branching point, where all branches have to be derivable to obtain a derivation. Application of a non-invertible rule to a sequent that can be the conclusion of different instances of non-invertible rules produces an OR-branching point, where only one branch need be derivable to obtain a derivation. In the procedure below we will assume that, given a calculus G3X and given a sequent $\Box\Pi,\Gamma^{p}\Longrightarrow\Delta^{p},\Box\Sigma$ (where $\Gamma^{p}$ and $\Delta^{p}$ are multisets of propositional variables), there is some fixed way of ordering the finite (see below) set of instances of modal and deontic rules of G3X (X-instances, for shortness) having that sequent as conclusion. Moreover, we will represent the root of branches above an OR-branching point by nodes of shape $\Box_{i}$ , where $\Box_{i}$ is the name of the $i$ -th X-instance applied (in the order of all X-instances having that conclusion). To illustrate, if we are in G3EN and we have to consider $\Box A,\Box B,\Gamma^{p}\Longrightarrow\Delta^{p},\Box C$ then we obtain (fixing one way of ordering the three X-instances having that sequent as conclusion):

[TABLE]

where the lowermost sequent is an OR-branching point and the two nodes $LR$ - $E_{1}$ and $LR$ - $E_{2}$ are AND-branching points. Finally, Given an AND(OR)-branching point

[TABLE]

we say that the branch above $\mathcal{S}_{i}$ is an unexplored AND(OR)-branch if no one of its nodes has already been active.

Definition 0.4.2 (G3X-decision procedure).

Stage 1.

We write the one node tree $\Gamma\Longrightarrow\Delta$ and we label $\Gamma\Longrightarrow\Delta$ as active.

Stage n+1.

Let $\mathcal{T}_{n}$ be the tree constructed at stage $n$ , let $\mathcal{S}\equiv\Pi\Longrightarrow\Sigma$ be its active sequent, and let $\mathcal{B}$ be the branch going from the root of $\mathcal{T}_{n}$ to $\mathcal{S}$ .

Closed.

If $\mathcal{S}$ is such that $p\in\Pi\cap\Sigma$ (for some propositional variable $p$ ) or $\bot\in\Pi$ , then we label $\mathcal{S}$ as closed and

Derivable.

If $\mathcal{B}$ contains no unexplored AND-branch, the procedure ends and $\Gamma\Longrightarrow\Delta$ is G3X-derivable;

AND-backtrack.

If, instead, $\mathcal{B}$ contains unexplored AND-branches, we choose the topmost one and we label as active its leftmost unexplored leaf. Else

Propositional.

if $\mathcal{S}$ can be the conclusion of some instances $\circ_{1},\dots,\circ_{m}$ of the invertible propositional rules, we extend $\mathcal{B}$ by applying one of such instances:

[TABLE]

where, if $\mathcal{S}_{2}$ , if present, $\mathcal{S}$ is an AND-branching point. Else

Modal.

If $\mathcal{S}$ can be the conclusion of the following canonically ordered list of X-instances:

[TABLE]

then we extend $\mathcal{B}$ as follows:

[TABLE]

where, if $m\geq 2$ , $\mathcal{S}$ is OR-branching and, if $\Box_{i}$ is a rule with more than one premiss, $\Box_{i}$ is AND-branching. Moreover, we label $\mathcal{S}_{1}^{1}$ as active. Else

Open.

No rule of G3x can be applied to $\mathcal{S}$ , then we label $\mathcal{S}$ as open and

Underivable.

If $\mathcal{B}$ contains no unexplored OR-branch, the procedure ends and $\Gamma\Longrightarrow\Delta$ is not G3X-derivable;

OR-backtrack.

If, instead, $\mathcal{B}$ contains unexplored OR-branches, we choose the topmost one and we label as active its leftmost unexplored leaf.

Termination can be shown as follows. Proposition 0.4.1.1 entails that the height of each branch of the tree $\mathcal{T}$ constructed in a G3X-decision procedure for a sequent $\Gamma\Longrightarrow\Delta$ is bounded by the weight of $\Gamma\Longrightarrow\Delta$ (in particular, given Proposition 0.4.1.2, the number of OR-branching points occurring in a branch is bounded by the modal depth of $\Gamma\Longrightarrow\Delta$ ). Moreover, $\mathcal{T}$ is finitary branching since all rules of G3X are finitary branching rules, and since each sequent can be the conclusion of a finite number $k$ of X-instances (for each G3X $k$ is bounded by a function of $|\Gamma|$ and $|\Delta|$ ). Hence, after a finite number of stages we are either in case Derivable or in case Underivable and, in both cases, the procedure ends. In the first case we can easily extract a G3X-derivation of $\Gamma\Longrightarrow\Delta$ from $\mathcal{T}$ (we just have to delete all unexplored branches as well as all underivable sub-trees above an OR-branching point). In the latter case, thanks to Proposition 0.4.1.3, we know that (modulo the order of the invertible propositional rules) we have explored the whole search space for a G3X-derivation of $\Gamma\Longrightarrow\Delta$ and we have found none.

We prove that it is possible to test G3X-derivability in polynomial space by showing how it is possible to store only the active node together with a stack containing information sufficient to reconstruct unexplored branches. For the propositional part of the calculi, we proceed as in [1, 16, 17]: each entry of the stack is a triple containing the name of the rule applied, an index recording which of its premisses is active, and its principal formula. For the X-instances two complications arise: we need to record which OR-branches are unexplored yet, and we have to keep track of the weakening contexts of the conclusion in the premisses of X-instances. The first problem has already been solved by having assumed that the X-instances applicable to a given sequent have a fixed canonical order. The second problem is solved by adding a numerical superscript to the formulas occurring in a sequent and by imposing that:

All formulas in the end-sequent have 1 as superscript;
The superscript $k$ of the principal formulas of rules and of initial sequents are maximal in that sequent;
Active formulas of X-instances (propositional rules) have $k+2$ ( $k$ , respectively) as superscript;

Contexts are copied in the premisses of each rule.

By doing so, the contexts of the conclusion are copied in the premisses in each rule of G3X, but they cannot be principal in the trees above the premisses of the X-instances because their superscript is never maximal therein. It is immediate to see the the superscripts occurring in a derivation are bounded by (twice) the modal depth of the end-sequent.

Instances of all modal and deontic rules in Table 6 but $LR$ - $C$ and $L$ - $D^{\Diamond_{C}}$ are such that there is no need to record their principal formulas in the stack entry: they are the boxed version of the formulas having maximal superscript in the active premiss; moreover, the name of the rule and the number of the premiss allow to reconstruct the position of the principal formulas (for the right premiss of $LR$ - $E$ and $L$ - $D^{\Diamond_{E}}$ , we have to switch the two formulas). In instances of rules $LR$ - $C$ and $L$ - $D^{\Diamond_{C}}$ , instead, this doesn’t hold since in all premisses but the leftmost one there is no subformula of some principal formulas. We can overcome this problem by copying in each premiss all principal formulas having no active subformula in that premiss and by adding one to their superscript. We also keep fixed the position of all formulas (modulo the swapping of the two active formulas). To illustrate, one such instance is:

[TABLE]

In this way, given the name of the modal or deontic rule applied, any premiss of this rule instance, and its position among the premisses of this rule, we can reconstruct both the conclusion of this rule instance and its position in the fixed order of X-instances concluding that sequent (thus we know which OR-branches are unexplored yet). In doing so, we use the hp-admissibility of contraction to ensure that no formula has more than one occurrence in the antecedent or in the succedent of the conclusion of X-instances (otherwise we might be unable to reconstruct which of two identical X-instances we are considering). Hence, for X-instances each stack entry records the name of the rule applied and an index recording which premiss we are considering.

The decision procedure is like in Definition 0.4.2. The only novelty is that at each stage, instead of storing the full tree constructed so far, we store only the active node and the stack, we push an entry in the stack and, if we are in a backtracking case, we pop stack entries (and we use them to reconstruct the corresponding active sequent) until we reach an entry recording unexplored branches of the appropriate kind, if any occurs.

Theorem 0.4.3.

G3X*-derivability is decidable in $\mathcal{O}(n\,\log{}n)$ -space, where $n$ is the weight of the end-sequent.*

Proof.

We have already argued that proof search terminates. As in [1, 16, 17], Proposition 0.4.1.1 entails that the stack depth is bounded by $\mathcal{O}(n)$ and, by storing the principal formulas of propositional rules as indexes into the end-sequent, each entry requires $\mathcal{O}(\log{}n)$ space. Hence we have an $\mathcal{O}(n\,\log{}n)$ space bound for the stack. Moreover, the active sequent contains at most $\mathcal{O}(n)$ subformulas of the end-sequent and their numerical superscripts. Each such subformula requires $\mathcal{O}(\log{}n)$ space since it can be recorded as an index into the end-sequent; its numerical superscript requires $\mathcal{O}(\log{}n)$ too since there are at most $\mathcal{O}(n)$ superscripts. Hence also the active sequent requires $\mathcal{O}(n\log{}n)$ space.∎

0.4.2 Equivalence with the axiomatic systems

It is now time to show that the sequent calculi introduced are equivalent to the non-normal logics of Section 0.2. We write G3X $\vdash\Gamma\Longrightarrow\Delta$ if the sequent $\Gamma\Longrightarrow\Delta$ is derivable in G3X, and we say that $A$ is derivable in G3X whenever G3X $\vdash\;\Longrightarrow A$ . We begin by proving the following

Lemma 0.4.4.

All the axioms of the axiomatic system X are derivable in G3X.

Proof.

A straightforward application of the rules of the appropriate sequent calculus, possibly using Proposition 0.3.1. As an example, we show that the deontic axiom $D^{\bot}$ is derivable by means of rule $L$ - $D^{\bot}$ and that axiom $C$ is derivable by means of $LR$ - $C$ .

[TABLE]

∎

Next we prove the equivalence of the sequent calculi for non-normal logics with the corresponding axiomatic systems in the sense that a sequent $\Gamma\Longrightarrow\Delta$ is derivable in G3X if and only if its characteristic formula $\bigwedge\Gamma\supset\bigvee\Delta$ is derivable in X (where the empty antecedent stands for $\top$ and the empty succedent for $\bot$ ). As a consequence each calculus is sound and complete with respect to the appropriate class of neighbourhood models (see Section 0.2.2).

Theorem 0.4.5.

Derivability in the sequent system G3X and in the axiomatic system X are equivalent, i.e.

G3X* * $\vdash\;\Gamma\Longrightarrow\Delta\qquad$ iff X $\vdash\bigwedge\Gamma\supset\bigvee\Delta$

Proof.

To prove the right-to-left implication, we argue by induction on the height of the axiomatic derivation in X. The base case is covered by Lemma 0.4.4. For the inductive steps, the case of $MP$ follows by the admissibility of Cut and the invertibility of rule $R\supset$ . If the last step is by $RE$ , then $\Gamma=\emptyset$ and $\Delta$ is $\Box C\leftrightarrow\Box D$ . We know that (in X) we have derived $\Box C\leftrightarrow\Box D$ from $C\leftrightarrow D$ . Remember that $C\leftrightarrow D$ is defined as $(C\supset D)\wedge(D\supset C)$ . Thus we assume, by inductive hypothesis (IH) , that G3ED $\vdash\;\Longrightarrow C\supset D\wedge D\supset C$ . From this, by invertibility of $R\wedge$ and $R\supset$ (Lemma 0.3.4), we obtain that G3ED $\vdash\;C\Longrightarrow D$ and G3ED $\vdash\;D\Longrightarrow C$ . We can thus proceed as follows

[TABLE]

For the converse implication, we assume G3X $\vdash\Gamma\Longrightarrow\Delta$ , and show, by induction on the height of the derivation in sequent calculus, that X $\vdash\bigwedge\Gamma\supset\bigvee\Delta$ . If the derivation has height 0, we have an initial sequent – so $\Gamma\cap\Delta\neq\emptyset$ – or an instance on $L\bot$ – thus $\bot\in\Gamma$ . In both cases the claim holds. If the height is $n+1$ , we consider the last rule applied in the derivation. If it is a propositional one, the proof is straightforward. If it is a modal rule, we argue by cases.

If the last step of a derivation in G3E(ND) is by $LR$ - $E$ , we have derived $\Box C,\Gamma^{\prime}\Longrightarrow\Delta^{\prime},\Box D$ from $C\Longrightarrow D$ and $D\Longrightarrow C$ . By IH and propositional reasoning, ED $\vdash C\leftrightarrow D$ , thus ED $\vdash\Box C\supset\Box D$ . By some propositional steps we conclude ED $\vdash(\Box C\wedge\bigwedge\Gamma^{\prime})\supset(\bigvee\Delta^{\prime}\lor\Box D).$ The cases of $LR$ - $M$ , $LR$ - $R$ , and $LR$ - $K$ can be treated in a similar manner (thanks, respectively, to the rule $RM$ , $RR$ , and $RK$ from Table 1).

If we are in G3C(ND), suppose the last step is the following instance of $LR$ - $C$ :

[TABLE]

By IH, we have that C(ND) $\vdash D\supset C_{i}$ for all $i\leq k$ , and, by propositional reasoning, we have that C(ND) $\vdash D\supset C_{1}\wedge\dots\wedge C_{k}$ . We also know, by IH, that C(ND) $\vdash C_{1}\wedge\dots\wedge C_{k}\supset D$ . By applying $RE$ to these two theorems we get that

[TABLE]

By using axiom $C$ and propositional reasoning, we know that

[TABLE]

By applying transitivity to (2) and (1) and some propositional steps, we conclude that

[TABLE]

Let’s now consider rule $L$ - $D^{\bot}$ . Suppose we are in G3XD⊥ and we have derived $\Box C,\Gamma^{\prime}\Longrightarrow\Delta$ from $C\Longrightarrow$ . By IH, XD⊥ $\vdash C\supset\bot$ , and we know that xD⊥ $\vdash\bot\supset C$ . Thus by $RE$ (or $RM$ ), we get XD⊥ $\vdash\Box C\supset\Box\bot$ . By contraposing it and then applying a $MP$ with the axiom $D^{\bot}$ , we get that XD⊥ $\vdash\neg\Box C$ . By some easy propositional steps we conclude XD⊥ $\vdash(\Box C\wedge\bigwedge\Gamma^{\prime})\supset\bigvee\Delta$ . The case $R$ - $N$ is similar.

Let’s consider rules $L$ - $D^{\Diamond_{E}}$ . Suppose we are in G3ED◇ and we have derived $\Box A,\Box B,\Gamma^{\prime}\Longrightarrow\Delta$ from the premisses $A,B\Longrightarrow$ and $\Longrightarrow A,B$ . By induction we get that ED◇ $\vdash A\wedge B\supset\bot$ and ED◇ $\vdash A\lor B$ . Hence, ED◇ $\vdash B\supset\neg A$ and ED◇ $\vdash\neg A\supset B$ . By applying $RE$ we get that

[TABLE]

which, thanks to axiom $D^{\Diamond}$ , entails that

[TABLE]

By some propositional steps we conclude

[TABLE]

Notice that, thanks to Proposition 0.4.1.4 and Theorem 0.3.6, we can assume that instances of rule $L$ - $D^{\Diamond}$ always have two principal formulas. Otherwise the calculus would prove the empty sequent (we will also assume that neither $\Pi$ nor $\Sigma$ is empty in instances of rule $L$ - $D^{\Diamond_{C}}$ ).

The case of $L$ - $D^{\Diamond_{M}}$ is analogous to that of $L$ - $D^{\bot}$ for instances with one principal formula and to that of $L$ - $D^{\Diamond_{E}}$ for instances with two principal formulas.

Let’s consider rule $L$ - $D^{\Diamond_{C}}$ . Suppose we have a G3CD◇-derivation whose last step is:

[TABLE]

By induction and by some easy propositional steps we know that ECD◇ $\vdash\bigwedge\Pi\leftrightarrow\neg\bigwedge\Sigma$ . By rule $RE$ we derive ECD◇ $\vdash\Box\bigwedge\Pi\supset\Box\neg\bigwedge\Sigma$ , which, thanks to axiom $D^{\Diamond}$ , entails that ECD◇ $\vdash\Box\bigwedge\Pi\supset\neg\Box\bigwedge\Sigma$ . By transitivity with two (generalized) instances of axiom $C$ we obtain ECD◇ $\vdash\bigwedge\Box\Pi\supset\neg\bigwedge\Box\Sigma$ . By some easy propositional steps we conclude that ECD◇ $\vdash(\bigwedge\Box\Pi\wedge\bigwedge\Box\Sigma\wedge\bigwedge\Gamma^{\prime})\supset\bigvee\Delta$ .

The admissibility of $L$ - $D^{*}$ in EC(N)D, RD, and KD is similar to that of $LR$ - $C$ : in (1) we replace $\Box D$ with $\Box\bot$ and then we use theorem $D^{\bot}$ to transform it into $\bot$ . ∎

By combining this and Theorem 0.2.6 we have the following result.

Corollary 0.4.6.

The calculus G3X is sound and complete with respect to the class of all neighbourhood models for X.

0.4.3 Forrester’s Paradox

As an application of our decision procedure, we use it to analyse two formal reconstructions of Forrester’s paradox [8], which is one of the many paradoxes that endanger the normal deontic logic KD [15]. Forrester’s informal argument goes as follows:

Consider the following three statements:

Jones murders Smith. 2. 2.

Jones ought not murder Smith. 3. 3.

If Jones murders Smith, then Jones ought to murder Smith gently.

Intuitively, these sentences appear to be consistent. However 1 and 3 together imply that

Jones ought to murder Smith gently.

Also we accept the following conditional:

If Jones murders Smith gently, then Jones murder Smith.

Of course, this is not a logical validity but, rather, a fact about the world we live in. Now, if we assume that the monotonicity rule is valid, then statement 5 entails

If Jones ought to murder Smith gently, then Jones ought to murder Smith.

And so, statements 4 and 6 together imply

Jones ought to murder Smith.

But [given the validity of $D^{\Diamond}$ ] this contradicts statement 2. The above argument suggests that classical deontic logic should not validate the monotonicity rule [ $RM$ ] [31, p. 16]

We show that Forrester’s paradox is not a valid argument in deontic logics by presenting, in Figure 5, a failed G3KD-proof search of the sequent that expresses it:

[TABLE]

where $m$ stands for ’John murders Smith’ and $g$ for ‘John murders Smith gently’ [15, pp. 87–91]. Note that, by Theorem 0.4.5, if Forrester’s paradox is not G3KD-derivable, then it is not valid in all the weaker deontic logics we have considered.

To make our failed proof search into a derivation of Forrester’s paradox, we would have to add (to G3MD◇ or stronger calculi) a non-logical axiom $\Longrightarrow g\supset m$ , and to have cut as a primitive – and ineliminable – rule of inference. An Hilbert-style axiomatization of Forrester’s argument – e.g., [15, p. 88] – hides this cut with a non-logical axiom in the step where $\Box g\supset\Box m$ is derived from $g\supset m$ , by one of $RM$ , $RR$ or $RK$ . This step – i.e., the step from 5 to 6 in the informal argument above – is not acceptable because none of these rules allows to infer its conclusion when the premiss is an assumption and not a theorem. We have here an instance of the same problem that has led many authors to conclude that the deduction theorem fails in modal logics, conclusion that has been shown to be wrong in [25].

An alternative formulation of Forrester’s argument is given in [36], where the sentence ‘John murders Smith gently’ is expressed by the complex formula $g\wedge m$ instead of by the atomic $g$ . In this case Forrester’s argument becomes valid whenever the monotonicity rule is valid as it shown in Figure 4. Nevertheless, whereas it was an essential ingredient of the informal version, under this formalization premiss 5 becomes dispensable. Hence it is disputable that this is an acceptable way of formalising Forrester’s argument.

This is not the place to discuss at length the correctness of formal representation of Forrester’s argument and their implications for deontic logics. We just wanted to illustrate how the calculi G3XD can be used to analyse formal representations of the deontic paradoxes. If Forrester’s argument is formalised as in [15] then it does not force to adopt a deontic logic weaker than KD. If, instead, it is formalised as in [36] then it forces the adoption of a logic where $RM$ fails, but the formal derivation differs substantially from Forrester’s informal argument [8].

0.5 Craig’s Interpolation Theorem

In this section we use Maehara’s [22, 23] technique to prove Craig’s interpolation theorem for each modal or deontic logic X which has $C$ as theorem only if it has also $M$ (Example 0.5.5 illustrates the problem with the non-standard rule $LR$ - $C$ ).

Theorem 0.5.1 (Craig’s interpolation theorem).

Let $A\supset B$ be a theorem of a logic X that differs from EC(N) and its deontic extensions EC(N)D and ECD◇, then there is a formula $I$ , which contains propositional variables common to $A$ and $B$ only, such that both $A\supset I$ and $I\supset B$ are theorems of X.

In order to prove this theorem, we use the following notions.

Definition 0.5.2.

A partition of a sequent $\Gamma\Longrightarrow\Delta$ is any pair of sequents

$\langle\Gamma_{1}\Longrightarrow\Delta_{1}\;||\;\Gamma_{2}\Longrightarrow\Delta_{2}\rangle$ such that $\Gamma_{1},\Gamma_{2}=\Gamma$ and $\Delta_{1},\Delta_{2}=\Delta$ .

A G3X-interpolant of a partition $\langle\Gamma_{1}\Longrightarrow\Delta_{1}\;||\;\Gamma_{2}\Longrightarrow\Delta_{2}\rangle$ is any formula $I$ such that:

All propositional variables in $I$ are in $(\Gamma_{1}\cup\Delta_{1})\cap(\Gamma_{2}\cup\Delta_{2})$ ; 2. 2.

G3X $\vdash\Gamma_{1}\Longrightarrow\Delta_{1},I$ and G3X $\vdash I,\Gamma_{2}\Longrightarrow\Delta_{2}$ .

If $I$ is a G3X-interpolant of the partition $\langle\Gamma_{1}\Longrightarrow\Delta_{1}\;||\;\Gamma_{2}\Longrightarrow\Delta_{2}\rangle$ , we write

[TABLE]

where one or more of the multisets $\Gamma_{1},\Gamma_{2},\Delta_{1},\Delta_{2}$ may be empty. When the set of propositional variables in $(\Gamma_{1}\cup\Delta_{1})\cap(\Gamma_{2}\cup\Delta_{2})$ is empty, the X-interpolant has to be constructed from $\bot$ (and $\top$ ). The proof of Theorem 0.5.1 is by the following lemma, originally due to Maehara [22, 23] for (an extension of) classical logic.

Lemma 0.5.3 (Maehara’s lemma).

If G3X $\vdash\Gamma\Longrightarrow\Delta$ and $LR$ - $C$ (and $L$ - $D^{\Diamond_{C}}$ ) is not a rule of G3X (see Tables 6 and 6), every partition of $\Gamma\Longrightarrow\Delta$ has a G3X-interpolant.

Proof.

The proof is by induction on the height of the derivation $\mathcal{D}$ of $\Gamma\Longrightarrow\Delta$ . We have to show that each partition of an initial sequent (or of a conclusion of a 0-premiss rule) has a G3X-interpolant and that for each rule of G3X (but $LR$ - $C$ and $L$ - $D^{\Diamond_{C}}$ ) we have an effective procedure that outputs a G3X-interpolant for any partition of its conclusion from the interpolant(s) of suitable partition(s) of its premiss(es). The proof is modular and, hence, we can consider the modal rules without having to reconsider them in the different calculi.

For the base case of initial sequents with $p$ principal formula, we have four possible partitions, whose interpolants are:

[TABLE]

and for the base case of rule $L\bot$ , we have:

[TABLE]

For the proof of (some of) the propositional cases the reader is referred to [37, pp. 117-118]. Thus, we have only to prove that all the modal and deontic rules of Table 6 (modulo $LR$ - $C$ and $L$ - $D^{\Diamond_{C}}$ ) behave as desired.

• LR-E $)\quad$ If the last rule applied in $\mathcal{D}$ is

tensy

$\displaystyle\penalty 1A\Longrightarrow B\qquad B\Longrightarrow A$

$LR\textrm{-}E$

$\displaystyle\Box A,\Gamma\Longrightarrow\Delta,\Box B$

we have four kinds of partitions of the conclusion:

[TABLE]

In each case we have to choose partitions of the premisses that permit to construct a G3E(ND)-interpolant for the partition under consideration.

In case (1) we have

[TABLE]

This can be shown as follows. By IH there is some $C$ ( $D$ ) that is a G3E(ND)-interpolant of the given partition of the left (right) premiss. Thus both $C$ and $D$ contains only propositional variables common to $A$ and $B$ ; and (i) $\vdash A\Longrightarrow B,C\;$ (ii) $\vdash C\Longrightarrow\;$ (iii) $\vdash B\Longrightarrow A,D\;$ and (iv) $\vdash D\Longrightarrow\;$ . Since the common language of the partitions of the premisses is empty, no propositional variable can occur in $C$ nor in $D$ . Here is a proof that $C$ is a G3E(ND)-interpolant of the partition under consideration (the sequents $A\Longrightarrow B$ and $B\Longrightarrow A$ are derivable since they are the premisses of the instance of $LR$ - $E$ we are considering):

[TABLE]

In case (2) we have

[TABLE]

By IH it holds that some $C$ and $D$ are G3E(ND)-interpolants of the given partitions of the premisses. Thus, (i) $\vdash A\Longrightarrow C\;$ (ii) $\vdash C\Longrightarrow B\;$ (iii) $\vdash B\Longrightarrow D\;$ (iv) $\vdash D\Longrightarrow A\;$ and (v) all propositional variables in $C\cup D$ are in $A\cap B$ . Here is a proof that $\Box C$ is a G3E(ND)-interpolant of the given partition (the language condition is satisfied thanks to (v) ):

[TABLE]

In case (3) we have

[TABLE]

By IH, there are $C$ and $D$ that are G3E(ND)-interpolants of the partitions of the premisses. Thus (i) $\vdash\Longrightarrow B,C\;$ (ii) $\vdash C,A\Longrightarrow\;$ (iii) $\vdash\Longrightarrow A,D\;$ and (iv) $\vdash D,B\Longrightarrow\;$ . We prove that $\Diamond C$ is a G3E(ND)-interpolant of the (given partition of the) conclusion as follows:

[TABLE]

In case (4) we have

[TABLE]

By IH, there are G3E(ND)-interpolants $C$ and $D$ of the partitions of the premisses. Thus (i) $\vdash\Longrightarrow C\;$ (ii) $\vdash C,A\Longrightarrow B\;$ (iii) $\vdash\Longrightarrow D\;$ and (iv) $\vdash D,B\Longrightarrow A\;$ . Since the common language of the partitions of the premisses is empty, no propositional variable occurs in $C$ nor in $D$ . We show that $C$ is a G3E(ND)-interpolant of the partition under consideration as follows (as in case (1), $A\Longrightarrow B$ and $B\Longrightarrow A$ , being the premisses of the instance of $LR$ - $E$ under consideration, are derivable):

[TABLE]

• LR-M $)\quad$ If the last rule applied in $\mathcal{D}$ is

[TABLE]

we give directly the G3M(ND)-interpolants of the possible partitions of the conclusion (and of the appropriate partition of the premiss). The proofs are parallel to those for $LR$ - $E$ .

[TABLE]

• LR-R $)\quad$ If the last rule applied in $\mathcal{D}$ is

[TABLE]

we have four kinds of partitions of the conclusion:

[TABLE]

In case (1) we have two subcases according to whether $\Pi_{2}$ is empty or not. If it is not empty we have

[TABLE]

By IH, there is a G3R(D⋆)-interpolant $C$ of the chosen partition of the premiss. Thus (i) $\vdash A,\Pi_{1}\Longrightarrow B,C$ and (ii) $\vdash C,\Pi_{2}\Longrightarrow$ , and we have the following derivations

[TABLE]

When $\Pi_{2}$ (and $\Box\Pi_{2}$ ) is empty we cannot proceed as above since we cannot apply $LR$ - $R$ in the right derivation. But in this case, reasoning like in case (1) for rule $LR$ - $E$ , we can show that

[TABLE]

Cases (2) and (3) are similar to the corresponding cases for rule $LR$ - $E$ :

[TABLE]

In case (4) we have two subcases according to whether $\Pi_{1}$ is empty or not:

[TABLE]

The proofs are similar to those for case (1).

• LR-K $)\quad$ If the last rule applied in $\mathcal{D}$ is

[TABLE]

we give directly the G3K(D)-interpolants of the two possible partitions of the conclusion:

[TABLE]

The proofs are, respectively, parallel to those for cases (2) and (3) of $LR$ - $E$ (when $\Pi=\emptyset$ , we can proceed as for rule $R$ - $N$ and use $C$ instead of $\Box C$ and of $\Diamond C$ , respectively).

• L-D ${}^{\bot})\quad$ If the last rule applied in $\mathcal{D}$ is

tensy

$\displaystyle\penalty 1A\Longrightarrow$

$\scriptstyle\it{L\mbox{-}D^{\bot}}$

$\displaystyle\Box A,\Gamma\Longrightarrow\Delta$

we have two kinds of partitions of the conclusion, whose G3XD⊥-interpolants are, respectively:

tensy

$\displaystyle\penalty 1\langle A\Longrightarrow\;\stackrel{{\scriptstyle C}}{{||}}\;\Longrightarrow\;\rangle$

$\scriptstyle\it{L\mbox{-}D^{\bot}}$

$\displaystyle\langle\Box A,\Gamma_{1}^{\prime}\Longrightarrow\Delta_{1}\;\stackrel{{\scriptstyle C}}{{||}}\;\Gamma_{2}\Longrightarrow\Delta_{2}\rangle$

tensy

$\displaystyle\penalty 1\langle\;\Longrightarrow\;\stackrel{{\scriptstyle C}}{{||}}\;A\Longrightarrow\;\rangle$

$\scriptstyle\it{L\mbox{-}D^{\bot}}$

$\displaystyle\langle\Gamma_{1}\Longrightarrow\Delta_{1}\;\stackrel{{\scriptstyle C}}{{||}}\;\Box A,\Gamma_{2}^{\prime}\Longrightarrow\Delta_{2}\rangle$

• L-D◇ $)\quad$ If the last rule applied in $\mathcal{D}$ is

[TABLE]

we have three kinds of partitions of the conclusion:

[TABLE]

In cases (1) and (2) we have, respectively (omitting the right premiss for $L$ - $D^{\Diamond_{M}}$ ):

[TABLE]

Finally, in case (3) we have:

[TABLE]

By IH, we can assume that $C$ is an interpolant of the partition of the left premiss and $D$ of the right one. We have the following G3YD◇-derivations (Y $\in\{$ E,M $\}$ ):

[TABLE]

It is also immediate to notice that $\Box C$ satisfies the language condition for being a G3YD◇-interpolant of the conclusion since, by IH, we know that each propositional variable occurring in $C$ occurs in $A\cap B$ .

• L-D⋆ $)\quad$ If the last rule applied in $\mathcal{D}$ is

tensy

$\displaystyle\penalty 1\Pi\Longrightarrow$

$\scriptstyle\it{L\mbox{-}D^{\star}}$

$\displaystyle\Box\Pi,\Gamma\Longrightarrow\Delta$

we have the following kind of partition: $\langle\Box\Pi_{1},\Gamma^{\prime}_{1}\Longrightarrow\Delta_{1}\;{||}\;\Box\Pi_{2},\Gamma^{\prime}_{2}\Longrightarrow\Delta_{2}\rangle$

If $\Pi_{1}$ is not empty we have:

tensy

$\displaystyle\penalty 1\langle\Pi_{1}\Longrightarrow\;\stackrel{{\scriptstyle C}}{{||}}\;\Pi_{2}\Longrightarrow\;\rangle$

$\scriptstyle\it{L\mbox{-}D^{\star}}$

$\displaystyle\langle\Box\Pi_{1},\Gamma^{\prime}_{1}\Longrightarrow\Delta_{1}\;\stackrel{{\scriptstyle\Box C}}{{||}}\;\Box\Pi_{2},\Gamma^{\prime}_{2}\Longrightarrow\Delta_{2}\rangle$

By IH, there is some $C$ that is an interpolant of the premiss. It holds that $\vdash\Pi_{1}\Longrightarrow C$ and $\vdash C,\Pi_{2}\Longrightarrow\;$ . We show that $\Box C$ is a G3YD-interpolant (Y $\in\{$ R,K $\}$ ) of the partition of the conclusion as follows:

[TABLE]

If, instead, $\Pi_{1}$ is empty then $\Pi_{2}$ cannot be empty and we have:

tensy

$\displaystyle\penalty 1\langle\;\Longrightarrow\;\stackrel{{\scriptstyle C}}{{||}}\;\Pi_{2}\Longrightarrow\;\rangle$

$\scriptstyle\it{L\mbox{-}D^{\star}}$

$\displaystyle\langle\Gamma_{1}\Longrightarrow\Delta_{1}\;\stackrel{{\scriptstyle\Diamond C}}{{||}}\;\Box\Pi_{2},\Gamma^{\prime}_{2}\Longrightarrow\Delta_{2}\rangle$

By IH there is a formula $C$ , containing no propositional variable, such that $\vdash\;\Longrightarrow C$ and $\vdash C,\Pi_{2}\Longrightarrow\;$ . Thus, G3YD $\vdash\Gamma_{1}\Longrightarrow\Delta_{1},\Diamond C$ ( $L$ - $D^{*}$ makes $\Longrightarrow\Diamond C$ derivable from $\Longrightarrow C$ ) and G3YD $\vdash\Diamond\top,\Box\Pi_{2},\Gamma_{2}^{\prime}\Longrightarrow\Delta_{2}$ ( $LR$ - $Y$ makes $\Diamond C,\Box\Pi_{2}\Longrightarrow$ derivable from $C,\Pi_{2}\Longrightarrow$ when $\Pi_{2}\neq\emptyset$ ).

• R-N $)\quad$ If the last rule applied in $\mathcal{D}$ is

tensy

$\displaystyle\penalty 1\Longrightarrow A$

$\scriptstyle\it{R\mbox{-}N}$

$\displaystyle\Gamma\Longrightarrow\Delta,\Box A$

The interpolants for the two possible partitions are:

$(1)\;$ tensy

$\displaystyle\penalty 1\langle\;\Longrightarrow A\stackrel{{\scriptstyle\bot}}{{||}}\;\Longrightarrow\;\rangle$

$\scriptstyle\it{R\mbox{-}N}\quad$

$\displaystyle\langle\Gamma_{1}\Longrightarrow\Delta_{1}^{\prime},\Box A\;\stackrel{{\scriptstyle\bot}}{{||}}\;\Gamma_{2}\Longrightarrow\Delta_{2}\rangle$

$(2)\;$ tensy

$\displaystyle\penalty 1\langle\;\Longrightarrow\;\stackrel{{\scriptstyle\top}}{{||}}\;\Longrightarrow A\rangle$

$\scriptstyle\it{R\mbox{-}N}$

$\displaystyle\langle\Gamma_{1}\Longrightarrow\Delta_{1}\;\stackrel{{\scriptstyle\top}}{{||}}\;\Gamma_{2}\Longrightarrow\Delta_{2}^{\prime},\Box A\rangle$

This completes the proof. ∎

Proof of Theorem 0.5.1.

Assume that $A\supset B$ is a theorem of X. By Theorem 0.4.5 and Lemma 0.3.4 we have that G3X $\vdash A\Longrightarrow B$ . By Lemma 0.5.3 (taking $A$ as $\Gamma_{1}$ and $B$ as $\Delta_{2}$ and $\Gamma_{2},\Delta_{1}$ empty) and Theorem 0.4.5 there exists a formula $I$ that is an interpolant of $A\supset B$ – i.e. $I$ is such such that all propositional variables occurring in $I$ , if any, occur in both $A$ and $B$ and such that $A\supset I$ and $I\supset B$ are theorems of X. ∎

Observe that the proof is constructive in that Lemma 0.5.3 gives a procedure to extract an interpolant for $A\supset B$ from a given derivation of $A\Longrightarrow B$ . Furthermore the proof is purely proof-theoretic in that it makes no use of model-theoretic notions.

Craig’s theorem is often – e.g., in [23] for an extension of classical logic – stated in the following stronger version:

If $A\supset B$ is a theorem of the logic X, then

If $A$ and $B$ share some propositional variable, there is a formula $I$ , which contains propositional variables common to $A$ and $B$ only, such that both $A\supset I$ and $I\supset B$ are theorems of X; 2. 2.

Else, either $\neg A$ or $B$ is a theorem of X.

But the second condition doesn’t hold for modal and deontic logics where at least one of $N:=\Box\top$ and $D^{\bot}:=\Diamond\top$ is not a theorem. To illustrate, it holds that $\Box\top\supset\Box\top$ is a theorem of E and its interpolant is $\Box\bot$ (see Figure 5), but neither $\neg\Box\top$ nor $\Box\top$ is a theorem of E. Analogously, we have that $\Box\bot\supset\Box\bot$ is a theorem of E and its interpolant is $\Box\bot$ (see Figure 5), but neither $\neg\Box\bot$ nor $\Box\bot$ is a theorem of E. These counterexamples work in all extensions of E that don’t have both $N$ and $D^{\bot}$ as theorems: to prove the stronger version of Craig’s theorem we need $N$ and $D^{\bot}$ , respectively.

Among the deontic logics considered here, the stronger version of Craig’s theorem holds only for END⊥(◇), MND⊥(◇), and KD, as shown by the following

Corollary 0.5.4.

Let XD be one of **END⊥(◇), **MND⊥(◇)**, and KD. If $A\supset B$ is a theorem of XD and $A$ and $B$ share no propositional variable, then either $\neg A$ or $B$ is a theorem of XD.

Proof.

Suppose that XD $\vdash A\supset B$ and that $A$ and $B$ share no propositional variable, then the interpolant $I$ is constructed from $\bot$ and $\top$ by means of classical and deontic operators. Whenever $D^{\bot}$ and $N$ are theorems of XD, we have that $\Diamond\top\leftrightarrow\top$ , $\Box\top\leftrightarrow\top$ , $\Diamond\bot\leftrightarrow\bot$ , and $\Box\bot\leftrightarrow\bot$ are theorems of XD. Hence, the interpolant $I$ is (equivalent to) either $\bot$ or $\top$ . In the first case XD $\vdash\neg A$ and in the second one XD $\vdash B$ . ∎

As noted in [7, p. 298], Corollary 0.5.4 is a Halldén-completeness result. A logic X is Halldén-complete if, for every formulas $A$ and $B$ that share no propositional variable, X $\vdash A\lor B$ if and only if X $\vdash A$ or X $\vdash B$ . All the modal and deontic logics considered here, being based on classical logic, are such that $A\supset B$ is equivalent to $\neg A\lor B$ . Thus the deontic logics considered in Corollary 0.5.4 are Halldén-complete, whereas all other non-normal logics for which we have proved interpolation are Halldén-incomplete since they don’t satisfy Corollary 0.5.4.

Example 0.5.5 (Maehara’s lemma and rule $LR$ - $C$ ).

We have not been able to prove Maehara’s Lemma 0.5.3 for rule $LR$ - $C$ because of the cases where the principal formulas of the antecedent are splitted in the two elements of the partition. In particular, if we have two principal formulas in the antecedent, the problematic partitions are (omitting the weakening contexts):

(1) $\langle\Box A_{1}\Longrightarrow\;||\;\Box A_{2}\Longrightarrow\Box B\rangle$ (2) $\langle\Box A_{1}\Longrightarrow\Box B\;||\;\Box A_{2}\Longrightarrow\rangle$

To illustrate, an interpolant of the first partition would be a formula $I$ such that:

[TABLE]

But we have not been able to find partitions of the premisses allowing to find such $I$ . More in details, for the first premiss it is natural to consider the partition $\langle A_{1}\Longrightarrow\;\stackrel{{\scriptstyle C}}{{||}}\;A_{2}\Longrightarrow B\rangle$ in order to find an $I$ that satisfies $(iii)$ . But, for any combination of the partitions of the other two premisses that is compatible with $(iii)$ , we can prove that $(ii)$ is satisfied (by $\Box C$ ) but we have not been able to prove that also $(i)$ is satisfied.

0.6 Conclusion

We presented cut- and contraction-free sequent calculi for non-normal modal and deontic logics. We have proved that these calculi have good structural properties in that weakening and contraction are height-preserving admissible and cut is (syntactically) admissible. Moreover, we have shown that these calculi allow for a terminating decision procedure whose complexity is in Pspace. Finally, we have given a constructive proof of Craig’s interpolation property for all the logics that do not contain rule $LR$ - $C$ . As far as we know, it is still an open problem whether it is possible to give a constructive proof of interpolation for these logics. Another open question is whether the calculi given here can be used to give a constructive proof of the uniform interpolation property for non-normal logics as it is done in [34] for $\mathbf{IL_{p}}$ and in [2] for K and T.

Thanks. Thanks are due to Tiziano Dalmonte, Simone Martini, and two anonymous referees for many helpful suggestions.

Bibliography39

The reference list from the paper itself. Each links out to its DOI / PubMed record.

1[1] Basin, D., Matthews, S., Viganò, L.: ‘A New Method for Bounding the Complexity of Modal Logics’. In Gottlob, G. et al (eds.): Computational Logic and Proof Theory (KGC 1997) , pp. 89–102. Springer (1997)
2[2] Bilková M.: ‘Uniform Interpolation and Propositional Quantifiers in Modal Logics’. Studia Logica 85, 1–31 (2007)
3[3] Calardo, E., Rotolo, A.: ‘Variants of Multi-Relational Semantics for Propositional Non-Normal Modal Logics’. Journal of Applied Non-Classical Logics 24, 293–320 (2014)
4[4] Chellas, B.F.: Modal Logic: an Introduction . CUP, Cambridge (1980)
5[5] Chen, J., Greco, G., Palmigiano, A., Tzimoulis, A.: ‘Non Normal Logics: Semantic Analysis and Proof Theory’. In Iemhoff, R. et al (eds.) Logic, Language, Information, and Computation (WOLLIC 2019) , pp. 99–118. Springer (2019)
6[6] Dalmonte, T., Olivetti, N., Negri, S.: ‘Non-Normal Modal Logics: Bi-Neighbourhood Semantics and its Labelled Calculi’. In Bezanishvili, G. et al (eds.): Advances in Modal Logic 12 , pp. 159–178. College Publications (2018)
7[7] Fitting, M.: Proof Methods for Modal and Intuitionistic Logics . D. Reidel, Dordrecht (1983)
8[8] Forrester, J.W.: ‘Gentle Murder, or the Adverbial Samaritan’. Journal of Philosophy , 81, 193-197 (1984)

TL;DR

Contribution

Findings

Abstract

Peer Reviews

Videos

Sequent Calculi and Interpolation for Non-Normal Modal and Deontic Logics

Abstract

0.1 Introduction

Related Work.

Synopsis.

0.2 Non-normal Logics

0.2.1 Axiomatic Systems

Proposition 0.2.1**.**

Proposition 0.2.2**.**

0.2.2 Semantics

Definition 0.2.3**.**

Definition 0.2.4**.**

Proposition 0.2.5**.**

Theorem 0.2.6**.**

0.3 Sequent Calculi

0.3.1 Structural rules of inference

Proposition 0.3.1**.**

Proof.

Theorem 0.3.2**.**

Proof.

Lemma 0.3.3**.**

Proof.

Lemma 0.3.4**.**

Proof.

Theorem 0.3.5**.**

Proof.

Theorem 0.3.6**.**

Proof.

0.4 Decidability and syntactic completeness

0.4.1 Decision procedure for G3X

Proposition 0.4.1**.**

Definition 0.4.2** (G3X-decision procedure).**

Theorem 0.4.3**.**

Proof.

0.4.2 Equivalence with the axiomatic systems

Lemma 0.4.4**.**

Proof.

Theorem 0.4.5**.**

Proof.

Corollary 0.4.6**.**

0.4.3 Forrester’s Paradox

0.5 Craig’s Interpolation Theorem

Theorem 0.5.1** (Craig’s interpolation theorem).**

Definition 0.5.2**.**

Lemma 0.5.3** (Maehara’s lemma).**

Proof.

Proof of Theorem 0.5.1.

Corollary 0.5.4**.**

Proof.

Example 0.5.5** (Maehara’s lemma and rule LRLRLR-CCC).**

0.6 Conclusion

Proposition 0.2.1.

Proposition 0.2.2.

Definition 0.2.3.

Definition 0.2.4.

Proposition 0.2.5.

Theorem 0.2.6.

Proposition 0.3.1.

Theorem 0.3.2.

Lemma 0.3.3.

Lemma 0.3.4.

Theorem 0.3.5.

Theorem 0.3.6.

Proposition 0.4.1.

Definition 0.4.2 (G3X-decision procedure).

Theorem 0.4.3.

Lemma 0.4.4.

Theorem 0.4.5.

Corollary 0.4.6.

Theorem 0.5.1 (Craig’s interpolation theorem).

Definition 0.5.2.

Lemma 0.5.3 (Maehara’s lemma).

Corollary 0.5.4.

Example 0.5.5 (Maehara’s lemma and rule $LR$ - $C$ ).