Model Existence Lemma

Let be a Consistent Theory in a first-order language
Then has a model.

Idea

We build a model from the language itself
To begin with, we let be the set of closed terms of , i.e. terms with no variables
We turn this into a Structure in the obvious way

is still not a model (e.g. and are not equal in )
Define equivalence relation on by
if and only if
(where )
Replace with
Two issues remain

Firstly, in general, is not complete (i.e. there are sentences where neither nor )
Remedy: Given consistent theory there is a consistent, complete

Secondly, we are missing some elements that are guaranteed by where is for example
Remedy: We add a witness, i.e. a new constant to (the new language is ) and a new sentence to to obtain

Proof (NONEXAMINABLE)

We start with two observations

1. Let be a consistent theory, be a sentence
   Then one of and is consistent
   If not, then by Deduction Theorem
   and and hence by (MP)
   By Zorn’s Lemma there is a maximal consistent theory .
   Then for every sentence , either or
   In particular is complete
2. Suppose where is a formula with . Add a new constant to . Then is consistent
   If not, then by Deduction Theorem
   Since does not appear in it follows that
   Then by (Gen).
   But
   We do this for every theorem of of the form to obtain a new language where is a set of new constants (disjoint from , ) and a new theory s.t. , is consistent and has witnesses for
   We now start with a consistent theory in and by induction construct theories
   and new languages where are pairwise disjoint sets of constants (also disjoint from , )
   s.t. for all , is complete, consistent theory in
   and is a consistent theory in which has witnesses for .
   Set and
   Easy to check that is a consistent theory in which contains , is complete and has witnesses.

Now WLOG and

We let be the set of equivalence classes of closed terms in where if and only if
We make an -Structure:

(lots of checking to do at this stage to prove this is all well defined)

Then prove by induction on terms: if is a term with variables in the set
then
If is a closed term, then

Similarly, for any formula with
iff
In particular, if then so
Thus is a model of