Completeness Proof (Section 6.4)

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 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 φ