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. Part of Def 6.2

Equations

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

def locallyConsistent (X : Finset Formula) : Prop

A set of formulas is lcoally consistent iff it does not contain ⊥ and for all atoms p ∈ X we do not have ~p ∈ X. Part of Def 6.2

Equations

• locallyConsistent X = (⊥ ∉ X.val ∧ ∀ (pp : ℕ), ·pp ∈ X.val → ~·pp ∉ X.val)

def Modelgraphs.Q {W : Finset (Finset Formula)} (R : ℕ → ↥W → ↥W → Prop) : Program → ↥W → ↥W → Prop

Q α

Equations

• Modelgraphs.Q R (·c) = R c
• Modelgraphs.Q R (?'τ) = fun (v w : ↥W) => v = w ∧ τ ∈ ↑v
• Modelgraphs.Q R (α⋓β) = fun (v w : ↥W) => Modelgraphs.Q R α v w ∨ Modelgraphs.Q R β v w
• Modelgraphs.Q R (α;'β) = Relation.Comp (Modelgraphs.Q R α) (Modelgraphs.Q R β)
• Modelgraphs.Q R (∗α) = Relation.ReflTransGen (Modelgraphs.Q R α)

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

Definition 6.4. A model graph is a Kripke model over sets of formulas as states fulfilling the conditions (a) to (b). See also [Bor88] Def 19 on page 31 where (a)-(b) are named (i)-(iv). Note: In MB item (b) aka (ii) only has →. We use ↔ similar to [BdRV01] Def 4.18 and 4.84. Note: In item (c) a is atomic, but in item (d) α 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]))[↑i].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.IsChain (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 : ↥Worlds) : Modelgraphs.Q (↑MG).Rel α X Y → relate (↑MG) α X Y

C3 in notes. Originally MB Lemma 9, page 32, stronger version for induction loading. Now also using Q relation to overwrite tests.

@[irreducible]

theorem loadedTruthLemma {Worlds : Finset (Finset Formula)} (MG : ModelGraph Worlds) (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 : ↥Worlds) (φ : Formula) : (⌈α⌉φ) ∈ ↑X → ∀ (Y : ↥Worlds), relate (↑MG) α X Y → φ ∈ ↑Y

C4 in notes

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

Additional Q relations for the completeness proof

def Qtests {W : Finset (Finset Formula)} (R : ℕ → ↥W → ↥W → Prop) (F : List Formula) : ↥W → ↥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, Modelgraphs.Q R (?'τ) x✝¹ x✝)

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

Q_δ for a list δ of programs.

Equations

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

@[simp]

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

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

def Qcombo {W : Finset (Finset Formula)} (R : ℕ → ↥W → ↥W → Prop) (F : List Formula) (δ : List Program) : ↥W → ↥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 cpHelpA {W : Finset (Finset Formula)} (R : ℕ → ↥W → ↥W → Prop) (α : Program) (Fδ : List Formula × List Program) : Fδ ∈ H α → ∀ (v w : ↥W), Qcombo R Fδ.1 Fδ.2 v w → Modelgraphs.Q R α v w

Q_Fδ v w implies Q v w.