The bulk of Henkin’s proof is to show that for any consistent sentence s of the predicate calculus there is a denumerable model that satisfies s.
<p>The proof works whether or not equality is included in predicate calculus.
<p>
It proceeds by enumerating the sentences of predicate calculus using just the predicates in s.
We accumulate a set of sentences beginning with s as the sole member.
As we proceed this set will grow and remain collectively consistent.
In turn consider each sentence t of the enumeration.
If the current set plus t is consistent then add t to the set.
If the set plus t is not consistent and of the form ⋀xφ then:<ul>
<li>let b be the first individual constant not appearing in our set so far,
<li>form the sentence ψ which is like φ except for having b wherever φ has a free occurrence of x.</ul>
¬ψ will be consistent (lemma) and we add it now to the set.
<p>After all sentences have been considered we have a consistent set of sentences including s.
Each sentence of our set without quantifiers, implications, or more than one not sign, is composed of an optional not sign, and predicate followed by some number of individual constants.
This reduced set is a very explicit denumerable model which satisfies s!