Semantics of GL

Here we supply the semantics of GL.

structure Lean4GlCoalgebras.Model (α : Type) : Type

Kripke models for GL (note: we add the transitivity and con_wf conditions directly into our definition of a model, i.e. this is not a general definition of a Krike model!)

• V : α → ℕ → Prop

  Auxiliary declaration used in the GL coalgebra development.

• R : α → α → Prop

  Auxiliary declaration used in the GL coalgebra development.

• trans {a b c : α} : self.R a b → self.R b c → self.R a c
• con_wf : WellFounded (Function.swap self.R)

instance Lean4GlCoalgebras.instModelIsIrref {α : Type} (M : Model α) : Std.Irrefl M.R

GL Models are irreflexive.

def Lean4GlCoalgebras.evaluate {α : Type} : Model α × α → Formula → Prop

Standard semantics for Kripke models.

Equations

• Lean4GlCoalgebras.evaluate (fst, snd) Lean4GlCoalgebras.Formula.bottom = False
• Lean4GlCoalgebras.evaluate (fst, snd) Lean4GlCoalgebras.Formula.top = True
• Lean4GlCoalgebras.evaluate (M, w) (at n) = M.V w n
• Lean4GlCoalgebras.evaluate (M, w) (na n) = ¬M.V w n
• Lean4GlCoalgebras.evaluate (M, w) (φ&ψ) = (Lean4GlCoalgebras.evaluate (M, w) φ ∧ Lean4GlCoalgebras.evaluate (M, w) ψ)
• Lean4GlCoalgebras.evaluate (M, w) (φ v ψ) = (Lean4GlCoalgebras.evaluate (M, w) φ ∨ Lean4GlCoalgebras.evaluate (M, w) ψ)
• Lean4GlCoalgebras.evaluate (M, w) (□φ) = ∀ (u : α), M.R w u → Lean4GlCoalgebras.evaluate (M, u) φ
• Lean4GlCoalgebras.evaluate (M, w) (◇φ) = ∃ (u : α), M.R w u ∧ Lean4GlCoalgebras.evaluate (M, u) φ

theorem Lean4GlCoalgebras.evaluate_neg {α : Type} (M : Model α) (u : α) (φ : Formula) : ¬evaluate (M, u) φ ↔ evaluate (M, u) (~φ)

@[simp]

theorem Lean4GlCoalgebras.evaluate_and {α : Type} (M : Model α) (u : α) (φ ψ : Formula) : evaluate (M, u) (φ&ψ) ↔ evaluate (M, u) φ ∧ evaluate (M, u) ψ

theorem Lean4GlCoalgebras.evaluate_imp {α : Type} (M : Model α) (u : α) (φ ψ : Formula) : evaluate (M, u) (~φ v ψ) ↔ evaluate (M, u) φ → evaluate (M, u) ψ

def Lean4GlCoalgebras.evaluateSeq {α : Type} : Model α × α → Sequent → Prop

note: sequent are read disjunctively!

Equations

• Lean4GlCoalgebras.evaluateSeq M_u Γ = ∃ φ ∈ Γ, Lean4GlCoalgebras.evaluate M_u φ

def Lean4GlCoalgebras.evaluateSSeq {α : Type} : Model α × α → SplitSequent → Prop

note: ignores the left/right annotation.

Equations

• Lean4GlCoalgebras.evaluateSSeq M_u Γ = ∃ φ ∈ Γ, Lean4GlCoalgebras.evaluate M_u (Sum.elim id id φ)

@[simp]

theorem Lean4GlCoalgebras.not_evaluateSSeq {α : Type} {M_u : Model α × α} {Γ : SplitSequent} : ¬evaluateSSeq M_u Γ ↔ (∀ (φ : Formula), Sum.inl φ ∈ Γ → ¬evaluate M_u φ) ∧ ∀ (φ : Formula), Sum.inr φ ∈ Γ → ¬evaluate M_u φ

def Lean4GlCoalgebras.Formula.isValid (φ : Formula) : Prop

A formula is valid if it holds at every world in every GL model.

Equations

• (⊨φ) = ∀ (α : Type) (M : Lean4GlCoalgebras.Model α) (u : α), Lean4GlCoalgebras.evaluate (M, u) φ

def Lean4GlCoalgebras.Sequent.isValid (Δ : Sequent) : Prop

A sequent is valid if some formula in it holds at every world in every GL model.

Equations

• (⊨Δ) = ∀ (α : Type) (M : Lean4GlCoalgebras.Model α) (u : α), Lean4GlCoalgebras.evaluateSeq (M, u) Δ

def Lean4GlCoalgebras.SplitSequent.isValid (Δ : SplitSequent) : Prop

A split sequent is valid if some formula in it holds at every world in every GL model.

Equations

• (⊨Δ) = ∀ (α : Type) (M : Lean4GlCoalgebras.Model α) (u : α), Lean4GlCoalgebras.evaluateSSeq (M, u) Δ

def Lean4GlCoalgebras.«term⊨_» : Lean.ParserDescr

Auxiliary declaration used in the GL coalgebra development.

Equations

• Lean4GlCoalgebras.«term⊨_» = Lean.ParserDescr.node `Lean4GlCoalgebras.«term⊨_» 40 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⊨") (Lean.ParserDescr.cat `term 40))

def Lean4GlCoalgebras.«term⊨__1» : Lean.ParserDescr

Auxiliary declaration used in the GL coalgebra development.

Equations

• Lean4GlCoalgebras.«term⊨__1» = Lean.ParserDescr.node `Lean4GlCoalgebras.«term⊨__1» 40 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⊨") (Lean.ParserDescr.cat `term 40))

def Lean4GlCoalgebras.«term⊨__2» : Lean.ParserDescr

Auxiliary declaration used in the GL coalgebra development.

Equations

• Lean4GlCoalgebras.«term⊨__2» = Lean.ParserDescr.node `Lean4GlCoalgebras.«term⊨__2» 40 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⊨") (Lean.ParserDescr.cat `term 40))

def Lean4GlCoalgebras.semEquiv : Formula → Formula → Prop

Two formulas are semantically equivalent if their biconditional is valid.

Equations

• Lean4GlCoalgebras.semEquiv φ ψ = (⊨((~φ v ψ)&~ψ v φ))

def Lean4GlCoalgebras.modelSubstitution {α : Type} (M : Model α) (n : ℕ) (φ : Formula) : Model α

Model construction for substitution lemma.

Equations

• Lean4GlCoalgebras.modelSubstitution M n φ = { V := fun (u : α) (k : ℕ) => if n = k then Lean4GlCoalgebras.evaluate (M, u) φ else M.V u k, R := M.R, trans := ⋯, con_wf := ⋯ }

theorem Lean4GlCoalgebras.substitution_lemma {α : Type} (M : Model α) (u : α) (n : ℕ) (ψ φ : Formula) : evaluate (M, u) (single n ψ φ) ↔ evaluate (modelSubstitution M n ψ, u) φ

Substitution Lemma for modal logic!

theorem Lean4GlCoalgebras.single_preserves_validity (n : ℕ) (φ ψ : Formula) : ⊨φ → ⊨single n ψ φ

Corollary of substitution lemma: If φ valid, then φ[ψ/n] is valid.

theorem Lean4GlCoalgebras.single_preserves_sem_equiv (n : ℕ) (χ φ ψ : Formula) (φ_equiv_ψ : ⊨((~φ v ψ)&~ψ v φ)) : ⊨((~single n χ φ v single n χ ψ)&~single n χ ψ v single n χ φ)

Corollary of substitution lemma: If φ ⟷ ψ valid, then φ[χ/n] ⟷ ψ[χ/n] is valid.