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} {τ : PFunctor.{u_2, u_3}} {Atom : Type u_4} (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} {τ✝ : PFunctor.{u_2, u_3}} {Atom✝ : Type u_4} {m : Model World✝ τ✝ Atom✝} : Congruence (Proposition.Equiv m)

Equations

• Cslib.Logic.Modal.instCongruencePropositionEquiv = { }

theorem Cslib.Logic.Modal.Proposition.equiv_def {World : Type u_1} {τ : PFunctor.{u_2, u_3}} {Atom : Type u_4} (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} {τ : PFunctor.{u_2, u_3}} {Atom : Type u_4} (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} {τ : PFunctor.{u_2, u_3}} {Atom : Type u_4} {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) (τ : PFunctor.{u_3, u_4}) (Atom : Type u_2) : Type (max (max (max u_4 u_3) 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} {τ : PFunctor.{u_2, u_3}} {Atom : Type u_4} (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} {τ✝ : PFunctor.{u_2, u_3}} {Atom✝ : Type u_4} {S : ModelClass World✝ τ✝ Atom✝} : Congruence (Proposition.EquivWithin S)

Equations

• Cslib.Logic.Modal.instCongruencePropositionEquivWithin = { }

@[reducible, inline]

abbrev Cslib.Logic.Modal.Proposition.UEquiv {τ : PFunctor.{u_2, u_3}} {Atom : Type u_4} {World : Type u_1} (φ₁ φ₂ : Proposition τ Atom) : Prop

Universal logical equivalence: φ₁ and φ₂ are equivalent in the class of all models.

Equations

• φ₁.UEquiv φ₂ = Cslib.Logic.Modal.Proposition.EquivWithin Set.univ φ₁ φ₂

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

theorem Cslib.Logic.Modal.Proposition.equivWithin_iff_forall_iff {World✝ : Type u_1} {τ✝ : PFunctor.{u_2, u_3}} {Atom✝ : Type u_4} {S : ModelClass World✝ τ✝ Atom✝} {φ₁ φ₂ : Proposition τ✝ Atom✝} : Congruence.r (EquivWithin S) φ₁ φ₂ ↔ ∀ m ∈ S, Congruence.r (Equiv m) φ₁ φ₂

theorem Cslib.Logic.Modal.Proposition.equiv_of_EquivWithin {World : Type u_1} {τ : PFunctor.{u_2, u_3}} {Atom : Type u_4} {φ₁ φ₂ : 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} {τ : PFunctor.{u_2, u_3}} {Atom : Type u_4} (S : ModelClass World τ Atom) (φ₁ φ₂ : Proposition τ Atom) (h : Congruence.r (EquivWithin S) φ₁ φ₂) : valid S φ₁ ↔ valid S φ₂

Logical equivalence preserves validity.

@[reducible, inline]

abbrev Cslib.Logic.Modal.PropositionMap.Without (τ : PFunctor.{u_2, u_3}) (Atom : Type u_1) (op : τ.A) (i : τ.B op) : Type (max (max u_3 u_2) u_1)

A proposition map missing a particular case (index).

Equations

• Cslib.Logic.Modal.PropositionMap.Without τ Atom op i = ({ j : τ.B op // j ≠ i } → Cslib.Logic.Modal.Proposition τ Atom)

inductive Cslib.Logic.Modal.Proposition.Context (τ : PFunctor.{u_1, u_2}) (Atom : Type u) : Type (max (max u u_1) u_2)

Propositional contexts.

• hole {τ : PFunctor.{u_1, u_2}} {Atom : Type u} : Context τ Atom
• not {τ : PFunctor.{u_1, u_2}} {Atom : Type u} (c : Context τ Atom) : Context τ Atom
• andL {τ : PFunctor.{u_1, u_2}} {Atom : Type u} (c : Context τ Atom) (φ : Proposition τ Atom) : Context τ Atom
• andR {τ : PFunctor.{u_1, u_2}} {Atom : Type u} (φ : Proposition τ Atom) (c : Context τ Atom) : Context τ Atom
• triangle {τ : PFunctor.{u_1, u_2}} {Atom : Type u} (op : τ.A) (i : τ.B op) (c : Context τ Atom) (φs : PropositionMap.Without τ Atom op i) : Context τ Atom

def Cslib.Logic.Modal.Proposition.Context.fill {τ : PFunctor.{u_2, u_3}} [τ.DecidableEqChildren] {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 φ)
• (Cslib.Logic.Modal.Proposition.Context.triangle op i c_2 φs).fill φ = Cslib.Logic.Modal.Proposition.triangle op fun (j : τ.B op) => if h : j = i then c_2.fill φ else φs ⟨j, h⟩

@[instance_reducible]

instance Cslib.Logic.Modal.instHasContextPropositionOfDecidableEqChildren {τ : PFunctor.{u_2, u_3}} [τ.DecidableEqChildren] {Atom : Type u_1} : HasContext (Proposition τ Atom)

Equations

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

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

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

Logical equivalence is an equivalence relation.

instance Cslib.Logic.Modal.instIsEquivPropositionEquivWithin {τ : PFunctor.{u_1, u_2}} {World : Type u_3} {Atom : Type u_4} (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_2} {τ : PFunctor.{u_3, u_4}} [τ.DecidableEqChildren] {Atom : Type u_1} (m : Model World τ Atom) : LawfulCongruence (Proposition.Equiv m)

Logical equivalence is a congruence.

instance Cslib.Logic.Modal.instLawfulCongruencePropositionEquivWithin {World : Type u_2} {τ : PFunctor.{u_3, u_4}} [τ.DecidableEqChildren] {Atom : Type u_1} (S : ModelClass World τ Atom) : LawfulCongruence (Proposition.EquivWithin S)

Logical equivalence within a class is a congruence.

structure Cslib.Logic.Modal.Judgement.Context (World : Type u_1) (τ : PFunctor.{u_3, u_4}) (Atom : Type u_2) : Type (max (max (max u_1 u_2) u_3) u_4)

Judgemental contexts.

• m : Model World τ Atom

  The model to consider.

• w : World

  The world to check propositions against.

def Cslib.Logic.Modal.Judgement.Context.fill {World : Type u_1} {τ : PFunctor.{u_2, u_3}} {Atom : Type u_4} (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} {τ : PFunctor.{u_3, u_4}} {Atom : Type u_2} : HasHContext (Judgement World τ Atom) (Proposition τ Atom)

Equations

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

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

@[instance_reducible]

instance Cslib.Logic.Modal.instLogicalEquivalencePropositionJudgementDefaultEquivWithinUnivModel {Atom : Type u_1} {World : Type u_2} {τ : PFunctor.{u_3, u_4}} [τ.DecidableEqChildren] : 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 {World : Type u_1} {τ : PFunctor.{u_2, u_3}} {Atom : Type u_4} (f : Frame World τ) (φ₁ φ₂ : Proposition τ Atom) : InferenceSystem.derivation (Axiom f) (HasIff.iff φ₁ φ₂) ↔ ∀ (v : World → Atom → Prop), Congruence.r (Equiv { toFrame := f, v := v }) φ₁ φ₂

Correspondence of equivalence and axiom validity.

theorem Cslib.Logic.Modal.Proposition.equiv_of_axiom {World : Type u_1} {τ : PFunctor.{u_2, u_3}} {Atom : Type u_4} {f : Frame World τ} {φ₁ φ₂ : Proposition τ Atom} (h : InferenceSystem.derivation (Axiom f) (HasIff.iff φ₁ φ₂)) (v : World → Atom → Prop) : Congruence.r (Equiv { toFrame := f, v := v }) φ₁ φ₂

A frame-valid bi-implication induces logical equivalence in every model over that frame.

theorem Cslib.Logic.Modal.Proposition.axiom_iff_equivWithin_modelsOfFrame {World : Type u_1} {τ : PFunctor.{u_2, u_3}} {Atom : Type u_4} (f : Frame World τ) (φ₁ φ₂ : Proposition τ Atom) : InferenceSystem.derivation (Axiom f) (HasIff.iff φ₁ φ₂) ↔ Congruence.r (EquivWithin (modelsOfFrame f)) φ₁ φ₂

A bi-implication is an axiom of f iff its sides are equivalent in every model over f.

theorem Cslib.Logic.Modal.Proposition.dual_equiv {τ : PFunctor.{u_1, u_2}} {op : τ.A} {Atom : Type u_3} {World : Type u_4} (φs : PropositionMap τ op Atom) : Congruence.r UEquiv (HasTriangle.triangle op φs) (HasNot.not (HasNabla.nabla op (HasNot.not φs)))

Triangle and the negation of the dual nabla are universally logically equivalent.