§ Completeness for first order logic

• This requires soundness to have been established before.
• We work with sequent calculus, where Γ => Δ means that g1 /\ g1 /\ ... /\ gn => d1 \/ d2 \/ .. \/ dn.
• First prove that Γ => Δ is derivable iff Γ U ~Δ => 0 is derivable.
• By soundness, this means that Γ U ~Δ is inconsistent.
• Thus, see that Γ => Δ is derivable ifff Γ U ~Δ is inconsistent.
• contraposing, Γ => Δ is NOT derivable ifff Γ U ~Δ is Consistent.
• Thus, the set CONSISTENT := { Γ=>Δ | Γ=>Δ has a model} is equal to the set { Γ=>Δ | Γ U ~Δ is inconsistent}, which (by soundness) is the same as { Γ=>Δ | ΓU~Δ is not derivable}.
• We want to show that CONSISTENT is a satisfiable set (obeys conditions (S0)... (S8)), which will allow us to produce models for all Φ ∈ CONSISTENT (by taking the closure Φ# and building the term model, where taking the closure needs the ambient CONSISTENT set to obey satisfiability).
• Thus, this shows that every element of consistent (proofs of sequent calculus) in fact has a model, and thus we are complete.