Completeness Proof (Section 6.4)

theorem PDL.strmg (X : Sequent) (s : Lean4GlCoalgebras.Strategy tableauGame Lean4GlCoalgebras.Player.B) (h : Lean4GlCoalgebras.winning s (startPos X)) : ∃ (WS : Finset (Finset Formula)) (x : ModelGraph WS), ∃ Z ∈ WS, X.toFinset ⊆ Z

Theorem 6.21: If Builder has a winning strategy then there is a model graph. Uses BuildTree.toModel.

theorem PDL.modelExistence {X : Sequent} : consistent X → ∃ (WS : Finset (Finset Formula)) (x : ModelGraph WS) (W : ↥WS), X.toFinset ⊆ ↑W

Helper for completeness. Uses gameP and strmg.

theorem PDL.Tableau.toUniformViaGame {X : Sequent} (Xfree : X.isFree) (tab : Tableau [] X) : ∃ (u_tab : Tableau [] X), u_tab.isUniform

If there is any tableau, then there is a uniform one. Proven via gameP and used to show interpolation.

theorem PDL.completeness (X : Sequent) : consistent X → HasSat.satisfiable X

Theorem 6.1

theorem PDL.consIffSat (X : Sequent) : X.isFree → (consistent X ↔ HasSat.satisfiable X)

theorem PDL.singletonConsIffSat (φ : Formula) : consistent ({φ}, ∅, none) ↔ HasSat.satisfiable φ