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} (S : Set (Model World Atom)) (φ₁ φ₂ : Proposition Atom) : Prop

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

Equations

• Cslib.Logic.Modal.Proposition.Equiv S φ₁ φ₂ = ∀ m ∈ S, ∀ (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} {S : Set (Model World✝ Atom✝)} : Congruence (Proposition.Equiv S)

Equations

• Cslib.Logic.Modal.instCongruencePropositionEquiv = { }

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

theorem Cslib.Logic.Modal.Proposition.equiv_forall_der {World : Type u_1} {Atom : Type u_2} (S : Set (Model World Atom)) (φ₁ φ₂ : Proposition Atom) (h : Congruence.r (Equiv S) φ₁ φ₂) (m : Model World Atom) : m ∈ S → ∀ (w : World), ⇓{ m := m, w := w, φ := HasIff.iff φ₁ φ₂ }

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

theorem Cslib.Logic.Modal.Proposition.equiv_iff {World : Type u_1} {Atom : Type u_2} (S : Set (Model World Atom)) (φ₁ φ₂ : Proposition Atom) (h : Congruence.r (Equiv S) φ₁ φ₂) (m : Model World Atom) (hm : m ∈ S) (w : World) : ⇓{ m := m, w := w, φ := φ₁ } ↔ ⇓{ m := m, w := w, φ := φ₂ }

theorem Cslib.Logic.Modal.Proposition.equiv_valid {World : Type u_1} {Atom : Type u_2} (S : Set (Model World Atom)) (φ₁ φ₂ : Proposition Atom) (h : Congruence.r (Equiv 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} (S : Set (Model World Atom)) : IsEquiv (Proposition Atom) (Proposition.Equiv S)

Logical equivalence is an equivalence relation.

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

Logical equivalence 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.instLogicalEquivalencePropositionJudgementDefaultEquivUnivModel {Atom : Type u_1} {World : Type u_2} : LogicalEquivalence InferenceSystem.Default (Proposition.Equiv Set.univ)

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

Equations

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