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_reducible]

instance formHasSat : HasSat Formula

Equations

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

@[instance_reducible]

instance setHasSat : HasSat (Finset Formula)

Equations

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

@[instance_reducible]

instance listHasSat : HasSat (List Formula)

Equations

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

theorem sat_congr_of_mem_iff {L L' : List Formula} (h : ∀ (f : Formula), f ∈ L ↔ f ∈ L') : HasSat.satisfiable L ↔ HasSat.satisfiable L'

Satisfiability of a list only depends on which formulas are in it.

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 : Std.Refl semEquiv

theorem semEquiv.symm : Std.Symm semEquiv

theorem semEquiv.trans : IsTrans Formula semEquiv

theorem relEquiv.refl : Std.Refl relEquiv

theorem relEquiv.symm : Std.Symm relEquiv

theorem relEquiv.trans : IsTrans Program relEquiv

class vDash (α β : Type) : Type

• SemImplies : α → β → Prop

@[instance_reducible]

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

Equations

• modelCanSemImplyForm = { SemImplies := evaluatePoint }

@[instance_reducible]

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_reducible]

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_reducible]

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

Equations

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

@[instance_reducible]

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_reducible]

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

Equations

• setCanSemImplySet = { SemImplies := semImpliesLists }

@[instance_reducible]

instance setCanSemImplyForm : vDash (List Formula) Formula

Equations

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

@[instance_reducible]

instance formCanSemImplySet : vDash Formula (List Formula)

Equations

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

@[instance_reducible]

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 deduction (X : List Formula) (ψ φ : Formula) : X ++ [ψ] ⊨ φ ↔ X ⊨ ~(ψ ⋀ ~φ)

The Local Deduction Theorem.

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} : tautology (~(φ ⋀ ~ψ)) ↔ ¬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_singleton {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 relate_steps_iff_relateSeq {W : Type} (M : KripkeModel W) (δ : List Program) (w v : W) : relate M (Program.steps δ) w v ↔ relateSeq M δ w 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.castSucc) (ws.get i.succ)

theorem relate_unions {W : Type} {M : KripkeModel W} (L : List Program) (v u : W) : relate M (Program.unions L) v u ↔ ∃ a ∈ L, relate M a v u

Relating along Program.unions L means relating along one of the programs in L.

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) ⊨ ~''ξ