Logical Equivalence in Modal Logic

This module defines logical equivalence for modal propositions. The definitions are parametric on the class of models under consideration.

We also instantiate LogicalEquivalence for Modal Logic K, i.e., equivalence for the class of all models.

def Cslib.Logic.Modal.Proposition.Equiv {World : Type u_1} {Atom : Type u_2} (m : Model World Atom) (φ₁ φ₂ : Proposition Atom) : Prop

The modal propositions φ₁ and φ₂ are equivalent in the model m.

Equations

• Cslib.Logic.Modal.Proposition.Equiv m φ₁ φ₂ = ∀ (w : World), ⇓{ m := m, w := w, φ := Cslib.Logic.HasIff.iff φ₁ φ₂ }

@[instance_reducible]

instance Cslib.Logic.Modal.instCongruencePropositionEquiv {World✝ : Type u_1} {Atom✝ : Type u_2} {m : Model World✝ Atom✝} : Congruence (Proposition.Equiv m)

Equations

• Cslib.Logic.Modal.instCongruencePropositionEquiv = { }

theorem Cslib.Logic.Modal.Proposition.equiv_def {World : Type u_1} {Atom : Type u_2} (m : Model World Atom) (φ₁ φ₂ : Proposition Atom) : Equiv m φ₁ φ₂ ↔ Congruence.r (Equiv m) φ₁ φ₂

theorem Cslib.Logic.Modal.Proposition.equiv_iff_forall_der {World : Type u_1} {Atom : Type u_2} (m : Model World Atom) (φ₁ φ₂ : Proposition Atom) : Congruence.r (Equiv m) φ₁ φ₂ ↔ ∀ (w : World), ⇓{ m := m, w := w, φ := HasIff.iff φ₁ φ₂ }

theorem Cslib.Logic.Modal.Proposition.equiv_iff_forall_iff {World : Type u_1} {Atom : Type u_2} {m : Model World Atom} {φ₁ φ₂ : Proposition Atom} : Congruence.r (Equiv m) φ₁ φ₂ ↔ ∀ (w : World), ⇓{ m := m, w := w, φ := φ₁ } ↔ ⇓{ m := m, w := w, φ := φ₂ }

@[reducible, inline]

abbrev Cslib.Logic.Modal.ModelClass (World : Type u_1) (Atom : Type u_2) : Type (max u_2 u_1)

A class of models, defined as a set.

Equations

• Cslib.Logic.Modal.ModelClass World Atom = Set (Cslib.Logic.Modal.Model World Atom)

def Cslib.Logic.Modal.Proposition.EquivWithin {World : Type u_1} {Atom : Type u_2} (S : ModelClass World Atom) (φ₁ φ₂ : Proposition Atom) : Prop

The modal propositions φ₁ and φ₂ are equivalent in the model class S.

Equations

• Cslib.Logic.Modal.Proposition.EquivWithin S φ₁ φ₂ = ∀ m ∈ S, Cslib.Congruence.r (Cslib.Logic.Modal.Proposition.Equiv m) φ₁ φ₂

@[instance_reducible]

instance Cslib.Logic.Modal.instCongruencePropositionEquivWithin {World✝ : Type u_1} {Atom✝ : Type u_2} {S : ModelClass World✝ Atom✝} : Congruence (Proposition.EquivWithin S)

Equations

• Cslib.Logic.Modal.instCongruencePropositionEquivWithin = { }

theorem Cslib.Logic.Modal.Proposition.equivWithin_def {World : Type u_1} {Atom : Type u_2} (S : ModelClass World Atom) (φ₁ φ₂ : Proposition Atom) : EquivWithin S φ₁ φ₂ ↔ Congruence.r (EquivWithin S) φ₁ φ₂

theorem Cslib.Logic.Modal.Proposition.equiv_of_EquivWithin {World : Type u_1} {Atom : Type u_2} {φ₁ φ₂ : Proposition Atom} {S : ModelClass World Atom} (h : Congruence.r (EquivWithin S) φ₁ φ₂) (m : Model World Atom) (hm : m ∈ S) : Congruence.r (Equiv m) φ₁ φ₂

theorem Cslib.Logic.Modal.Proposition.equivWithin_valid {World : Type u_1} {Atom : Type u_2} (S : ModelClass World Atom) (φ₁ φ₂ : Proposition Atom) (h : Congruence.r (EquivWithin S) φ₁ φ₂) : valid S φ₁ ↔ valid S φ₂

Logical equivalence preserves validity.

inductive Cslib.Logic.Modal.Proposition.Context (Atom : Type u) : Type u

Propositional contexts.

• hole {Atom : Type u} : Context Atom
• not {Atom : Type u} (c : Context Atom) : Context Atom
• andL {Atom : Type u} (c : Context Atom) (φ : Proposition Atom) : Context Atom
• andR {Atom : Type u} (φ : Proposition Atom) (c : Context Atom) : Context Atom
• diamond {Atom : Type u} (c : Context Atom) : Context Atom

def Cslib.Logic.Modal.Proposition.Context.fill {Atom : Type u_1} (c : Context Atom) (φ : Proposition Atom) : Proposition Atom

Replaces a hole in a propositional context with a proposition.

Equations

• Cslib.Logic.Modal.Proposition.Context.hole.fill φ = φ
• c_2.not.fill φ = (c_2.fill φ).not
• (c_2.andL φ').fill φ = (c_2.fill φ).and φ'
• (Cslib.Logic.Modal.Proposition.Context.andR φ' c_2).fill φ = φ'.and (c_2.fill φ)
• c_2.diamond.fill φ = (c_2.fill φ).diamond

@[instance_reducible]

instance Cslib.Logic.Modal.instHasContextProposition {Atom : Type u_1} : HasContext (Proposition Atom)

Equations

• Cslib.Logic.Modal.instHasContextProposition = { Context := Cslib.Logic.Modal.Proposition.Context Atom, fill := Cslib.Logic.Modal.Proposition.Context.fill }

theorem Cslib.Logic.Modal.Proposition.Context.fill_def {Atom : Type u_1} {φ : Proposition Atom} {c : HasContext.Context (Proposition Atom)} : fill c φ = c<[φ]

instance Cslib.Logic.Modal.instIsEquivPropositionEquiv {World : Type u_1} {Atom : Type u_2} (m : Model World Atom) : IsEquiv (Proposition Atom) (Proposition.Equiv m)

Logical equivalence is an equivalence relation.

instance Cslib.Logic.Modal.instIsEquivPropositionEquivWithin {World : Type u_1} {Atom : Type u_2} (S : ModelClass World Atom) : IsEquiv (Proposition Atom) (Proposition.EquivWithin S)

Logical equivalence within a class is an equivalence relation.

instance Cslib.Logic.Modal.instLawfulCongruencePropositionEquiv {World : Type u_1} {Atom : Type u_2} (m : Model World Atom) : LawfulCongruence (Proposition.Equiv m)

Logical equivalence is a congruence.

instance Cslib.Logic.Modal.instLawfulCongruencePropositionEquivWithin {World : Type u_1} {Atom : Type u_2} (S : ModelClass World Atom) : LawfulCongruence (Proposition.EquivWithin S)

Logical equivalence within a class is a congruence.

structure Cslib.Logic.Modal.Satisfies.Context (World : Type u_1) (Atom : Type u_2) : Type (max u_1 u_2)

Judgemental contexts.

• m : Model World Atom

  The model to consider.

• w : World

  The world to check propositions against.

def Cslib.Logic.Modal.Satisfies.Context.fill {World : Type u_1} {Atom : Type u_2} (c : Context World Atom) (φ : Proposition Atom) : Judgement World Atom

Fills a judgemental context with a proposition.

Equations

• c.fill φ = { m := c.m, w := c.w, φ := φ }

@[instance_reducible]

instance Cslib.Logic.Modal.instHasHContextJudgementProposition {World : Type u_1} {Atom : Type u_2} : HasHContext (Judgement World Atom) (Proposition Atom)

Equations

• Cslib.Logic.Modal.instHasHContextJudgementProposition = { Context := Cslib.Logic.Modal.Satisfies.Context World Atom, fill := Cslib.Logic.Modal.Satisfies.Context.fill }

theorem Cslib.Logic.Modal.Satisfies.Context.fill_def {World : Type u_1} {Atom : Type u_2} {φ : Proposition Atom} {c : Context World Atom} : { m := c.m, w := c.w, φ := φ } = c<[φ]

@[instance_reducible]

instance Cslib.Logic.Modal.instLogicalEquivalencePropositionJudgementDefaultEquivWithinUnivModel {Atom : Type u_1} {World : Type u_2} : LogicalEquivalence InferenceSystem.Default (Proposition.EquivWithin Set.univ)

Logical equivalence for Modal Logic K. That is, no assumptions on models are made.

Equations

• Cslib.Logic.Modal.instLogicalEquivalencePropositionJudgementDefaultEquivWithinUnivModel = { toLawfulCongruence := ⋯, eqvFillValid := ⋯ }

theorem Cslib.Logic.Modal.Proposition.axiom_iff_forall_equiv {α : Type u_1} {Atom : Type u_2} (r : α → α → Prop) (φ₁ φ₂ : Proposition Atom) : InferenceSystem.derivation (Axiom r) (HasIff.iff φ₁ φ₂) ↔ ∀ (v : α → Atom → Prop), Congruence.r (Equiv { r := r, v := v }) φ₁ φ₂

Correspondence of equivalence and axiom validity.

theorem Cslib.Logic.Modal.Proposition.diamond_and_equiv_of_preserves {World : Type u_1} {Atom : Type u_2} {m : Model World Atom} [IsTrans World m.r] {φ₁ φ₂ : Proposition Atom} (hd : Relation.Diamond m.r) (h₁ : Relation.Preserves m.r fun (x : World) => ⇓{ m := m, w := x, φ := φ₁ }) (h₂ : Relation.Preserves m.r fun (x : World) => ⇓{ m := m, w := x, φ := φ₂ }) : Congruence.r (Equiv m) (HasDiamond.diamond (HasAnd.and φ₁ φ₂)) (HasAnd.and (HasDiamond.diamond φ₁) (HasDiamond.diamond φ₂))

In a transitive diamond model, possibility distributes over conjunction for propositions whose satisfaction is preserved along accessibility.

theorem Cslib.Logic.Modal.Proposition.diamond_diamond_equiv {World : Type u_1} {Atom : Type u_2} {m : Model World Atom} [Std.Refl m.r] [IsTrans World m.r] (φ : Proposition Atom) : Congruence.r (Equiv m) (HasDiamond.diamond (HasDiamond.diamond φ)) (HasDiamond.diamond φ)

In a reflexive and transitive model, diamond absorbs itself (idempotency).