Modal operators and frame conditions

This file defines the relational necessity and possibility of Kripke semantics over an accessibility relation R : SetRel W' W, as operators on propositions W → Prop: □[R] p w holds when p holds at every R-successor of w, ◇[R] p w when it holds at some. They are mathlib's SetRel.core and SetRel.preimage read on predicates (box_iff_mem_core, diamond_iff_mem_preimage), in the way Filter.Eventually reads a filter on predicates, so propositions stated as sets use the mathlib operators directly. Of the frame conditions of correspondence theory, reflexivity, symmetry and transitivity are mathlib's SetRel.IsRefl, SetRel.IsSymm and SetRel.IsTrans; this file adds seriality and the Euclidean property and proves the axioms K, T, D, B, 4, 5 and Alt₁ over their frames, each axiom defining its frame condition. Along a composite relation necessity nests in necessity (box_comp). Negation Swap, □¬p ↔ ¬□p for every p, defines functionality (box_not_iff_not_box_at_iff): a modal that commutes with negation is necessity along the graph of a function, which is precomposition (box_compl_eq_iff, box_graph).

Main definitions

• ModalLogic.Box, ModalLogic.Diamond, with notation □[R] and ◇[R].
• ModalLogic.IsSerial, ModalLogic.IsEuclidean: the frame conditions of D and 5.

References

• [Kri63] — relational semantics
• [BdRV01] — Chapter 3, frame definability

Box and diamond

def ModalLogic.Box {W : Type u_1} {W' : Type u_2} (R : SetRel W' W) (p : W → Prop) (w : W') : Prop

Necessity along R holds of p at w when p holds at every R-successor of w.

Equations

• ModalLogic.Box R p w = ∀ (v : W), (w, v) ∈ R → p v

def ModalLogic.Diamond {W : Type u_1} {W' : Type u_2} (R : SetRel W' W) (p : W → Prop) (w : W') : Prop

Possibility along R holds of p at w when p holds at some R-successor of w.

Equations

• ModalLogic.Diamond R p w = ∃ (v : W), (w, v) ∈ R ∧ p v

def ModalLogic.«term□[_]» : Lean.ParserDescr

Necessity along R holds of p at w when p holds at every R-successor of w.

Equations

• One or more equations did not get rendered due to their size.

def ModalLogic.«term◇[_]» : Lean.ParserDescr

Possibility along R holds of p at w when p holds at some R-successor of w.

Equations

• One or more equations did not get rendered due to their size.

theorem ModalLogic.box_iff_mem_core {W : Type u_1} {W' : Type u_2} {R : SetRel W' W} {p : W → Prop} {w : W'} : Box R p w ↔ w ∈ R.core {v : W | p v}

Necessity on predicates is the mathlib core on sets.

theorem ModalLogic.diamond_iff_mem_preimage {W : Type u_1} {W' : Type u_2} {R : SetRel W' W} {p : W → Prop} {w : W'} : Diamond R p w ↔ w ∈ R.preimage {v : W | p v}

Possibility on predicates is the mathlib preimage on sets.

@[simp]

theorem ModalLogic.not_box {W : Type u_1} {W' : Type u_2} {R : SetRel W' W} {p : W → Prop} {w : W'} : ¬Box R p w ↔ Diamond R (fun (v : W) => ¬p v) w

@[simp]

theorem ModalLogic.not_diamond {W : Type u_1} {W' : Type u_2} {R : SetRel W' W} {p : W → Prop} {w : W'} : ¬Diamond R p w ↔ Box R (fun (v : W) => ¬p v) w

theorem ModalLogic.box_and {W : Type u_1} {W' : Type u_2} (R : SetRel W' W) {p : W → Prop} {w : W'} (q : W → Prop) : Box R (fun (v : W) => p v ∧ q v) w ↔ Box R p w ∧ Box R q w

Necessity distributes over conjunction ([Hin62]'s a believes A and B ↔ a believes A and a believes B).

theorem ModalLogic.box_iUnion {W : Type u_1} {W' : Type u_2} {p : W → Prop} {w : W'} {ι : Sort u_3} (R : ι → SetRel W' W) : Box (⋃ (i : ι), R i) p w ↔ ∀ (i : ι), Box (R i) p w

Necessity along a union of relations is necessity along each.

theorem ModalLogic.box_congr_left {W : Type u_1} {W' : Type u_2} {R : SetRel W' W} {p : W → Prop} {w w'' : W'} (h : ∀ (v : W), (w, v) ∈ R ↔ (w'', v) ∈ R) : Box R p w ↔ Box R p w''

Necessity depends only on the worlds accessed, so two worlds accessing the same worlds carry the same box.

theorem ModalLogic.box_comp {W : Type u_1} (R S : SetRel W W) (p : W → Prop) : Box (R.comp S) p = Box R (Box S p)

Necessity along a composite relation is necessity nested in necessity.

theorem ModalLogic.diamond_comp {W : Type u_1} (R S : SetRel W W) (p : W → Prop) : Diamond (R.comp S) p = Diamond R (Diamond S p)

Possibility along a composite relation is possibility nested in possibility.

Frame conditions

class ModalLogic.IsSerial {W : Type u_1} (R : SetRel W W) : Prop

R is serial if every world accesses at least one world.

• serial (w : W) : ∃ (v : W), (w, v) ∈ R

class ModalLogic.IsEuclidean {W : Type u_1} (R : SetRel W W) : Prop

R is Euclidean if any two R-successors of a world access each other.

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

instance ModalLogic.instIsEuclideanUnivProd {W : Type u_1} : IsEuclidean Set.univ

instance ModalLogic.instIsSerialOfIsRefl {W : Type u_1} {R : SetRel W W} [R.IsRefl] : IsSerial R

Reflexive relations are serial.

instance ModalLogic.instIsSerialComp {W : Type u_1} {R S : SetRel W W} [IsSerial R] [IsSerial S] : IsSerial (R.comp S)

A composite of serial relations is serial.

instance ModalLogic.instIsSymmOfIsReflOfIsEuclidean {W : Type u_1} {R : SetRel W W} [R.IsRefl] [IsEuclidean R] : R.IsSymm

Reflexive and Euclidean implies symmetric.

instance ModalLogic.instIsTransOfIsReflOfIsEuclidean {W : Type u_1} {R : SetRel W W} [R.IsRefl] [IsEuclidean R] : R.IsTrans

Reflexive and Euclidean implies transitive.

instance ModalLogic.instIsEuclideanOfIsSymmOfIsTrans {W : Type u_1} {R : SetRel W W} [R.IsSymm] [R.IsTrans] : IsEuclidean R

Symmetric and transitive implies Euclidean.

Axiom correspondence

theorem ModalLogic.box_K {W : Type u_1} {R : SetRel W W} {p q : W → Prop} {w : W} (hpq : Box R (fun (v : W) => p v → q v) w) (hp : Box R p w) : Box R q w

Axiom K, □(p → q) → □p → □q, holds over any relation.

theorem ModalLogic.box_T {W : Type u_1} {R : SetRel W W} {p : W → Prop} {w : W} [R.IsRefl] (h : Box R p w) : p w

Axiom T, □p → p, holds over a reflexive relation.

theorem ModalLogic.box_D {W : Type u_1} {R : SetRel W W} {p : W → Prop} {w : W} [IsSerial R] (h : Box R p w) : Diamond R p w

Axiom D, □p → ◇p, holds over a serial relation.

theorem ModalLogic.diamond_of_box {W : Type u_1} {R : SetRel W W} {p : W → Prop} {w : W} {S : SetRel W W} (h : Diamond R (fun (x : W) => (w, x) ∈ S) w) (hp : Box R p w) : Diamond S p w

Necessity along R gives possibility along a relation sharing an R-successor of the world, and box_D is the case S = R.

theorem ModalLogic.box_B {W : Type u_1} {R : SetRel W W} {p : W → Prop} {w : W} [R.IsSymm] (h : p w) : Box R (Diamond R p) w

Axiom B, p → □◇p, holds over a symmetric relation.

theorem ModalLogic.box_four {W : Type u_1} {R : SetRel W W} {p : W → Prop} {w : W} [R.IsTrans] (h : Box R p w) : Box R (Box R p) w

Axiom 4, □p → □□p, holds over a transitive relation.

theorem ModalLogic.box_five {W : Type u_1} {R : SetRel W W} {p : W → Prop} {w : W} [IsEuclidean R] (h : Diamond R p w) : Box R (Diamond R p) w

Axiom 5, ◇p → □◇p, holds over a Euclidean relation.

theorem ModalLogic.box_of_diamond_box {W : Type u_1} {R : SetRel W W} {p : W → Prop} {w : W} [IsEuclidean R] (h : Diamond R (Box R p) w) : Box R p w

Over a Euclidean relation what is possibly necessary is necessary, ◇□p → □p.

theorem ModalLogic.diamond_box_of_box {W : Type u_1} {R : SetRel W W} {p : W → Prop} {w : W} [IsSerial R] [R.IsTrans] (h : Box R p w) : Diamond R (Box R p) w

Over a serial transitive relation, □p → ◇□p.

Frame definability

Each axiom, read as an inequality between operators on W → Prop, characterizes its frame condition.

theorem ModalLogic.box_T_iff {W : Type u_1} {R : SetRel W W} : Box R ≤ id ↔ R.IsRefl

T defines reflexivity.

theorem ModalLogic.diamond_T_iff {W : Type u_1} {R : SetRel W W} : id ≤ Diamond R ↔ R.IsRefl

Axiom T for the diamond, that what holds is possible, defines reflexivity.

theorem ModalLogic.box_D_iff {W : Type u_1} {R : SetRel W W} : Box R ≤ Diamond R ↔ IsSerial R

D defines seriality.

theorem ModalLogic.box_B_iff {W : Type u_1} {R : SetRel W W} : id ≤ Box R ∘ Diamond R ↔ R.IsSymm

B defines symmetry.

theorem ModalLogic.box_four_iff {W : Type u_1} {R : SetRel W W} : Box R ≤ Box R ∘ Box R ↔ R.IsTrans

4 defines transitivity.

theorem ModalLogic.box_five_iff {W : Type u_1} {R : SetRel W W} : Diamond R ≤ Box R ∘ Diamond R ↔ IsEuclidean R

5 defines the Euclidean property.

Seriality and functionality at a world

Excluded middle and non-contradiction for necessity at a world, read for every prejacent, each define a condition on the successors of the world, and Negation Swap defines their conjunction: □p ∨ □¬p holds for every p iff the world sees at most one world (Alt₁), ¬(□p ∧ □¬p) iff it sees at least one (D), and □¬p ↔ ¬□p iff it sees exactly one. For possibility the two conditions trade places. A relation satisfying Negation Swap at every world is the graph of a function, and necessity along a graph is precomposition with the function.

theorem ModalLogic.diamond_le_box_at_iff {W : Type u_2} {W' : Type u_3} {R : SetRel W' W} {w : W'} : (∀ (p : W → Prop), Diamond R p w → Box R p w) ↔ ∀ ⦃v : W⦄, (w, v) ∈ R → ∀ ⦃u : W⦄, (w, u) ∈ R → v = u

Axiom Alt₁, ◇p → □p for every p, holds at w iff w sees at most one world.

theorem ModalLogic.diamond_le_box_iff {W : Type u_2} {W' : Type u_3} {R : SetRel W' W} : Diamond R ≤ Box R ↔ ∀ (w : W') ⦃v : W⦄, (w, v) ∈ R → ∀ ⦃u : W⦄, (w, u) ∈ R → v = u

Alt₁ defines partial functionality.

theorem ModalLogic.box_or_box_not_at_iff {W : Type u_2} {W' : Type u_3} {R : SetRel W' W} {w : W'} : (∀ (p : W → Prop), Box R p w ∨ Box R (fun (v : W) => ¬p v) w) ↔ ∀ ⦃v : W⦄, (w, v) ∈ R → ∀ ⦃u : W⦄, (w, u) ∈ R → v = u

The excluded middle for every p at w, □p ∨ □¬p, holds iff w sees at most one world.

theorem ModalLogic.box_not_of_not_box_at_iff {W : Type u_2} {W' : Type u_3} {R : SetRel W' W} {w : W'} : (∀ (p : W → Prop), ¬Box R p w → Box R (fun (v : W) => ¬p v) w) ↔ ∀ ⦃v : W⦄, (w, v) ∈ R → ∀ ⦃u : W⦄, (w, u) ∈ R → v = u

The neg-raising inference for every p at w, ¬□p → □¬p, holds iff w sees at most one world.

theorem ModalLogic.not_box_and_box_not_at_iff {W : Type u_2} {W' : Type u_3} {R : SetRel W' W} {w : W'} : (∀ (p : W → Prop), ¬(Box R p w ∧ Box R (fun (v : W) => ¬p v) w)) ↔ ∃ (v : W), (w, v) ∈ R

Non-contradiction for every p at w, ¬(□p ∧ □¬p), holds iff w sees some world.

theorem ModalLogic.box_not_iff_not_box_at_iff {W : Type u_2} {W' : Type u_3} {R : SetRel W' W} {w : W'} : (∀ (p : W → Prop), Box R (fun (v : W) => ¬p v) w ↔ ¬Box R p w) ↔ ∃! v : W, (w, v) ∈ R

Negation Swap for every p at w, □¬p ↔ ¬□p, holds iff w sees exactly one world.

theorem ModalLogic.diamond_or_diamond_not_at_iff {W : Type u_2} {W' : Type u_3} {R : SetRel W' W} {w : W'} : (∀ (p : W → Prop), Diamond R p w ∨ Diamond R (fun (v : W) => ¬p v) w) ↔ ∃ (v : W), (w, v) ∈ R

The excluded middle for possibility, ◇p ∨ ◇¬p for every p at w, holds iff w sees some world.

theorem ModalLogic.not_diamond_and_diamond_not_at_iff {W : Type u_2} {W' : Type u_3} {R : SetRel W' W} {w : W'} : (∀ (p : W → Prop), ¬(Diamond R p w ∧ Diamond R (fun (v : W) => ¬p v) w)) ↔ ∀ ⦃v : W⦄, (w, v) ∈ R → ∀ ⦃u : W⦄, (w, u) ∈ R → v = u

Non-contradiction for possibility, ¬(◇p ∧ ◇¬p) for every p at w, holds iff w sees at most one world.

@[simp]

theorem ModalLogic.box_graph {W : Type u_2} {W' : Type u_3} (f : W' → W) (p : W → Prop) : Box (Function.graph f) p = p ∘ f

Necessity along the graph of a function is precomposition with the function.

theorem ModalLogic.box_compl_eq_iff {W : Type u_2} {W' : Type u_3} {R : SetRel W' W} : (∀ (p : W → Prop), Box R pᶜ = (Box R p)ᶜ) ↔ ∃ (f : W' → W), Function.graph f = R

Negation Swap at every world holds iff the relation is the graph of a function.