Semantics of GL

Here we supply the semantics of GL.

structure 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
• R : α → α → Prop
• trans : Transitive self.R
• con_wf : WellFounded (Function.swap self.R)

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

GL Models are irreflexive.

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

Standard semantics for Kripke models.

Equations

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

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

@[simp]

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

@[simp]

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

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

note: sequent are read disjunctively!

Equations

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

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

note: ignores the left/right annotation.

Equations

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

def Formula.isValid (φ : Formula) : Prop

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

Equations

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

def Sequent.isValid (Δ : Sequent) : Prop

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

Equations

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

def 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 : Model α) (u : α), evaluateSSeq (M, u) Δ

def «term⊨_» : Lean.ParserDescr

Equations

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

def «term⊨__1» : Lean.ParserDescr

Equations

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

def «term⊨__2» : Lean.ParserDescr

Equations

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

def semEquiv : Formula → Formula → Prop

Two formulas are semantically equivalent if their biconditional is valid.

Equations

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

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

Model construction for substitution lemma.

Equations

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

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

Substitution Lemma for modal logic!

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

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

theorem 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.