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