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.bothSides.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.bothSides.toFinset ⊆ ↑W

Helper for completeness. Uses gameP and strmg.

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

Theorem 6.1

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

theorem singletonConsIffSat (φ : Formula) : consistent ([φ], [], none) ↔ HasSat.satisfiable φ