Model Graphs (Section 7.1)

Definition of Model Graphs

def saturated : Finset Formula → Prop

A set of formulas is saturated if it is closed under: removing double negations, splitting (negated) conjunctions, unfolding boxes using any test profile, and unfolding diamonds using H.

Equations

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

def Q {W : Finset (Finset Formula)} (R : ℕ → { x : Finset Formula // x ∈ W } → { x : Finset Formula // x ∈ W } → Prop) : Program → { x : Finset Formula // x ∈ W } → { x : Finset Formula // x ∈ W } → Prop

Q α

Equations

• Q R (·c) = R c
• Q R (?'τ) = fun (v w : { x : Finset Formula // x ∈ W }) => v = w ∧ τ ∈ ↑v
• Q R (α⋓β) = fun (v w : { x : Finset Formula // x ∈ W }) => Q R α v w ∨ Q R β v w
• Q R (α;'β) = Relation.Comp (Q R α) (Q R β)
• Q R (∗α) = Relation.ReflTransGen (Q R α)

def ModelGraph (W : Finset (Finset Formula)) : Type

A model graph is a Kripke model using sets of formulas as states and fulfilling conditions (i) to (iv). See MB Def 19, page 31. Note: In (ii) MB only has →. We follow BRV Def 4.18 and 4.84. Note: In (iii) "a" is atomic, but in iv "α" is any program.

Equations

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

Truth Lemma

theorem get_eq_getzip {α : Type u_1} {l : List α} {α✝ : Type u_2} {x : α✝} {δ : List α✝} {X Y : α} {i : Fin (l ++ [Y]).length} {h : ↑i < ((x, X) :: δ.zip (l ++ [Y])).length} : (X :: (l ++ [Y])).get i.castSucc = (((x, X) :: δ.zip (l ++ [Y])).get ⟨↑i, h⟩).2

theorem loadClaimHelper {Worlds : Finset (Finset Formula)} {MG : ModelGraph Worlds} {X Y : { x : Finset Formula // x ∈ Worlds }} {δ : List Program} {φ : Formula} {l : List { x : Finset Formula // x ∈ Worlds }} (length_def : l.length + 1 = δ.length) (δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X) (lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))) (IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x : Finset Formula // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y') (i : Fin (X :: l ++ [Y]).length) : (⌈⌈List.drop (↑i) δ⌉⌉φ) ∈ ↑((X :: l ++ [Y]).get i)

@[irreducible]

theorem Q_then_relate {Worlds : Finset (Finset Formula)} (MG : ModelGraph Worlds) (α : Program) (X Y : { x : Finset Formula // x ∈ Worlds }) : Q (↑MG).Rel α X Y → relate (↑MG) α X Y

C3 in notes

@[irreducible]

theorem loadedTruthLemma {Worlds : Finset (Finset Formula)} (MG : ModelGraph Worlds) (X : { x : Finset Formula // x ∈ Worlds }) (P : Formula) : (P ∈ ↑X → evaluate (↑MG) X P) ∧ ((~P) ∈ ↑X → ¬evaluate (↑MG) X P)

C1 and C2 in notes

@[irreducible]

theorem loadedTruthLemmaProg {Worlds : Finset (Finset Formula)} (MG : ModelGraph Worlds) (α : Program) (X : { x : Finset Formula // x ∈ Worlds }) (φ : Formula) : (⌈α⌉φ) ∈ ↑X → ∀ (Y : { x : Finset Formula // x ∈ Worlds }), relate (↑MG) α X Y → φ ∈ ↑Y

C4 in notes

theorem truthLemma {Worlds : Finset (Finset Formula)} (MG : ModelGraph Worlds) (X : { x : Finset Formula // x ∈ Worlds }) (P : Formula) : P ∈ ↑X → evaluate (↑MG) X P

Additional Q relations for the completeness proof

def Qtests {W : Finset (Finset Formula)} (R : ℕ → { x : Finset Formula // x ∈ W } → { x : Finset Formula // x ∈ W } → Prop) (F : List Formula) : { x : Finset Formula // x ∈ W } → { x : Finset Formula // x ∈ W } → Prop

Q_F - for a list F of tests (instead of a set in the notes).

Equations

• Qtests R F x✝¹ x✝ = ((x✝¹ == x✝) = true ∧ ∀ τ ∈ F, Q R (?'τ) x✝¹ x✝)

def Qsteps {W : Finset (Finset Formula)} (R : ℕ → { x : Finset Formula // x ∈ W } → { x : Finset Formula // x ∈ W } → Prop) : List Program → { x : Finset Formula // x ∈ W } → { x : Finset Formula // x ∈ W } → Prop

Q_δ for a list δ of programs.

Equations

• Qsteps R [] x✝¹ x✝ = ((x✝¹ == x✝) = true)
• Qsteps R (α :: δ) x✝¹ x✝ = Relation.Comp (Q R α) (Qsteps R δ) x✝¹ x✝

@[simp]

theorem Qsteps_single {a✝ : Finset (Finset Formula)} {R : ℕ → { x : Finset Formula // x ∈ a✝ } → { x : Finset Formula // x ∈ a✝ } → Prop} {α : Program} {v w : { x : Finset Formula // x ∈ a✝ }} : Qsteps R [α] v w ↔ Q R α v w

theorem Qsteps_append {a✝ : Finset (Finset Formula)} {R : ℕ → { x : Finset Formula // x ∈ a✝ } → { x : Finset Formula // x ∈ a✝ } → Prop} {δ1 δ2 : List Program} {v w : { x : Finset Formula // x ∈ a✝ }} : Qsteps R (δ1 ++ δ2) v w ↔ ∃ (u : { x : Finset Formula // x ∈ a✝ }), Qsteps R δ1 v u ∧ Qsteps R δ2 u w

def Qcombo {W : Finset (Finset Formula)} (R : ℕ → { x : Finset Formula // x ∈ W } → { x : Finset Formula // x ∈ W } → Prop) (F : List Formula) (δ : List Program) : { x : Finset Formula // x ∈ W } → { x : Finset Formula // x ∈ W } → Prop

Q_Fδ for a list of tests F and a list or programs δ.

Equations

• Qcombo R F δ = Relation.Comp (Qtests R F) (Qsteps R δ)

theorem cp3a {W : Finset (Finset Formula)} (R : ℕ → { x : Finset Formula // x ∈ W } → { x : Finset Formula // x ∈ W } → Prop) (α : Program) (Fδ : List Formula × List Program) : Fδ ∈ H α → ∀ (v w : { x : Finset Formula // x ∈ W }), Qcombo R Fδ.1 Fδ.2 v w → Q R α v w

Q_Fδ v w implies Q v w.