Modal logic over accessibility relations

This file proves the order theory of □ and ◇: the Galois connection ◇[R] ⊣ □[R.inv] and the normality laws it yields, antitonicity in the relation (conversational backgrounds strengthen necessity by shrinking accessibility), necessity along the transitive closure as the infinite conjunction of iterated necessity, and the modal square of opposition. It also defines the bundled frame classes IsS5Frame, IsKD45Frame, IsK45Frame, IsKTBFrame, and the indicial operators, with Montague's S5 □/◇ as the universal-accessibility case R = .univ. On propositions as sets the same laws are mathlib's SetRel.core_mono, SetRel.core_inter, SetRel.core_univ, SetRel.preimage_union, SetRel.image_core_gc and SetRel.core_transGen.

References

• [Kra81b] — necessity strengthened by restricting accessibility
• [CP08a] — the modal square of opposition
• [Gal75] — the indicial operator hierarchy
• [DWP81] — Montague's S5 operators

Modal square of opposition

theorem ModalLogic.box_disjoint_compl {W : Type u_1} {R : SetRel W W} {p : W → Prop} [IsSerial R] : Disjoint (Box R p) (Box R pᶜ)

Over a serial relation, □p and □¬p are incompatible.

theorem ModalLogic.compl_box_compl {W : Type u_1} (R : SetRel W W) (p : W → Prop) : (Box R pᶜ)ᶜ = Diamond R p

Box–diamond duality as an equation of predicates: ¬□¬p = ◇p.

def ModalLogic.modalSquare {W : Type u_1} (R : SetRel W W) (p : W → Prop) : Aristotelian.Square (W → Prop)

The modal square of opposition over R: A = □p, E = □¬p, I = ◇p, O = ¬□p.

Equations

• ModalLogic.modalSquare R p = { A := ModalLogic.Box R p, E := ModalLogic.Box R pᶜ, I := ModalLogic.Diamond R p, O := (ModalLogic.Box R p)ᶜ }

theorem ModalLogic.modalSquare_relations {W : Type u_1} (R : SetRel W W) [IsSerial R] (p : W → Prop) : Aristotelian.SquareRelations (modalSquare R p)

Over a serial relation the modal square satisfies all six Aristotelian relations.

The Galois connection and normality

theorem ModalLogic.diamond_box_gc {W : Type u_1} (R : SetRel W W) : GaloisConnection (Diamond R) (Box R.inv)

◇ along R is left adjoint to □ along the converse relation, the characteristic adjunction of relational modality.

theorem ModalLogic.box_mono {W : Type u_1} (R : SetRel W W) : Monotone (Box R)

theorem ModalLogic.diamond_mono {W : Type u_1} (R : SetRel W W) : Monotone (Diamond R)

theorem ModalLogic.box_inf {W : Type u_1} (R : SetRel W W) {p q : W → Prop} : Box R (p ⊓ q) = Box R p ⊓ Box R q

theorem ModalLogic.diamond_sup {W : Type u_1} (R : SetRel W W) {p q : W → Prop} : Diamond R (p ⊔ q) = Diamond R p ⊔ Diamond R q

theorem ModalLogic.box_top {W : Type u_1} (R : SetRel W W) : Box R ⊤ = ⊤

Necessitation: □⊤ = ⊤.

theorem ModalLogic.le_box_inv_diamond {W : Type u_1} (R : SetRel W W) (p : W → Prop) : p ≤ Box R.inv (Diamond R p)

Conversion (Prior's tense axiom A ⊃ G P A), the unit of the adjunction: over any relation, p ≤ □_{R⁻¹} ◇_R p.

Accessibility restriction

theorem ModalLogic.box_restrict {W : Type u_1} (p : W → Prop) : Antitone fun (R : SetRel W W) => Box R p

Restricting accessibility strengthens necessity.

theorem ModalLogic.diamond_restrict {W : Type u_1} (p : W → Prop) : Monotone fun (R : SetRel W W) => Diamond R p

Restricting accessibility weakens possibility.

Transitive closure

Necessity along the transitive closure of R is the infinite conjunction of iterated necessity along R: □[R⁺] p = □[R] p ∧ □[R] (□[R] p) ∧ ⋯.

theorem ModalLogic.box_iterate_succ_of_box_transGen {W : Type u_1} (R : SetRel W W) (n : ℕ) {p : W → Prop} {w : W} : Box R.transGen p w → (Box R)^[n + 1] p w

theorem ModalLogic.exists_box_iterate_imp_of_transGen {W : Type u_1} (R : SetRel W W) {w v : W} (h : Relation.TransGen (fun (x1 x2 : W) => (x1, x2) ∈ R) w v) : ∃ (n : ℕ), ∀ (q : W → Prop), (Box R)^[n + 1] q w → q v

theorem ModalLogic.box_transGen_iff {W : Type u_1} (R : SetRel W W) {p : W → Prop} {w : W} : Box R.transGen p w ↔ ∀ (n : ℕ), (Box R)^[n + 1] p w

Bundled frame classes

class ModalLogic.IsS5Frame {W : Type u_1} (R : SetRel W W) extends Std.Refl fun (x1 x2 : W) => (x1, x2) ∈ R, ModalLogic.IsEuclidean R : Prop

R is an S5 frame if it is reflexive and Euclidean.

• refl (a : W) : (a, a) ∈ R
• eucl (w v u : W) : (w, v) ∈ R → (w, u) ∈ R → (v, u) ∈ R

class ModalLogic.IsKD45Frame {W : Type u_1} (R : SetRel W W) extends ModalLogic.IsSerial R, IsTrans W fun (x1 x2 : W) => (x1, x2) ∈ R, ModalLogic.IsEuclidean R : Prop

R is a KD45 frame, the doxastic frame, if it is serial, transitive, and Euclidean.

• serial (w : W) : ∃ (v : W), (w, v) ∈ R
• trans (a b c : W) : (a, b) ∈ R → (b, c) ∈ R → (a, c) ∈ R
• eucl (w v u : W) : (w, v) ∈ R → (w, u) ∈ R → (v, u) ∈ R

class ModalLogic.IsK45Frame {W : Type u_1} (R : SetRel W W) extends IsTrans W fun (x1 x2 : W) => (x1, x2) ∈ R, ModalLogic.IsEuclidean R : Prop

R is a K45 frame if it is transitive and Euclidean.

• trans (a b c : W) : (a, b) ∈ R → (b, c) ∈ R → (a, c) ∈ R
• eucl (w v u : W) : (w, v) ∈ R → (w, u) ∈ R → (v, u) ∈ R

class ModalLogic.IsKTBFrame {W : Type u_1} (R : SetRel W W) extends Std.Refl fun (x1 x2 : W) => (x1, x2) ∈ R, Std.Symm fun (x1 x2 : W) => (x1, x2) ∈ R : Prop

R is a KTB frame if it is reflexive and symmetric.

• refl (a : W) : (a, a) ∈ R
• symm (a b : W) : (a, b) ∈ R → (b, a) ∈ R

theorem ModalLogic.diamond_box_iff {W : Type u_1} (R : SetRel W W) [IsKD45Frame R] {p : W → Prop} {w : W} : Diamond R (Box R p) w ↔ Box R p w

Over a KD45 frame the modalities collapse: ◇□p ↔ □p. An agent introspective about her own beliefs considers it possible that she must do something exactly when she must.

The Gallin hierarchy

Operators (W → Prop) → W → Prop form a three-level hierarchy ([Gal75]): arbitrary operators, the indicial (Kripke-definable) ones, □[R] for some accessibility relation, and S5, the indicial case R = .univ. Tense and other non-Kripke operators live outside IsIndicial.

def ModalLogic.IsIndicial {W : Type u_1} (N : (W → Prop) → W → Prop) : Prop

An operator on world-propositions is indicial (Kripke-definable) if it is □[R] for some accessibility relation R.

Equations

• ModalLogic.IsIndicial N = ∃ (R : SetRel W W), N = ModalLogic.Box R

theorem ModalLogic.box_isIndicial {W : Type u_1} (R : SetRel W W) : IsIndicial (Box R)

Decidability over finite worlds

@[instance_reducible]

instance ModalLogic.instDecidableBoxOfFintypeOfMemProdSetRelMkOfDecidablePred {W : Type u_1} {W' : Type u_2} [Fintype W] (R : SetRel W' W) (p : W → Prop) (w : W') [(v : W) → Decidable ((w, v) ∈ R)] [DecidablePred p] : Decidable (Box R p w)

Equations

• ModalLogic.instDecidableBoxOfFintypeOfMemProdSetRelMkOfDecidablePred R p w = { decide := decide (∀ a ∈ Finset.univ, (fun (v : W) => (w, v) ∈ R → p v) a), reflects_decide := ⋯ }

@[instance_reducible]

instance ModalLogic.instDecidableDiamondOfFintypeOfMemProdSetRelMkOfDecidablePred {W : Type u_1} {W' : Type u_2} [Fintype W] (R : SetRel W' W) (p : W → Prop) (w : W') [(v : W) → Decidable ((w, v) ∈ R)] [DecidablePred p] : Decidable (Diamond R p w)

Equations

• ModalLogic.instDecidableDiamondOfFintypeOfMemProdSetRelMkOfDecidablePred R p w = { decide := decide (∃ a ∈ Finset.univ, (fun (v : W) => (w, v) ∈ R ∧ p v) a), reflects_decide := ⋯ }