Semantics (Section 2.2)

Models and Truth

structure KripkeModel (W : Type) : Type

Kripke Models, also known as Labelled Transition Systems

• val : W → ℕ → Prop
• Rel : ℕ → W → W → Prop

def complexityOfQuery {W : Type} : (_ : KripkeModel W) ×' (_ : W) ×' Formula ⊕' (_ : KripkeModel W) ×' (_ : Program) ×' (_ : W) ×' W → ℕ

Equations

• complexityOfQuery (PSum.inl val) = lengthOfFormula val.snd.snd
• complexityOfQuery (PSum.inr val) = lengthOfProgram val.snd.fst

def evaluate {W : Type} : KripkeModel W → W → Formula → Prop

Equations

• evaluate x✝¹ x✝ Formula.bottom = False
• evaluate x✝¹ x✝ (·c) = x✝¹.val x✝ c
• evaluate x✝¹ x✝ (~φ) = ¬evaluate x✝¹ x✝ φ
• evaluate x✝¹ x✝ (φ⋀ψ) = (evaluate x✝¹ x✝ φ ∧ evaluate x✝¹ x✝ ψ)
• evaluate x✝¹ x✝ (⌈α⌉φ) = ∀ (v : W), relate x✝¹ α x✝ v → evaluate x✝¹ v φ

def relate {W : Type} : KripkeModel W → Program → W → W → Prop

Equations

• relate x✝² (·c) x✝¹ x✝ = x✝².Rel c x✝¹ x✝
• relate x✝² (α;'β) x✝¹ x✝ = ∃ (y : W), relate x✝² α x✝¹ y ∧ relate x✝² β y x✝
• relate x✝² (α⋓β) x✝¹ x✝ = (relate x✝² α x✝¹ x✝ ∨ relate x✝² β x✝¹ x✝)
• relate x✝² (∗α) x✝¹ x✝ = Relation.ReflTransGen (relate x✝² α) x✝¹ x✝
• relate x✝² (?'φ) x✝¹ x✝ = (x✝¹ = x✝ ∧ evaluate x✝² x✝¹ φ)

@[simp]

theorem evalDis {W : Type} {M : KripkeModel W} {f g : Formula} {w : W} : evaluate M w (f⋁g) ↔ evaluate M w f ∨ evaluate M w g

def evaluatePoint {W : Type} : KripkeModel W × W → Formula → Prop

Equations

• evaluatePoint (M, w) x✝ = evaluate M w x✝

def tautology (φ : Formula) : Prop

Equations

• tautology φ = ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w φ

def contradiction (φ : Formula) : Prop

Equations

• contradiction φ = ∀ (W : Type) (M : KripkeModel W) (w : W), ¬evaluate M w φ

Satisfiability

class HasSat (α : Type) : Type

• satisfiable : α → Prop

instance formHasSat : HasSat Formula

Equations

• formHasSat = { satisfiable := fun (ϕ : Formula) => ∃ (W : Type) (M : KripkeModel W) (w : W), evaluate M w ϕ }

instance setHasSat : HasSat (Finset Formula)

Equations

• setHasSat = { satisfiable := fun (X : Finset Formula) => ∃ (W : Type) (M : KripkeModel W) (w : W), ∀ φ ∈ X, evaluate M w φ }

instance listHasSat : HasSat (List Formula)

Equations

• listHasSat = { satisfiable := fun (X : List Formula) => ∃ (W : Type) (M : KripkeModel W) (w : W), ∀ φ ∈ X, evaluate M w φ }

Semantic implication and vDash notation

def semImpliesSets (X Y : Finset Formula) : Prop

Equations

• semImpliesSets X Y = ∀ (W : Type) (M : KripkeModel W) (w : W), (∀ φ ∈ X, evaluate M w φ) → ∀ ψ ∈ Y, evaluate M w ψ

def semImpliesLists (X Y : List Formula) : Prop

Equations

• semImpliesLists X Y = ∀ (W : Type) (M : KripkeModel W) (w : W), (∀ φ ∈ X, evaluate M w φ) → ∀ ψ ∈ Y, evaluate M w ψ

def semEquiv (φ ψ : Formula) : Prop

Equations

• (φ≡ψ) = ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w φ ↔ evaluate M w ψ

def relEquiv (α β : Program) : Prop

Equations

• (α≡ᵣβ) = ∀ (W : Type) (M : KripkeModel W) (v w : W), relate M α v w ↔ relate M β v w

theorem notsatisfnotThenTaut (φ : Formula) : ¬HasSat.satisfiable (~φ) → tautology φ

theorem subsetSat {W : Type} {M : KripkeModel W} {w : W} {X Y : List Formula} : (∀ φ ∈ X, evaluate M w φ) → Y ⊆ X → ∀ φ ∈ Y, evaluate M w φ

theorem semEquiv.refl : Reflexive semEquiv

theorem semEquiv.symm : Symmetric semEquiv

theorem semEquiv.trans : Transitive semEquiv

class vDash (α β : Type) : Type

• SemImplies : α → β → Prop

instance modelCanSemImplyForm {W : Type} : vDash (KripkeModel W × W) Formula

Equations

• modelCanSemImplyForm = { SemImplies := evaluatePoint }

instance modelCanSemImplySet {W : Type} : vDash (KripkeModel W × W) (List Formula)

Equations

• modelCanSemImplySet = { SemImplies := fun (x : KripkeModel W × W) (fs : List Formula) => match x with | (M, w) => ∀ f ∈ fs, evaluate M w f }

instance modelCanSemImplyList {W : Type} : vDash (KripkeModel W × W) (List Formula)

Equations

• modelCanSemImplyList = { SemImplies := fun (x : KripkeModel W × W) (fs : List Formula) => match x with | (M, w) => ∀ f ∈ fs, evaluate M w f }

instance modelCanSemImplyAnyFormula {W : Type} : vDash (KripkeModel W × W) AnyFormula

Equations

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

instance modelCanSemImplyAnyNegFormula {W : Type} : vDash (KripkeModel W × W) AnyNegFormula

Equations

• modelCanSemImplyAnyNegFormula = { SemImplies := fun (x : KripkeModel W × W) (x_1 : AnyNegFormula) => match x with | (M, w) => match x_1 with | ~''ξ => ¬(M, w)⊨ξ }

instance setCanSemImplySet : vDash (List Formula) (List Formula)

Equations

• setCanSemImplySet = { SemImplies := semImpliesLists }

instance setCanSemImplyForm : vDash (List Formula) Formula

Equations

• setCanSemImplyForm = { SemImplies := fun (X : List Formula) (ψ : Formula) => semImpliesLists X [ψ] }

instance formCanSemImplySet : vDash Formula (List Formula)

Equations

• formCanSemImplySet = { SemImplies := fun (φ : Formula) (X : List Formula) => semImpliesLists [φ] X }

instance formCanSemImplyForm : vDash Formula Formula

Equations

• formCanSemImplyForm = { SemImplies := fun (φ ψ : Formula) => semImpliesLists [φ] [ψ] }

def «term_⊨_» : Lean.TrailingParserDescr

Equations

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

def «term_≡_» : Lean.TrailingParserDescr

Equations

• «term_≡_» = Lean.ParserDescr.trailingNode `«term_≡_» 40 40 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "≡") (Lean.ParserDescr.cat `term 41))

def «term_≡ᵣ_» : Lean.TrailingParserDescr

Equations

• «term_≡ᵣ_» = Lean.ParserDescr.trailingNode `«term_≡ᵣ_» 40 40 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "≡ᵣ") (Lean.ParserDescr.cat `term 41))

def «term_⊭_» : Lean.TrailingParserDescr

Equations

• «term_⊭_» = Lean.ParserDescr.trailingNode `«term_⊭_» 40 40 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⊭") (Lean.ParserDescr.cat `term 41))

@[simp]

theorem singletonSat_iff_sat (φ : Formula) : HasSat.satisfiable {φ} ↔ HasSat.satisfiable φ

@[simp]

theorem vDashSingleton_iff_vDash_formula {W : Type} {M : KripkeModel W} {w : W} (φ : Formula) : (M, w)⊨[φ] ↔ evaluate M w φ

theorem forms_to_lists {φ ψ : Formula} : φ⊨ψ → [φ]⊨[ψ]

theorem notSat_iff_semImplies (X : List Formula) (φ : Formula) : ¬HasSat.satisfiable (X ∪ [~φ]) ↔ X⊨[φ]

theorem equivSat {W : Type} (φ ψ : Formula) {M : KripkeModel W} {w : W} : φ≡ψ → (M, w)⊨φ → (M, w)⊨ψ

theorem equiv_iff (φ ψ : Formula) (φ_eq_ψ : φ≡ψ) {W : Type} {M : KripkeModel W} {w : W} : (M, w)⊨φ ↔ (M, w)⊨ψ

theorem tautImp_iff_comboNotUnsat {φ ψ : Formula} : φ⊨ψ ↔ ¬HasSat.satisfiable [φ, ~ψ]

theorem relate_steps_append {W✝ : Type} {M : KripkeModel W✝} {as bs : List Program} (x z : W✝) : relate M (Program.steps (as ++ bs)) x z ↔ ∃ (y : W✝), relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z

theorem rel_steps_last {W✝ : Type} {M : KripkeModel W✝} {a : Program} {as : List Program} (v w : W✝) : relate M (Program.steps (as ++ [a])) v w ↔ ∃ (mid : W✝), relate M (Program.steps as) v mid ∧ relate M a mid w

def relateSeq {W : Type} (M : KripkeModel W) (δ : List Program) (w v : W) : Prop

Equations

• relateSeq M [] w v = (w = v)
• relateSeq M (α :: as) w v = ∃ (u : W), relate M α w u ∧ relateSeq M as u v

@[simp]

theorem relateSeq_nil {W : Type} (M : KripkeModel W) (w v : W) : relateSeq M [] w v ↔ w = v

@[simp]

theorem relateSeq_singelton {W : Type} (M : KripkeModel W) (α : Program) (w v : W) : relateSeq M [α] w v ↔ relate M α w v

theorem relateSeq_cons {W : Type} (M : KripkeModel W) (d : Program) (δ : List Program) (w v : W) : relateSeq M (d :: δ) w v ↔ ∃ (u : W), relate M d w u ∧ relateSeq M δ u v

theorem relateSeq_append {W : Type} (M : KripkeModel W) (l1 l2 : List Program) (w v : W) : relateSeq M (l1 ++ l2) w v ↔ ∃ (u : W), relateSeq M l1 w u ∧ relateSeq M l2 u v

theorem relateSeq_iff_exists_Vector {W : Type} (M : KripkeModel W) (δ : List Program) (w v : W) : relateSeq M δ w v ↔ ∃ (ws : List.Vector W δ.length.succ), w = ws.head ∧ v = ws.last ∧ ∀ (i : Fin δ.length), relate M (δ.get i) (ws.get ↑↑i) (ws.get i.succ)

theorem evalBoxes {W✝ : Type} {M : KripkeModel W✝} {w : W✝} (δ : List Program) (φ : Formula) : evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ

@[simp]

theorem evaluate_unload_box {W✝ : Type} {M : KripkeModel W✝} {w : W✝} {α : Program} {af : AnyFormula} : evaluate M w (⌊α⌋af).unload ↔ ∀ (v : W✝), relate M α w v → (M, v)⊨af

theorem truthImply_then_satImply (X Y : List Formula) : X⊨Y → HasSat.satisfiable X → HasSat.satisfiable Y

theorem stepToStar {φ : Formula} {α : Program} {ψ : Formula} : φ⊨(⌈α⌉φ)⋀ψ → φ⊨⌈∗α⌉ψ

Semantic induction rule for the Kleene star operator.

theorem SemImplyAnyNegFormula_loadBoxes_iff {W : Type} {w : W} {δ : List Program} {M : KripkeModel W} {ξ : AnyFormula} : (M, w)⊨~''(AnyFormula.loadBoxes δ ξ) ↔ ∃ (v : W), relateSeq M δ w v ∧ (M, v)⊨~''ξ