Completeness Proof (Section 6.4)

theorem strmg (X : Sequent) (s : Strategy tableauGame Builder) (h : 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 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 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 completeness (X : Sequent) : consistent X → HasSat.satisfiable X

Theorem 6.1

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

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