Semantics (Section 2.2)

Models and Truth

structure PDL.KripkeModel (W : Type) : Type

Kripke Models, also known as Labelled Transition Systems

• val : W → ℕ → Prop

  The truth assignment for atomic propositions at each world.

• Rel : ℕ → W → W → Prop

  The accessibility relation for each atomic program.

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

The syntactic measure used to define formula evaluation and program relations mutually.

Equations

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

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

Truth of a PDL formula at a world in a Kripke model.

Equations

• PDL.evaluate x✝¹ x✝ PDL.Formula.bottom = False
• PDL.evaluate x✝¹ x✝ (PDL.Formula.atom_prop c) = x✝¹.val x✝ c
• PDL.evaluate x✝¹ x✝ φ.neg = ¬PDL.evaluate x✝¹ x✝ φ
• PDL.evaluate x✝¹ x✝ (φ.and ψ) = (PDL.evaluate x✝¹ x✝ φ ∧ PDL.evaluate x✝¹ x✝ ψ)
• PDL.evaluate x✝¹ x✝ (PDL.Formula.box α φ) = ∀ (v : W), PDL.relate x✝¹ α x✝ v → PDL.evaluate x✝¹ v φ

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

The binary relation denoted by a PDL program in a Kripke model.

Equations

• PDL.relate x✝² (PDL.Program.atom_prog c) x✝¹ x✝ = x✝².Rel c x✝¹ x✝
• PDL.relate x✝² (α.sequence β) x✝¹ x✝ = ∃ (y : W), PDL.relate x✝² α x✝¹ y ∧ PDL.relate x✝² β y x✝
• PDL.relate x✝² (α.union β) x✝¹ x✝ = (PDL.relate x✝² α x✝¹ x✝ ∨ PDL.relate x✝² β x✝¹ x✝)
• PDL.relate x✝² α.star x✝¹ x✝ = Relation.ReflTransGen (PDL.relate x✝² α) x✝¹ x✝
• PDL.relate x✝² (PDL.Program.test φ) x✝¹ x✝ = (x✝¹ = x✝ ∧ PDL.evaluate x✝² x✝¹ φ)

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

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

Evaluate a formula at a pointed Kripke model.

Equations

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

def PDL.tautology (φ : Formula) : Prop

Validity of a formula at every world of every Kripke model.

Equations

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

def PDL.contradiction (φ : Formula) : Prop

Falsity of a formula at every world of every Kripke model.

Equations

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

Satisfiability

class PDL.HasSat (α : Type) : Type

Types equipped with a notion of semantic satisfiability.

• satisfiable : α → Prop

  Existence of a semantic model for an object.

@[instance_reducible]

instance PDL.formHasSat : HasSat Formula

Equations

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

@[instance_reducible]

instance PDL.setHasSat : HasSat (Finset Formula)

Equations

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

@[instance_reducible]

instance PDL.listHasSat : HasSat (List Formula)

Equations

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

theorem PDL.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 PDL.semImpliesSets (X Y : Finset Formula) : Prop

Semantic consequence between finite sets of formulas.

Equations

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

def PDL.semImpliesLists (X Y : List Formula) : Prop

Semantic consequence between lists of formulas.

Equations

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

def PDL.semEquiv (φ ψ : Formula) : Prop

Agreement of two formulas at every pointed Kripke model.

Equations

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

def PDL.relEquiv (α β : Program) : Prop

Agreement of two program relations in every Kripke model.

Equations

• PDL.relEquiv α β = ∀ (W : Type) (M : PDL.KripkeModel W) (v w : W), PDL.relate M α v w ↔ PDL.relate M β v w

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

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

theorem PDL.semEquiv.refl : Std.Refl semEquiv

theorem PDL.semEquiv.symm : Std.Symm semEquiv

theorem PDL.semEquiv.trans : IsTrans Formula semEquiv

theorem PDL.relEquiv.refl : Std.Refl relEquiv

theorem PDL.relEquiv.symm : Std.Symm relEquiv

theorem PDL.relEquiv.trans : IsTrans Program relEquiv

class PDL.vDash (α β : Type) : Type

An overloaded semantic satisfaction or consequence relation.

• SemImplies : α → β → Prop

  The semantic relation for the two specified types.

@[instance_reducible]

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

Equations

• PDL.modelCanSemImplyForm = { SemImplies := PDL.evaluatePoint }

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

• PDL.setCanSemImplySet = { SemImplies := PDL.semImpliesLists }

@[instance_reducible]

instance PDL.setCanSemImplyForm : vDash (List Formula) Formula

Equations

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

@[instance_reducible]

instance PDL.formCanSemImplySet : vDash Formula (List Formula)

Equations

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

@[instance_reducible]

instance PDL.formCanSemImplyForm : vDash Formula Formula

Equations

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

def PDL.«term_⊨_» : Lean.TrailingParserDescr

Semantic satisfaction or consequence.

Equations

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

def PDL.«term_≡_» : Lean.TrailingParserDescr

Semantic equivalence of formulas.

Equations

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

def PDL.«term_≡ᵣ_» : Lean.TrailingParserDescr

Semantic equivalence of program relations.

Equations

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

def PDL.«term_⊭_» : Lean.TrailingParserDescr

Failure of semantic satisfaction or consequence.

Equations

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

@[simp]

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

@[simp]

theorem PDL.vDashSingleton_iff_vDash_formula {W : Type} {M : KripkeModel W} {w : W} (φ : Formula) : vDash.SemImplies (M, w) [φ] ↔ evaluate M w φ

theorem PDL.forms_to_lists {φ ψ : Formula} : vDash.SemImplies φ ψ → vDash.SemImplies [φ] [ψ]

theorem PDL.deduction (X : List Formula) (ψ φ : Formula) : vDash.SemImplies (X ++ [ψ]) φ ↔ vDash.SemImplies X (ψ.and φ.neg).neg

The Local Deduction Theorem.

theorem PDL.notSat_iff_semImplies (X : List Formula) (φ : Formula) : ¬HasSat.satisfiable (X ∪ [φ.neg]) ↔ vDash.SemImplies X [φ]

theorem PDL.equivSat {W : Type} (φ ψ : Formula) {M : KripkeModel W} {w : W} : semEquiv φ ψ → vDash.SemImplies (M, w) φ → vDash.SemImplies (M, w) ψ

theorem PDL.equiv_iff (φ ψ : Formula) (φ_eq_ψ : semEquiv φ ψ) {W : Type} {M : KripkeModel W} {w : W} : vDash.SemImplies (M, w) φ ↔ vDash.SemImplies (M, w) ψ

theorem PDL.tautImp_iff_comboNotUnsat {φ ψ : Formula} : tautology (φ.and ψ.neg).neg ↔ ¬HasSat.satisfiable [φ, ψ.neg]

theorem PDL.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 PDL.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 PDL.relateSeq {W : Type} (M : KripkeModel W) (δ : List Program) (w v : W) : Prop

Relational composition of a list of programs, with equality for the empty list.

Equations

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

@[simp]

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

@[simp]

theorem PDL.relateSeq_singleton {W : Type} {M : KripkeModel W} {α : Program} {w v : W} : relateSeq M [α] w v ↔ relate M α w v

theorem PDL.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 PDL.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 PDL.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 PDL.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 PDL.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 PDL.evalBoxes {W✝ : Type} {M : KripkeModel W✝} {w : W✝} (δ : List Program) (φ : Formula) : evaluate M w (Formula.boxes δ φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ

@[simp]

theorem PDL.evaluate_unload_box {W✝ : Type} {M : KripkeModel W✝} {w : W✝} {α : Program} {af : AnyFormula} : evaluate M w (LoadFormula.box α af).unload ↔ ∀ (v : W✝), relate M α w v → vDash.SemImplies (M, v) af

theorem PDL.truthImply_then_satImply (X Y : List Formula) : vDash.SemImplies X Y → HasSat.satisfiable X → HasSat.satisfiable Y

theorem PDL.stepToStar {φ : Formula} {α : Program} {ψ : Formula} : vDash.SemImplies φ ((Formula.box α φ).and ψ) → vDash.SemImplies φ (Formula.box α.star ψ)

Semantic induction rule for the Kleene star operator.

theorem PDL.SemImplyAnyNegFormula_loadBoxes_iff {W : Type} {w : W} {δ : List Program} {M : KripkeModel W} {ξ : AnyFormula} : vDash.SemImplies (M, w) (AnyNegFormula.neg (AnyFormula.loadBoxes δ ξ)) ↔ ∃ (v : W), relateSeq M δ w v ∧ vDash.SemImplies (M, v) (AnyNegFormula.neg ξ)