Theorem 1 (Gödel completeness theorem, informal statement) Let be a first-order theory (a formal language , together with a set of axioms, i.e. sentences assumed to be true), and let be a sentence in the formal language. Assume also that the language has at most countably many symbols. Then the following are equivalent:
- (i) (Syntactic consequence) can be deduced from the axioms in by a finite number of applications of the laws of deduction in first order logic. (This property is abbreviated as .)
- (ii) (Semantic consequence) Every structure which satisfies or models , also satisfies . (This property is abbreviated as .)
- (iii) (Semantic consequence for at most countable models) Every structure which is at most countable, and which models , also satisfies .
One can also formulate versions of the completeness theorem for languages with uncountably many symbols, but I will not do so here. One can also force other cardinalities on the model by using the Löwenheim-Skolem theorem.
To state this theorem even more informally, any (first-order) result which is true in all models of a theory, must be logically deducible from that theory, and vice versa. (For instance, any result which is true for all groups, must be deducible from the group axioms; any result which is true for all systems obeying Peano arithmetic, must be deducible from the Peano axioms; and so forth.) In fact, it suffices to check countable and finite models only; for instance, any first-order statement which is true for all finite or countable groups, is in fact true for all groups! Informally, a first-order language with only countably many symbols cannot “detect” whether a given structure is countably or uncountably infinite. Thus for instance even the ZFC axioms of set theory must have some at most countable model, even though one can use ZFC to prove the existence of uncountable sets; this is known as Skolem’s paradox. (To resolve the paradox, one needs to carefully distinguish between an object in a set theory being “externally” countable in the structure that models that theory, and being “internally” countable within that theory.)
Of course, a theory may contain undecidable statements – sentences which are neither provable nor disprovable in the theory. By the completeness theorem, this is equivalent to saying that is satisfied by some models of but not by other models. Thus the completeness theorem is compatible with the incompleteness theorem: recursively enumerable theories such as Peano arithmetic are modeled by the natural numbers , but are also modeled by other structures also, and there are sentences satisfied by which are not satisfied by other models of Peano arithmetic, and are thus undecidable within that arithmetic.
An important corollary of the completeness theorem is the compactness theorem:
- (i) is consistent, i.e. it is not possible to logically deduce a contradiction from the axioms in .
- (ii) is satisfiable, i.e. there exists a structure that models .
- (iii) There exists a structure which is at most countable, that models .
- (iv) Every finite subset of is consistent.
- (v) Every finite subset of is satisfiable.
- (vi) Every finite subset of is satisfiable with an at most countable model.
Indeed, the equivalence of (i)-(iii), or (iv)-(vi), follows directly from the completeness theorem, while the equivalence of (i) and (iv) follows from the fact that any logical deduction has finite length and so can involve at most finitely many of the axioms in . (Again, the theorem can be generalised to uncountable languages, but the models become uncountable also.)
There is a consequence of the compactness theorem which more closely resembles the sequential concept of compactness. Given a sequence of structures for , and another structure for , let us say that converges elementarily to if every sentence which is satisfied by , is also satisfied by for sufficiently large . (Replacing by its negation , we also see that every sentence that is not satisfied by , is not satisfied by for sufficiently large .) Note that the limit is only unique up to elementary equivalence. Clearly, if each of the models some theory , then the limit will also; thus for instance the elementary limit of a sequence of groups is still a group, the elementary limit of a sequence of rings is still a ring, etc.
Corollary 3 (Sequential compactness theorem) Let be a language with at most countably many symbols, and let be a sequence of structures for . Then there exists a subsequence which converges elementarily to a limit which is at most countable.
Proof: For each structure , let be the theory of that structure, i.e. the set of all sentences that are satisfied by that structure. One can view that theory as a point in , where is the set of all sentences in the language . Since has at most countably many symbols, is at most countable, and so (by the sequential Tychonoff theorem) is sequentially compact in the product topology. (This can also be seen directly by the usual Arzelá-Ascoli diagonalisation argument.) Thus we can find a subsequence which converges in the product topology to a limit theory , thus every sentence in is satisfied by for sufficiently large (and every sentence not in is not satisfied by for sufficiently large ). In particular, any finite subset of is satisfiable, hence consistent; by the compactness theorem, itself is therefore consistent, and has an at most countable model . Also, each of the theories is clearly complete (given any sentence , either or is in the theory), and so is complete as well. One concludes that is the theory of , and hence is the elementary limit of the as claimed.
[It is also possible to state the compactness theorem using the topological notion of compactness, as follows: let be the space of all structures of a given language , quotiented by elementary equivalence. One can define a topology on by taking the sets as a sub-base, where ranges over all sentences. Then the compactness theorem is equivalent to the assertion that is topologically compact.]
One can use the sequential compactness theorem to build a number of interesting “non-standard” models to various theories. For instance, consider the language used by Peano arithmetic (which contains the operations and the successor operation , the relation , and the constant ), and adjoint a new constant to create an expanded language . For each natural number , let be a structure for which consists of the natural numbers (with the usual interpretations of , , etc.) and interprets the symbol as the natural number . By the compactness theorem, some subsequence of must converge elementarily to a new structure of , which still models Peano arithmetic, but now has the additional property that for every (standard) natural number ; thus we have managed to create a non-standard model of Peano arithmetic which contains a non-standardly large number (one which is larger than every standard natural number).
The sequential compactness theorem also lets us construct infinitary limits of various sequences of finitary objects; for instance, one can construct infinite pseudo-finite fields as the elementary limits of sequences of finite fields. I recently discovered that other several correspondence principles between finitary and infinitary objects, such as the Furstenberg correspondence principle between sets of integers and dynamical systems, or the more recent correspondence principles concerning graph limits, can be viewed as special cases of the sequential compactness theorem; it also seems possible to encode much of the sum-product theory in finite fields in an infinitary setting using this theorem. I hope to discuss these points in more detail in a later post. In this post, I wish to review (partly for my own benefit) the proof of the completeness (and hence compactness) theorem. The material here is quite standard (I basically follow the usual proof of Henkin, and taking advantage of Skolemisation), but perhaps the concept of an elementary limit is not as well-known outside of logic as it might be. (The closely related concept of an ultraproduct is better known, and can be used to prove most of the compactness theorem already, thanks to Los’s theorem, but I do not know how to use ultraproducts to ensure that the limiting model is countable. However, one can think (intuitively, at least), of the limit model in the above theorem as being the set of “constructible” elements of an ultraproduct of the .)
In order to emphasise the main ideas in the proof, I will gloss over some of the more technical details in the proofs, relying instead on informal arguments and examples at various points.
— 1. Completeness and compactness in propositional logic —
The completeness and compactness theorems are results in first-order logic. But to motivate some of the ideas in proving these theorems, let us first consider the simpler case of propositional logic. The language of a propositional logic consists of the following:
- A finite or infinite collection of propositional variables – atomic formulae which could be true or false, depending on the interpretation;
- A collection of logical connectives, such as conjunction , disjunction , negation , or implication . (The exact choice of which logical connectives to include in the language is to some extent a matter of taste.)
- Parentheses (in order to indicate the order of operations).
Of course, we assume that the symbols used for atomic formulae are distinct from those used for logical connectives, or for parentheses; we will implicitly make similar assumptions of this type in later sections without further comment.
Using this language, one can form sentences (or formulae) by some standard formal rules which I will not write down here. Typical examples of sentences in propositional logic are , , and . Each sentence is of finite length, and thus involves at most finitely many of the propositional variables. Observe that if is at most countable, then there are at most countably many sentences.
The analogue of a structure in propositional logic is a truth assignment. A truth assignment for a propositional language consists of a truth value assigned to each propositional variable . (Thus, for instance, if there are propositional variables in the language, then there are possible truth assignments.) Once a truth assignment has assigned a truth value to each propositional variable , it can then assign a truth value to any other sentence in the language by using the usual truth tables for conjunction, negation, etc.; we write if assigns a true value to (and say that is satisfied by ), and otherwise. Thus, for instance, if and , then and , but . Some sentences, e.g. , are true in every truth assignment; these are the (semantic) tautologies. At the other extreme, the negation of a tautology will of course be false in every truth assignment.
A theory is a language , together with a (finite or infinite) collection of sentences (also called ) in that language. A truth assignment satisfies (or models) the theory , and we write , if we have for all . Thus, for instance, if is as in the preceding example and , then .
The analogue of the Gödel completeness theorem is then
- (i) (Syntactic consequence) can be deduced from the axioms in by a finite number of applications of the laws of propositional logic.
- (ii) (Semantic consequence) Every truth assignment which satisfies (or models) , also satisfies .
One can list a complete set of laws of propositional logic used in (i), but we will not do so here.
To prove the completeness theorem, it suffices to show the following equivalent version.
- (i) is consistent, i.e. it is not possible to logically deduce a contradiction from the axioms in .
- (ii) is satisfiable, i.e. there exists a truth assignment that models .
It remains to prove Theorem 5. It is easy to deduce (i) from (ii), because the laws of propositional logic are sound: given any truth assignment, it is easy to verify that these laws can only produce true conclusions given true hypotheses. The more interesting implication is to obtain (ii) from (i) – given a consistent theory , one needs to produce a truth assignment that models that theory.
Let’s first consider the case when the propositional language is finite, so that there are only finitely many propositional variables . Then we can argue using the following “greedy algorithm”.
- We begin with a consistent theory .
- Observe that at least one of or must be consistent. For if both and led to a logical contradiction, then by the laws of logic one can show that must also lead to a logical contradiction.
- If is consistent, we set and ; otherwise, we set and .
- is consistent, so arguing as before we know that at least one of or must be consistent. If the former is consistent, we set and ; otherwise set and .
- We continue in this fashion, eventually ending up with a consistent theory containing , and a complete truth assignment such that whenever is such that , and such that whenever is such that .
- From the laws of logic and an induction argument, one then sees that if is any sentence with , then is a logical consequence of , and hence (since is consistent) is not a consequence of . Taking contrapositives, we see that whenever is a consequence of ; replacing by we conclude that satisfies every sentence in , and the claim follows.
Remark 1 The above argument shows in particular that any finite theory either has a model or a proof of a contradictory statement (such as ). Actually producing a model if it exists, though, is essentially the infamous satisfiability problem, which is known to be NP-complete, and thus (if ) would require super-polynomial time to execute.
The case of an infinite language can be obtained by combining the above argument with Zorn’s lemma (or transfinite induction and the axiom of choice, if the set of propositional variables happens to be well-ordered). Alternatively, one can proceed by establishing
- (i) is satisfiable.
- (ii) Every finite subset of is satisfiable.
It is easy to see that Theorem 6 will allow us to use the finite case of Theorem 5 to deduce the infinite case, so it remains to prove Theorem 6. The implication of (ii) from (i) is trivial; the interesting implication is the converse.
Observe that there is a one-to-one correspondence between truth assignments and elements of the product space , where is the set of propositional variables. For every sentence , let be the collection of all truth assignments that satisfy ; observe that this is a closed (and open) subset of in the product topology (basically because only involves finitely many of the propositional variables). If every finite subset of is satisfiable, then is non-empty; thus the family of closed sets enjoys the finite intersection property. On the other hand, from Tychonoff’s theorem, is compact. We conclude that is non-empty, and the claim follows.
Remark 2 While Tychonoff’s theorem in full generality is equivalent to the axiom of choice, it is possible to prove the compactness theorem using a weaker version of this axiom, namely the ultrafilter lemma. In fact, the compactness theorem is logically equivalent to this lemma.
— 2. Zeroth-order logic —
Propositional logic is far too limited a language to do much mathematics. Let’s make the language a bit more expressive, by adding constants, operations, relations, and (optionally) the equals sign; however, we refrain at this stage from adding variables or quantifiers, making this a zeroth-order logic rather than a first-order one.
A zeroth-order language consists of the following objects:
- A (finite or infinite) collection of propositional variables;
- A collection of relations (or predicates), with each having an arity (or valence) (e.g. unary relation, binary relation, etc.);
- A collection of constants;
- A collection of operators (or functions), with each operator having an arity (e.g. unary operator, binary operator, etc.);
- Logical connectives;
- Optionally, the equals sign .
For instance, a zeroth-order language for arithmetic on the natural numbers might include the constants , the binary relations , the binary operations , the unary successor operation , and the equals sign . A zeroth-order language for studying all groups generated by six elements might include six generators and the identity element as constants, as well as the binary operation of group multiplication and the unary operation of group inversion, together with the equals sign . And so forth.
Note that one could shorten the description of such languages by viewing propositional variables as relations of arity zero, and similarly viewing constants as operators of arity zero, but I find it conceptually clearer to leave these two operations separate, at least initially. As we shall see shortly, one can also essentially eliminate the privileged role of the equals sign by treating it as just another binary relation, which happens to have some standard axioms attached to it.
By combining constants and operators together in the usual fashion one can create terms; for instance, in the zeroth-order language for arithmetic, is a term. By inserting terms into a predicate or relation (or the equals sign ), or using a propositional variable, one obtains an atomic formula; thus for instance is an atomic formula. By combining atomic formulae using logical connectives, one obtains a sentence (or formula); thus for instance is a sentence.
In order to assign meaning to sentences, we need the notion of a structure for a zeroth-order language . A structure consists of the following objects:
- A domain of discourse (or universe of discourse) ;
- An assignment of a value to every constant ;
- An assignment of a function to every operation ;
- An assignment of a truth value to every propositional variable ;
- An assignment of a function to every relation .
For instance, if is the language of groups with six generators discussed above, then a structure would consist of a set , seven elements in that set, a binary operation , and a unary operation . At present, no group-type properties are assumed on these operations; the structure here is little more than a magma at this point.
Every sentence in a zeroth-order language can be interpreted in a structure for that language to give a truth value , simply by substituting all symbols in the language with their interpreted counterparts (note that the equals sign does not need any additional data in order to be interpreted). For instance, the sentence is true in if . Similarly, every term in the language can be interpreted to give a value in the domain of discourse .
As before, a theory is a collection of sentences; we can define satisfiability , of a sentence or a theory by a structure just as in the previous section. For instance, to describe groups with at most six generators in the language , one might use the theory which consists of all the group axioms, specialised to terms, e.g. would contain the associativity axioms for all choices of terms . (Note that this theory is not quite strong enough to capture the concept of a structure being a group generated by six elements, because the domain of may contain some “inaccessible” elements which are not the interpretation of any term in , but without the universal quantifier, there is not much we can do in zeroth-order logic to say anything about those elements, and so this is pretty much the best we can do with this limited logic.)
Now we can state the completeness theorem:
- (i) (Syntactic consequence) can be deduced from the axioms in by a finite number of applications of the laws of zeroth-order logic (i.e. all the laws of first-order logic that do not involve variables or quantifiers).
- (ii) (Semantic consequence) Every truth assignment which satisfies (or models) , also satisfies .
To prove this theorem, it suffices as before to show that every consistent theory in a zeroth-order logic is satisfiable, and conversely. The converse implication is again straightforward (the laws of zeroth-order logic are easily seen to be sound); the main task is to show the forward direction, i.e.
Proof: It is convenient to begin by eliminating the equality symbol from the language. Suppose we have already proven Proposition 8 has already been shown for languages without the equality symbol. Then we claim that the proposition also holds for languages with the equality symbol. Indeed, given a consistent theory in a language with equality, we can form a companion theory in the language formed by removing the equality symbol from and replacing it with a new binary relation , by taking all the sentences in and replacing by , and then adding in all the axioms of equality (with replaced by ) to . Thus, for instance, one would add the transitivity axioms to for each triple of terms , as well as substitution axioms such as for any terms and binary functions . It is straightforward to verify that if is consistent, then is also consistent, because any contradiction derived in can be translated to a contradiction derived in simply by replacing with throughout and using the axioms of equality. By hypothesis, we conclude that has some model . By the axioms of equality, the interpretation of in this model is then an equivalence relation on the domain of . One can also remove from the domain of any element which is not of the form for some term , as such “inaccessible” elements will not influence the satisfiability of . We can then define a structure for the original language by quotienting the domain of by the equivalence relation , and also quotienting all the interpretations of the relations and operations of ; the axioms of equality ensure that this quotienting is possible, and that the quotiented structure satisfies ; we omit the details.
Henceforth we assume that does not contain the equality sign. We will then choose a “tautological” domain of discourse , by setting this domain to be nothing more than the collection of all terms in the language . For instance, in the language of groups on six generators, the domain is basically the free magma (with “inverse”) on six generators plus an “identity”, consisting of terms such as , , etc. With this choice of domain, there is an obvious “tautological” interpretation of constants () and operations (e.g. for binary operations and terms ), which leads to every term being interpreted as itself: .
It remains to figure out how to interpret the propositional variables and relations . Actually, one can replace each relation with an equivalent collection of new propositional variables by substituting in all possible terms in the relation. For instance, if one has a binary relation , one can replace this single relation symbol in the language by a (possibly infinite) collection of propositional variables , one for each pair of terms , leading to a new (and probably much larger) language without any relation symbols. It is not hard to see that if theory is consistent in , then the theory in formed by interpreting all atomic formulae such as as propositional variables is also consistent. If has a model with the tautological domain of discourse, it is not hard to see that this can be converted to a model of with the same domain by defining the interpretation of relations in the obvious manner.
So now we may assume that there are no relation symbols, so that now consists entirely of propositional sentences involving the propositional variables. But the claim now follows from the completeness theorem in propositional logic.
Remark 3 The above proof can be viewed as a combination of the completeness theorem in propositional logic and the familiar procedure in algebra of constructing an algebraic object (e.g. a group) that obeys various relations, by starting with the free version of that object (e.g. a free group) and then quotienting out by the equivalence relation generated by those relations.
Remark 4 Observe that if is at most countable, then the structures constructed by the above procedure are at most countable (because the set of terms is at most countable, and quotienting by an equivalence relation cannot increase the cardinality). Thus we see (as in Theorem 1 or Corollary 2) that if a zeroth-order theory in an at most countable language is satisfiable, then it is in fact satisfiable with an at most countable model.
From the completeness theorem for zeroth-order logic and the above remark we obtain the compactness theorem for zeroth-order logic, which is formulated exactly as in Corollary 2.
— 3. First-order logic —
We are now ready to study languages which are expressive enough to do some serious mathematics, namely the languages of first-order logic, which are formed from zeroth-order logics by adding variables and quantifiers. (There are higher-order logics as well, but unfortunately the completeness and compactness theorems typically fail for these, and they will not be discussed here.)
A language for a first-order logic consists of the following:
- A (finite or infinite) collection of propositional variables;
- A collection of relations, with each having an arity ;
- A collection of constants;
- A collection of operators, with each having an arity ;
- A collection of variables;
- Logical connectives;
- The quantifiers ;
- Optionally, the equals sign .
For instance, the language for Peano arithmetic includes a constant , a unary operator , binary operators , the equals sign , and a countably infinite number of variables .
By combining constants, variables and operators together one creates terms; by inserting terms into predicates or relations, or using propositional variables, one obtains atomic formulae. These atomic formulae can contain a number of free variables. Using logical connectives as well as quantifiers to bind any or all of these variables, one obtains well-formed formulae; a formula with no free variables is a sentence. Thus, for instance, is a well-formed formula, and is a sentence.
A structure for a first-order language is exactly the same concept as for a zeroth-order language: a domain of discourse, together with an interpretation of all the constants, operators, propositional variables, and relations in the language. Given a structure , one can interpret terms with no free variables as elements of , and interpret sentences as truth values , in the standard fashion.
A theory is, once again, a collection of sentences in the first-order language ; one can define what it means for a structure to satisfy a sentence or a theory just as before.
Remark 5 In most fields of mathematics, one wishes to discuss several types of objects (e.g. numbers, sets, points, group elements, etc.) at once. For this, one would prefer to use a typed language, in which variables, constants, and functions take values in one type of object, and relations and functions take only certain types of objects as input. However, one can easily model a typed theory using a typeless theory by the trick of adding some additional unary predicates to capture type (e.g. to indicate the assertion “ is a natural number”, to indicate the assertion “ is a set”, etc.) and modifying the axioms of the theory being considered accordingly. (For instance, in a language involving both natural numbers and other mathematical objects, one might impose a new closure axiom , and axioms such as the commutativity axiom would need to be modified to .) It is a tedious but routine matter to show that the completeness and compactness theorems for typeless first-order logic imply analogous results for typed first-order logic; we omit the details.
To prove the completeness (and hence compactness) theorem, it suffices as before to show that
We shall prove this result using a series of reductions. Firstly, we can mimic the arguments in the zeroth-order case and reduce to the case when does not contain the equality symbol. (We no longer need to restrict the domain of discourse to those elements which can be interpreted by terms, because the universal quantifier is now available for use when stating the axioms of equality.) Henceforth we shall assume that the equality symbol is not present in the language.
Next, by using the laws of first-order logic to push all quantifiers in the sentences in to the beginning (e.g. replacing with ) one may assume that all sentences in are in prenex normal form, i.e. they consist of a “matrix” of quantifiers, followed by an quantifier-free formula – a well-formed formula with no quantifiers. For instance, is in prenex normal form, where is an quantifier-free formula with four free variables .
Now we will start removing the existential quantifiers from the sentences in . Let’s begin with a simple case, when contains a sentence of the form for some quantifier-free formula of one free variable . Then one can eliminate the existential quantifier by introducing a witness, or more precisely adjoining a new constant to the language and replacing the statement with the statement , giving rise to a new theory in a new language . The consistency of easily implies the consistency of , while any at most countable model for can be easily converted to an at most countable model for (by “forgetting” the symbol ). (In fact, is a conservative extension of .) We can apply this reduction simultaneously to all sentences of the form in (thus potentially expanding the collection of constants in the language by a countable amount).
The same argument works for any sentence in prenex normal form in which all the existential quantifiers are to the left of the universal quantifiers, e.g. ; this statement requires two constants to separately witness and , but otherwise one proceeds much as in the previous paragraph. But what about if one or more of the existential quantifiers is buried behind a universal quantifier? The trick is then to use Skolemisation. We illustrate this with the simplest case of this type, namely that of a sentence . Here, one cannot use a constant witness for . But this is no problem: one simply introduces a witness that depends on . More precisely, one adjoins a new unary operator to the language and replaces the statement by , creating a new theory in a new language . One can again show (though this is not entirely trivial) that the consistency of implies the consistency of , and that every countable model for can be converted to a countable model for (again by “forgetting” ). So one can eliminate the existential quantifier from this sentence also. Similar methods work for any other prenex normal form; for instance with the sentence
one can obtain a conservative extension of that theory by introducing a unary operator and a binary operator and replacing the above sentence with
One can show that one can perform Skolemisation on all the sentences in simultaneously, which has the effect of eliminating all existential quantifiers from while still keeping the language at most countable (since is at most countable). (Intuitively, what is going on here is that we are interpreting all existential axioms in the theory as implicitly defining functions, which we then explicitly formalise as a new symbol in the language. For instance, if we had some theory of sets which contained the axiom of choice (every family of non-empty sets admits a choice function ), then we can Skolemise this by introducing a “choice function function” that witnessed this axiom to the language. Note that we do not need uniqueness in the existential claim in order to be able to perform Skolemisation.)
After performing Skolemisation and adding all the witnesses to the language, we are reduced to the case in which all the sentences in are in fact universal statements, i.e. of the form , where is an quantifier-free formula of free variables. In this case one can repeat the zeroth-order arguments, selecting a structure whose domain of discourse is the tautological one, indexed by all the terms with no free variables (in particular, this structure will be countable). One can then replace each first-order statement in by the family of zeroth-order statements , where ranges over all terms with no free variables, thus creating a zeroth-order theory . As is consistent, is also, so by the zeroth-order theory, we can find a model for with the tautological domain of discourse, and it is clear that this structure will also be a model for the original theory . The proof of the completeness theorem (and thus the compactness theorem) is now complete.
In summary: to create a countable model from a consistent first-order theory, one first replaces the equality sign (if any) by a binary relation , then uses Skolemisation to make all implied functions and operations explicit elements of the language. Next, one makes the zeroth-order terms of the new language the domain of discourse, applies a greedy algorithm to decide the truth assignment of all zeroth-order sentences, and then finally quotients out by the equivalence relation given by to recover the countable model.
Remark 6 I find the use of Skolemisation to greatly clarify, at a conceptual level, the proof of the completeness theorem. However, at a technical level it does make things more complicated: in particular, showing that the Skolemisation of a consistent theory is still consistent does require some non-trivial effort (one has to take all arguments involving the Skolem function , and replace every occurence of by a “virtual” function, defined implicitly using existential quantifiers). On the other hand, this fact is easy to prove once one already has the completeness theorem, though we of course cannot formally take advantage of this while trying to prove that theorem!
The more traditional Henkin approach is based instead on adding a large number of constant witnesses, one for every existential statement: roughly speaking, for each existential sentence in the language, one adds a new constant to the language and inserts an axiom to the theory; it is easier to show that this preserves consistency than it is with a more general Skolemisation. Unfortunately, every time one adds a constant to the language, one increases the number of existential sentences for which one needs to perform this type of witnessing, but it turns out that after applying this procedure a countable number of times, one can get to the point where every existential sentence is automatically witnessed by some constant. This has the same ultimate effect as Skolemisation, namely one can convert sentences containing existential quantifiers to ones which are purely universal, and so the rest of the proof is much the same as the proof described above. On the other hand, the Henkin approach avoids the axiom of choice (though one still must use the ultrafilter lemma, of course).