Section 2.5: Soundness and Completeness Theorems
Soundness
Every logical axiom is valid.
A1: Exercise 2.4.3(b). A3: Exercise 2.2.3. A4: Exercise 2.2.4. A5: By definition.
A6: Similar to Exercise 2.2.5, but using induction in general.
A2: We prove and use
and (Substitution Lemma)
(where
is substitutable for
in
) for terms and formulas, respectively.
A set of wffs
is called satisfiable iff there is
and
such that
satisfies (every member of)
with
.
(Soundness Theorem) If
, then
.
 If is satisfiable, then is consistent. This is, in fact, equivalent to the theorem.

If
or, equivalently,
and
, then
and
are logically equivalent.
 Alphabetic variants are logically equivalent.
(Completeness Theorem; Gödel, 1930) If
, then
.

If
is consistent, then
is satisfiable. This is, in fact, equivalent to the theorem.Let be consistent. First, we expand the language by adding infinitely many constant symbols , and expand by adding wffs for each (in the expanded language) and using constant symbols such that and does not occur in . The resulting set is consistent. Further, we extend to a consistent such that for each , either or (in the uncountable case we use Zorn’s Lemma, but however we do this, turns out to be deductively closed: iff ).Second, we define a) a new binary relation (instead of ); b) a structure where is the set of all terms (of the expanded language), , , ; , and c) a function by ( ). Then, iff where is with replaced by .Third, we note that is a congruence relation for (an equivalence relation such that and are compatible with ), therefore, the quotient structure is such that a) is a homomorphism of onto where , b) is the equality relation on , and c) iff . The restriction of to the original language satisfies every member of with .
(Compactness Theorem) If
, then for some finite
,
.
 is satisfiable iff every finite is satisfiable. has a model iff every finite has a model.
 Disjoint classes can be separated by an class: if for two sets of sentences, , then there is a sentence such that and .
 For where iff , there is an elementarily equivalent disconnected structure.
Decidability
(Enumerability Theorem) For a reasonable language (the set of parameters can be effectively enumerated and the relations
and
are decidable), the set of valid wffs can be effectively enumerated.
 A finite language is one having only finitely many parameters. A finite language is reasonable.
 A reasonable language must be countable.
 If is decidable and the language is reasonable, then and are effectively enumerable.
 If is decidable, the language is reasonable, and for every sentence , or , then is decidable.