Modal logic over accessibility relations

This file proves the order theory of box and diamond: the Galois connection ◇[R] ⊣ □[flip R] and the normality laws it yields, antitonicity in the relation (conversational backgrounds strengthen necessity by shrinking accessibility), 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 box/diamond as the universal-accessibility case R = ⊤.

References

• [Kra81] — 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 : W → W → Prop} {p : W → Prop} [hS : 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 : W → W → Prop) (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 : W → W → Prop) (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 : W → W → Prop) [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 : W → W → Prop) : GaloisConnection (diamond R) (box (flip R))

◇ 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 : W → W → Prop) : Monotone (box R)

theorem ModalLogic.diamond_mono {W : Type u_1} (R : W → W → Prop) : Monotone (diamond R)

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

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

theorem ModalLogic.box_top {W : Type u_1} (R : W → W → Prop) : box R ⊤ = ⊤

Necessitation: □⊤ = ⊤.

theorem ModalLogic.self_imp_box_flip_diamond {W : Type u_1} (R : W → W → Prop) (p : W → Prop) : p ≤ box (flip R) (diamond R p)

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

Accessibility restriction

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

Restricting accessibility strengthens necessity.

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

Restricting accessibility weakens possibility.

Bundled frame classes

class ModalLogic.IsS5Frame {W : Type u_1} (R : W → W → Prop) extends Std.Refl R, ModalLogic.IsEuclidean R : Prop

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

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

class ModalLogic.IsKD45Frame {W : Type u_1} (R : W → W → Prop) extends ModalLogic.IsSerial R, IsTrans W R, ModalLogic.IsEuclidean R : Prop

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

• serial : Relator.LeftTotal R
• trans (a b c : W) : R a b → R b c → R a c
• eucl (w v u : W) : R w v → R w u → R v u

class ModalLogic.IsK45Frame {W : Type u_1} (R : W → W → Prop) extends IsTrans W R, ModalLogic.IsEuclidean R : Prop

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

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

class ModalLogic.IsKTBFrame {W : Type u_1} (R : W → W → Prop) extends Std.Refl R, Std.Symm R : Prop

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

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

The Gallin hierarchy

Operators (W → Prop) → W → Prop form a three-level hierarchy ([Gal75]): arbitrary operators, the indicial (Kripke-definable) ones — box R for some accessibility relation — and S5, the indicial case R = ⊤. 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 box R for some accessibility relation R.

Equations

• ModalLogic.IsIndicial N = ∃ (R : W → W → Prop), N = ModalLogic.box R

theorem ModalLogic.box_isIndicial {W : Type u_1} (R : W → W → Prop) : IsIndicial (box R)

Flat S5 operators

poss/nec are the flat existential/universal modals (∃ w / ∀ w) — the S5 operators □[⊤]/◇[⊤] with their vestigial evaluation world dropped.

def ModalLogic.poss {W : Type u_1} (p : W → Prop) : Prop

Flat S5 possibility: poss p iff p holds at some world.

Equations

• ModalLogic.poss p = ∃ (w : W), p w

def ModalLogic.nec {W : Type u_1} (p : W → Prop) : Prop

Flat S5 necessity: nec p iff p holds at every world.

Equations

• ModalLogic.nec p = ∀ (w : W), p w

theorem ModalLogic.nec_mono {W : Type u_1} : Monotone nec

Decidability over finite worlds

@[instance_reducible]

instance ModalLogic.instDecidableBoxOfFintypeOfDecidablePred {W : Type u_1} [Fintype W] (R : W → W → Prop) (p : W → Prop) (w : W) [(v : W) → Decidable (R w v)] [DecidablePred p] : Decidable (box R p w)

Equations

• ModalLogic.instDecidableBoxOfFintypeOfDecidablePred R p w = ModalLogic.instDecidableBoxOfFintypeOfDecidablePred._aux_1 R p w

@[instance_reducible]

instance ModalLogic.instDecidableDiamondOfFintypeOfDecidablePred {W : Type u_1} [Fintype W] (R : W → W → Prop) (p : W → Prop) (w : W) [(v : W) → Decidable (R w v)] [DecidablePred p] : Decidable (diamond R p w)

Equations

• ModalLogic.instDecidableDiamondOfFintypeOfDecidablePred R p w = ModalLogic.instDecidableDiamondOfFintypeOfDecidablePred._aux_1 R p w