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), Cslib.Logic.InferenceSystem.derivation Cslib.Logic.InferenceSystem.Default { m := m, w := w, φ := φ₁.iff φ₂ }

def Cslib.Logic.Modal.«term_≡[_]_» : Lean.TrailingParserDescr

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

Equations

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

def Cslib.Logic.Modal.«term_≡_» : Lean.TrailingParserDescr

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

Equations

• Cslib.Logic.Modal.«term_≡_» = Lean.ParserDescr.trailingNode `Cslib.Logic.Modal.«term_≡_» 1022 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≡ ") (Lean.ParserDescr.cat `term 0))

theorem Cslib.Logic.Modal.Proposition.equiv_def {World : Type u_1} {Atom : Type u_2} (S : Set (Model World Atom)) (φ₁ φ₂ : Proposition Atom) : Equiv S φ₁ φ₂ ↔ ∀ m ∈ S, ∀ (w : World), InferenceSystem.derivation InferenceSystem.Default { m := m, w := w, φ := φ₁.iff φ₂ }

theorem Cslib.Logic.Modal.Proposition.equiv_iff {World : Type u_1} {Atom : Type u_2} (S : Set (Model World Atom)) (φ₁ φ₂ : Proposition Atom) : Equiv S φ₁ φ₂ ↔ ∀ m ∈ S, ∀ (w : World), InferenceSystem.derivation InferenceSystem.Default { m := m, w := w, φ := φ₁ } ↔ InferenceSystem.derivation InferenceSystem.Default { 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 : Equiv S φ₁ φ₂) : valid S φ₁ ↔ valid S φ₂

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

@[implicit_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} {Γ : HasContext.Context (Proposition Atom)} : fill Γ φ = Γ<[φ]

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.instCongruencePropositionEquiv {World : Type u_1} {Atom : Type u_2} (S : Set (Model World Atom)) : Congruence (Proposition Atom) (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, φ := φ }

@[implicit_reducible]

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

Equations

• Cslib.Logic.Modal.judgementalContext = { 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<[φ]

@[implicit_reducible]

instance Cslib.Logic.Modal.instLogicalEquivalencePropositionJudgementBundled {Atom : Type u_1} {World : Type u_2} : LogicalEquivalence (Proposition Atom) (Judgement World Atom) Satisfies.Bundled

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

Equations

• Cslib.Logic.Modal.instLogicalEquivalencePropositionJudgementBundled = { eqv := Cslib.Logic.Modal.Proposition.Equiv Set.univ, congruence := ⋯, eqvFillValid := ⋯ }