scratch
§ Completeness for First Order Logic
created 2022-09-07
- 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.
❦