## § 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.