Soundness (Section 6)

Soundness of the PDL rules

theorem pdlRuleSat {X Y : Sequent} (r : PdlRule X Y) (satX : HasSat.satisfiable X) : HasSat.satisfiable Y

The PDL rules are sound.

Companion, cEdge, etc.

def companionOf {X : Sequent} {tab : Tableau [] X} (s : PathIn tab) (lpr : LoadedPathRepeat (tabAt s).fst (tabAt s).snd.fst) : (tabAt s).snd.snd = Tableau.lrep lpr → PathIn tab

To get the companion of a LoadedPathRepeat we rewind the path with the lpr value. The succ is there because the lpr values are indices of the history starting with 0, but PathIn.rewind 0 would do nothing.

Equations

• companionOf s lpr x✝ = s.rewind (⋯ ▸ ↑lpr).succ

def companion {X : Sequent} {tab : Tableau [] X} (s t : PathIn tab) : Prop

s ♥ t means s is a LoadedPathRepeat and the companionOf s is t.

Equations

• s ♥ t = ∃ (lpr : LoadedPathRepeat (tabAt s).fst (tabAt s).snd.fst) (h : (tabAt s).snd.snd = Tableau.lrep lpr), t = companionOf s lpr h

def «term_♥_» : Lean.TrailingParserDescr

Equations

• «term_♥_» = Lean.ParserDescr.trailingNode `«term_♥_» 1022 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ♥ ") (Lean.ParserDescr.cat `term 1023))

theorem nodeAt_companionOf_eq_toHistory_get_lpr_val {a✝ : Sequent} {tab : Tableau [] a✝} (s : PathIn tab) (lpr : LoadedPathRepeat (tabAt s).fst (tabAt s).snd.fst) (h : (tabAt s).snd.snd = Tableau.lrep lpr) : nodeAt (companionOf s lpr h) = List.get s.toHistory (⋯ ▸ ↑lpr)

The node at a companion is the same as the one in the history.

theorem nodeAt_companionOf_setEq {X : Sequent} {tab : Tableau [] X} (s : PathIn tab) (lpr : LoadedPathRepeat (tabAt s).fst (tabAt s).snd.fst) (h : (tabAt s).snd.snd = Tableau.lrep lpr) : (nodeAt (companionOf s lpr h)).setEqTo (nodeAt s)

theorem companion_loaded {a✝ : Sequent} {a✝¹ : Tableau [] a✝} {s t : PathIn a✝¹} : s ♥ t → (nodeAt s).isLoaded = true ∧ (nodeAt t).isLoaded = true

Any repeat and companion are both loaded.

theorem companionOf_length_lt_length {a✝ : Sequent} {tab : Tableau [] a✝} {t : PathIn tab} (lpr : LoadedPathRepeat (tabAt t).fst (tabAt t).snd.fst) (h : (tabAt t).snd.snd = Tableau.lrep lpr) : (companionOf t lpr h).length < t.length

The companion is strictly before the the repeat.

def cEdge {X : Sequent} {ctX : Tableau [] X} (s t : PathIn ctX) : Prop

Equations

• s ◃ t = (s ⋖_ t ∨ s ♥ t)

def «term_◃_» : Lean.TrailingParserDescr

Equations

• «term_◃_» = Lean.ParserDescr.trailingNode `«term_◃_» 1022 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ◃ ") (Lean.ParserDescr.cat `term 1023))

def «term_◃⁺_» : Lean.TrailingParserDescr

Equations

• «term_◃⁺_» = Lean.ParserDescr.trailingNode `«term_◃⁺_» 1022 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ◃⁺ ") (Lean.ParserDescr.cat `term 1023))

def «term_◃*_» : Lean.TrailingParserDescr

Equations

• «term_◃*_» = Lean.ParserDescr.trailingNode `«term_◃*_» 1022 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ◃* ") (Lean.ParserDescr.cat `term 1023))

≡ᶜ and Clusters

def cEquiv {X : Sequent} {tab : Tableau [] X} (s t : PathIn tab) : Prop

Nodes are c-equivalent iff there are ◃ paths both ways. Note that this is not a closure, so we do not want Relation.EqvGen here.

Equations

• s ≡ᶜ t = (s ◃* t ∧ t ◃* s)

def «term_≡ᶜ_» : Lean.TrailingParserDescr

Equations

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

theorem cEquiv.symm {a✝ : Sequent} {tab : Tableau [] a✝} (s t : PathIn tab) : s ≡ᶜ t ↔ t ≡ᶜ s

≡ᶜ is symmetric.

def clusterOf {X : Sequent} {tab : Tableau [] X} (p : PathIn tab) : Quot cEquiv

Equations

• clusterOf p = Quot.mk cEquiv p

def before {X : Sequent} {tab : Tableau [] X} (s t : PathIn tab) : Prop

We have before s t iff there is a path from s to t but not from t to s. This means the cluster of s comes before the cluster of t in tab. NB: The notes use ◃* here but we use ◃⁺. The definitions are equivalent.

Equations

• s <ᶜ t = (s ◃⁺ t ∧ ¬t ◃⁺ s)

def «term_<ᶜ_» : Lean.TrailingParserDescr

s <ᶜ t means there is a ◃-path from s to t but not from t to s. This means t is simpler to deal with first.

Equations

• «term_<ᶜ_» = Lean.ParserDescr.trailingNode `«term_<ᶜ_» 1022 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <ᶜ ") (Lean.ParserDescr.cat `term 1023))

theorem before.irrefl {X : Sequent} {tab : Tableau [] X} : IsIrrefl (PathIn tab) before

The <ᶜ relation is irreflexive.

theorem before.trans {X : Sequent} {tab : Tableau [] X} : Transitive before

The <ᶜ relation is transitive.

theorem trans_before.irrefl {X : Sequent} {tab : Tableau [] X} : IsIrrefl (PathIn tab) (Relation.TransGen before)

The transitive closure of <ᶜ (which in fact is the same as <ᶜ) is irreflexive.

theorem before.wellFounded {X : Sequent} {tab : Tableau [] X} : WellFounded before

The before relation in a tableau is well-founded.

theorem flip_before.irrefl {X : Sequent} {tab : Tableau [] X} : IsIrrefl (PathIn tab) (flip before)

The converse of <ᶜ is irreflexive.

theorem Relation.TransGen.flip_iff (α : Type) {r : α → α → Prop} {a b : α} : TransGen (flip r) a b ↔ TransGen r b a

theorem trans_flip_before.irrefl {X : Sequent} {tab : Tableau [] X} : IsIrrefl (PathIn tab) (Relation.TransGen (flip before))

The transtive closure of the converse of <ᶜ is irreflexive.

theorem flip_before.wellFounded {X : Sequent} {tab : Tableau [] X} : WellFounded (flip before)

The before relation in a tableau is converse well-founded.

theorem eProp {X : Sequent} (tab : Tableau [] X) : Equivalence cEquiv ∧ WellFounded before ∧ WellFounded (flip before)

≣ᶜ is an equivalence relation and <ᶜ is well-founded and converse well-founded. The converse well-founded is what we really need for induction proofs.

theorem eProp2.a {X : Sequent} {tab : Tableau [] X} (s t : PathIn tab) : s ⋖_ t → s <ᶜ t ∨ t ≡ᶜ s

theorem eProp2.b {X : Sequent} {tab : Tableau [] X} (s t : PathIn tab) : s ♥ t → t ≡ᶜ s

theorem eProp2.c_help {X : Sequent} {tab : Tableau [] X} (s : PathIn tab) : (nodeAt s).isFree = true → ∀ (t : PathIn tab), s < t → s <ᶜ t

theorem eProp2.c {X : Sequent} {tab : Tableau [] X} (s t : PathIn tab) : (nodeAt s).isFree = true → s ⋖_ t → s <ᶜ t

theorem not_cEquiv_of_free_loaded {a✝ : Sequent} {tab : Tableau [] a✝} (s t : PathIn tab) (s_free : (nodeAt s).isFree = true) (t_loaded : (nodeAt t).isLoaded = true) : ¬s ≡ᶜ t

A free node and a loaded node cannot be ≡ᶜ equivalent.

theorem eProp2.d {X : Sequent} {tab : Tableau [] X} (s t : PathIn tab) : (nodeAt s).isLoaded = true → (nodeAt t).isFree = true → s ⋖_ t → s <ᶜ t

theorem eProp2.d_help {X : Sequent} {tab : Tableau [] X} (s t : PathIn tab) : (nodeAt t).isLoaded = true → (nodeAt s).isFree = true → t ◃⁺ s → ¬s ◃⁺ t

theorem eProp2.e {X : Sequent} {tab : Tableau [] X} (s u t : PathIn tab) : s <ᶜ u → u <ᶜ t → s <ᶜ t

<ᶜ is transitive

theorem eProp2.f {X : Sequent} {tab : Tableau [] X} (s t : PathIn tab) : t ◃⁺ s → ¬t ≡ᶜ s → t <ᶜ s

theorem eProp2.f_tweak {X : Sequent} {tab : Tableau [] X} (s u t : PathIn tab) : s ◃⁺ u → u ◃⁺ t → ¬t ≡ᶜ u → ¬t ≡ᶜ s

theorem eProp2.g {X : Sequent} {tab : Tableau [] X} (s t : PathIn tab) : s <ᶜ t → ¬s ≡ᶜ t

theorem eProp2.h {X : Sequent} {tab : Tableau [] X} (s u t : PathIn tab) : s <ᶜ u → s ≡ᶜ t → t <ᶜ u

theorem eProp2 {X : Sequent} {tab : Tableau [] X} (s u t : PathIn tab) : (s ⋖_ t → s <ᶜ t ∨ t ≡ᶜ s) ∧ (s ♥ t → t ≡ᶜ s) ∧ ((nodeAt s).isFree = true → s ⋖_ t → s <ᶜ t) ∧ ((nodeAt s).isLoaded = true → (nodeAt t).isFree = true → s ⋖_ t → s <ᶜ t) ∧ (t <ᶜ u → u <ᶜ s → t <ᶜ s) ∧ (t ◃⁺ s → ¬t ≡ᶜ s → t <ᶜ s) ∧ (s <ᶜ t → ¬s ≡ᶜ t) ∧ (s <ᶜ u → s ≡ᶜ t → t <ᶜ u)

Soundness

theorem localLoadedDiamond (α : Program) {X : Sequent} (ltab : LocalTableau X) {W : Type} {M : KripkeModel W} {v w : W} (v_α_w : relate M α v w) (v_t : (M, v)⊨X) (ξ : AnyFormula) {side : Side} (negLoad_in : (~''(AnyFormula.loaded (⌊α⌋ξ))).in_side side X) (w_nξ : (M, w)⊨~''ξ) : ∃ Y ∈ endNodesOf ltab, (M, v)⊨Y ∧ (Y.isFree = true ∨ ∃ (F : List Formula) (γ : List Program), (~''(AnyFormula.loadBoxes γ ξ)).in_side side Y ∧ relateSeq M γ v w ∧ (M, v)⊨F ∧ (F, γ) ∈ H α ∧ (Y.without (~''(AnyFormula.loadBoxes γ ξ))).isFree = true)

Helper to deal with local tableau in loadedDiamondPaths.

theorem Sequent.isLoaded_of_negAnyFormula_loaded {α : Program} {ξ : AnyFormula} {side : Side} {X : Sequent} (negLoad_in : (~''(AnyFormula.loaded (⌊α⌋ξ))).in_side side X) : X.isLoaded = true

theorem boxes_true_at_k_of_Vector_rel {W : Type} {M : KripkeModel W} (ξ : AnyFormula) (δ : List Program) (h : ¬δ = []) (ws : List.Vector W δ.length.succ) (ws_rel : ∀ (i : Fin δ.length), relate M (δ.get i) (ws.get ↑↑i) (ws.get i.succ)) (k : Fin δ.length) (w_nξ : (M, ws.last)⊨~''ξ) : (M, ws.get k.succ)⊨~''(AnyFormula.loadBoxes (List.drop (↑k.succ) δ) ξ)

@[irreducible]

theorem loadedDiamondPaths (α : Program) {X : Sequent} (tab : Tableau [] X) (root_free : X.isFree = true) (t : PathIn tab) {W : Type} {M : KripkeModel W} {v w : W} (v_t : (M, v)⊨nodeAt t) (ξ : AnyFormula) {side : Side} (negLoad_in : (~''(AnyFormula.loaded (⌊α⌋ξ))).in_side side (nodeAt t)) (v_α_w : relate M α v w) (w_nξ : (M, w)⊨~''ξ) : ∃ (s : PathIn tab), t ◃⁺ s ∧ (HasSat.satisfiable (nodeAt s) ∧ ¬s ≡ᶜ t ∨ (~''ξ).in_side side (nodeAt s) ∧ (M, w)⊨nodeAt s ∧ ((nodeAt s).without (~''ξ)).isFree = true)

Soundness of loading and repeats: a tableau can immitate all moves in a model.

theorem simpler_equiv_simpler {a✝ : Sequent} {tab : Tableau [] a✝} {u s t : PathIn tab} : s <ᶜ u → s ≡ᶜ t → t <ᶜ u

theorem tableauThenNotSat {Root : Sequent} (tab : Tableau [] Root) (Root_isFree : Root.isFree = true) (t : PathIn tab) : ¬HasSat.satisfiable (nodeAt t)

Any node in a closed tableau with a free root is not satisfiable. This is the main argument for soundness.

theorem correctness (LR : Sequent) : LR.isFree = true → HasSat.satisfiable LR → consistent LR

theorem soundTableau (φ : Formula) : provable φ → ¬HasSat.satisfiable {~φ}

theorem soundness (φ : Formula) : provable φ → tautology φ

All provable formulas are semantic tautologies. See tableauThenNotSat for what the notes call soundness.