In this post I prove a variant of Gödel's completeness theorem. My intention has been to really understand the theorem, so that I am not simply shuffling symbols around, but am actually understanding why it is true. I hope it is helpful for at least some other people.

For sources, I have myself relied mainly on Srivastava's presentation. I have relied a lot on intuitions about sequent calculus; while I present a sequent calculus in this post, this is not a complete introduction to sequent calculus. I recommend Logitext as an online proof tool for gaining more intuition about sequent proofs. I am familiar with sequent calculus mainly through type theory.

First-order theories and models

A first-order theory consists of:

• A countable set of functions, which each have an arity, a non-negative integer.
• A countable set of predicates, which also have non-negative integer arities.
• A countable set of axioms, which are sentences in the theory.

Assume a countably infinite set of variables. A term consists of either a variable, or a function applied to a number of terms equal to its arity. An atomic sentence is a predicate applied to a number of terms equal to its arity. A sentence may be one of:

• an atomic sentence.
• a negated sentence, $\neg P$.
• a conjunction of sentences, $P\wedge Q$.
• a universal, $\forall x,P$, where x is a variable.

Define disjunctions ($P\vee Q:=\neg (\neg P\vee \neg Q)$), implications ($P\to Q:=\neg (P\wedge \neg Q)$), and existentials ($\exists x,P:=\neg \forall x,\neg P$) from these other terms in the usual manner. A first-order theory has a countable set of axioms, each of which are sentences.

So far this is fairly standard; see Peano arithmetic for an example of a first-order theory. I am omitting equality from first-order theories, as in general equality can be replaced with an equality predicate and axioms.

A term or sentence is said to be closed if it has no free variables (that is, variables which are not quantified over). A closed term or sentence can be interpreted without reference to variable assignments, similar to a variable-free expression in a programming language.

Let a constant be a function of arity zero. I will make the non-standard assumption that first-order theories have a countably infinite set of constants which do not appear in any axiom. This will help in defining inference rules and proving completeness. Generally it is not a problem to add a countably infinite set of constants to a first-order theory; it does not strengthen the theory (except in that it aids in proving universals, as defined below).

Before defining inference rules, I will define models. A model of a theory consists of a set (the domain of discourse), interpretations of the functions (as mapping finite lists of values in the domain to other values), and interpretations of predicates (as mapping finite lists of values in the domain to Booleans), which satisfies the axioms. Closed terms have straightforward interpretations in a model, as evaluating the expression (as if in a programming language). Closed sentences have straightforward truth values, e.g. the formula $\neg P$ is true in a model when P is false in the model.

Judgments and sequent rules

A judgment is of the form $\Gamma ⊢\Delta$, where Γ and Δ are (possibly infinite) countable sets of closed sentences. The judgment is true in a model if at least one of Γ is false or at least one of Δ is true. As notation, if Γ is a set of sentences and P is a sentence, then $\Gamma ,P$ denotes $\Gamma \cup \left\{P\right\}$.

The inference rules are expressed as sequents. A sequent has one judgment on the bottom, and a finite set of judgments on top. Intuitively, it states that if all the judgments on top are provable, the rule yields a proof of the judgment on the bottom. Along the way, I will show that each rule is sound: if every judgment on the top is true in all models, then the judgment on the bottom is also true in all models. Note that the rules do not take into account axioms; we can add the axioms as assumptions on the left hand side later, to compensate.

In these rules, Γ, Δ, Σ, and Π represent countable sets of closed sentences, P and Q represent closed sentences, x represents a variable, c represents a constant, and t represents a closed term. $\varphi$ represents a sentence with zero or one free variables; if it has no free variables, $\varphi \left[t\right]=\varphi$, and if it has one free variable, $\varphi \left[t\right]$ represents substituting the term t for the free variable of $\varphi$.

Assumption rule:

$$\frac{}{\Gamma ,P⊢\Delta ,P}$$

This states that if the same sentence appears on both sides, the judgment can be trivially proven. Clearly, in any model, P must be true or false, so either a sentence on the left is false or one on the right is true.

Cut rule:

$$\frac{\Gamma ⊢\Delta ,P\Gamma ,P⊢\Delta }{\Gamma ⊢\Delta }$$

Suppose the top two judgments are true in all models. Then in any model where all of Γ are true and all of Δ are false, P must be true, but it also must be false, a contradiction. So any model must have at least one of Γ false or at least one of Δ true, showing the conclusion. (Note that this cut rule is simplified relative to the usual presentation.)

Weakening rule:

$$\frac{\Gamma ⊢\Delta }{\Gamma \cup \Sigma ⊢\Delta \cup \Pi }$$

Suppose the top judgment is true in all models. Then no model has all of Γ true and all of Δ false. So clearly the bottom judgment is true in all models.

Weakening simply let us remove sentences from either side. Most sequent calculi involve contraction rules, for "doubling" a given sentence, but this is unnecessary given our set-theoretic interpretation of both sides of a judgment.

Rules for compound sentences (negations, conjunctions, and universals) come in left and right varieties, to handle compounds on the left and right of judgments respectively.

Left negation rule:

$$\frac{\Gamma ⊢\Delta ,P}{\Gamma ,\neg P⊢\Delta }$$

Suppose the top judgment is true in all models. Then any model in which Γ are all true and Δ are all false has P true. So clearly, the bottom judgment must be true of all models.

Right negation rule:

$$\frac{\Gamma ,P⊢\Delta }{\Gamma ⊢\Delta ,\neg P}$$

Suppose the top judgment is true in all models. Then any model in which Γ are all true and Δ are all false has P false. So clearly, the bottom judgment must be true of all models.

Left conjunction rule:

$$\frac{\Gamma ,P,Q⊢\Delta }{\Gamma ,P\wedge Q⊢\Delta }$$

Clearly, all of $\Gamma ,P,Q$ are true in exactly the cases where all of $\Gamma ,P\wedge Q$ are true, so the top and bottom judgments are true in the same set of models.

Right conjunction rule:

$$\frac{\Gamma ⊢\Delta ,P\Gamma ⊢\Delta ,Q}{\Gamma ⊢\Delta ,P\wedge Q}$$

Suppose both top judgments are true in all models. Then in any model where Γ are all true and Δ are all false, P and Q must both be true. So the bottom judgment holds in all models.

Left universal rule:

$$\frac{\Gamma ,\varphi \left[t\right]⊢\Delta }{\Gamma ,(\forall x,\varphi [x\left]\right)⊢\Delta }$$

Suppose the top judgment is true in all models. Then in any model where all of Γ are true and all of Δ are false, $\varphi \left[t\right]$ must be false. So in any model where all of Γ are true and all of Δ are false, $\forall x,\varphi \left[x\right]$ must be false, showing the bottom judgment is true in all models.

Right universal rule:

$$\frac{\Gamma ⊢\Delta ,\varphi \left[c\right]}{\Gamma ⊢\Delta ,(\forall x,\varphi [x\left]\right)}$$

We require that the constant c does not appear in Γ, Δ, or $\varphi \left[x\right]$. Suppose the top judgment is true in all models. For contradiction, suppose the bottom judgment is false in some model. In that model, all of Γ must be true and all of Δ must be false, and $\forall x,\varphi \left[x\right]$ must be false, meaning there is some value y in the domain of discourse for which $\varphi$ is false (when interpreting x as equaling y). Consider a modification to this model where the interpretation of c is set to y. Since c does not appear in Γ or Δ, it remains the case that all of Γ are true and all of Δ are false in this model. In this model, $\varphi \left[c\right]$ must also be false. This contradicts that the top judgment is true in all models. (Note that using a constant for c rather than a variable is non-standard, although it helps later.)

A proof of a judgment can be defined recursively: it selects a rule whose bottom is the judgment to be proven, and includes a proof of every judgment on the top. The proof tree must be finite for the proof to be valid.

To simplify future proofs, we will show derived sequent rules:

Right disjunction rule (derived):

$$\frac{\Gamma ,\neg P,\neg Q⊢\Delta }{\frac{\Gamma ,\neg P\wedge \neg Q⊢\Delta }{\Gamma ⊢\Delta ,P\vee Q}}$$

This demonstrates how sequents can be composed. While we could move P and Q to the right side, this turns out to be unnecessary as the rule is used later.

Contradiction rule (derived):

$$\frac{\frac{\Gamma ⊢P}{\Gamma ,\neg P⊢}\Gamma ⊢\neg P}{\Gamma ⊢}$$

This shows that a set of assumptions that implies a sentence and its negation is inconsistent. Note that either side of a judgment can be left empty to indicate an empty set of sentences.

Left double negation rule (derived):

$$\frac{\frac{\Gamma ,P⊢\Delta }{\Gamma ⊢\Delta ,\neg P}}{\Gamma ,\neg \neg P⊢\Delta }$$

Right double negation rule (derived):

$$\frac{\frac{\Gamma ⊢\Delta ,P}{\Gamma ,\neg P⊢\Delta }}{\Gamma ⊢\Delta ,\neg \neg P}$$

Proving soundness

Gödel's completeness theorem states that a closed sentence is provable in a first-order theory if and only if it is true in all models of the theory. This can be separated into a soundness lemma, stating that any provable sentence holds in all models of the theory, and a completeness lemma, stating that any sentence holding in all models of the theory is provable.

What I am showing here is Gödel's completeness theorem for the variant of first-order logic presented. Specifically, if T is a first-order theory, let $T^{\ast }$ be the theory with no axioms, and let Θ be the set of axioms. We say the sentence P is provable in the T if the judgment $\Theta ⊢P$ is provable.

Let's consider the soundness lemma, which states that if $\Theta ⊢P$ is provable, then P is true in all models of T. Suppose we have a proof of $\Theta ⊢P$. We have shown for each rule that if all the top judgments are true in all models, then the bottom judgment is true in all models. So by induction on the proof tree, $\Theta ⊢P$ must be true in all models of $T^{\ast }$. So in any model of $T^{\ast }$, at least one of Θ is false or P is true. The models of T are exactly those models of $T^{\ast }$ in which all of Θ are true, and in all of these models, P must be true.

Alternative statement of the completeness lemma

The completeness lemma states that any sentence holding in all models of the theory is provable. If the theory is T with axioms Θ, this states that for any sentence P, if P is true in all models of T, then $\Theta ⊢P$ is provable.

Let's consider an alternative lemma, the model existence lemma, stating that if a theory is consistent (in that the judgment $\Theta ⊢$ is not provable, with Θ being the axioms of the theory), then it has a model. Suppose the model existence lemma is true; does it follow that the completeness lemma is true?

Suppose we have a theory T with axioms Θ, and P is true in all models of T. Construct the alternative theory T' which is T with the additional axiom that $\neg P$. Suppose P is true in all models of T. Then there are no models of T'. By the model existence lemma, there is a proof of $\Theta ,\neg P⊢$. Now we show $\Theta ⊢P$:

$$\frac{\frac{\frac{}{\Theta ,P⊢P}}{\Theta ⊢P,\neg P}\frac{\Theta ,\neg P⊢}{\Theta ,\neg P⊢P}}{\Theta ⊢P}$$

We have shown that if P is true in all models of T, then it is provable in T. So if we prove the model existence lemma, the completeness lemma follows.

The Henkin construction

To make it easier to prove the model existence lemma, we will consider constructing an alternative Henkin theory for T. In a Henkin theory, for any sentence $\varphi$ with zero or one free variables, it is provable that $(\exists x,\varphi [x\left]\right)\to \varphi \left[c\right]$ for some constant c. We will rewrite the sentence to a logically equivalent one, $(\forall x,\neg \varphi [x\left]\right)\vee \varphi \left[c\right]$. The main purpose of all this is to avoid a situation where an existential statement $\exists x,\varphi \left[x\right]$ is true in a model, but no particular $\varphi \left[t\right]$ is true for closed terms t.

We wish to show that if T is a consistent theory, then there is a consistent Henkin theory whose axioms are a superset of T's. Let us number in order the sentences with zero or one free variables as ${\varphi }_1,{\varphi }_2,\dots$. Start with ${\Theta }_0:=\Theta$. We will define ${\Theta }_i$ for each natural $i\ge 1$:

$${\Theta }_i:={\Theta }_{i-1},(\forall x,\neg \varphi [x\left]\right)\vee \varphi \left[c_i\right]$$

We set each constant $c_i$ so that it appears in neither ${\Theta }_{i-1}$ nor ${\varphi }_i\left[x\right]$. This is doable given that there is a countably infinite set of constants in T not appearing in Θ.

Define each theory $T_i$ to be T except with ${\Theta }_i$ being the set of axioms. We wish to show that each $T_i$ is consistent. By assumption, $T_0=T$ is consistent. Now suppose $T_{i-1}$ is consistent for $i\ge 1$. For contradiction, suppose $T_i$ is inconsistent. Then we have a proof of ${\Theta }_{i-1},(\forall x,\neg \varphi [x\left]\right)\vee \varphi \left[c_i\right]⊢$.

Intuitively, if $T_{i-1}$ disproves $(\forall x,\neg \varphi [x\left]\right)\vee \varphi \left[c_i\right]$, then it must disprove both sides of the disjunct. Let Q be an arbitrary closed sentence and consider the following sequent proof (using cut, the derived rule for right disjunctions, and weakening):

$$\frac{\frac{{\Theta }_{i-1},\neg (\forall x,\neg \varphi [x\left]\right),\neg \varphi \left[c_i\right]⊢Q}{{\Theta }_{i-1}⊢(\forall x,\neg \varphi [x\left]\right)\vee \varphi \left[c_i\right],Q}\frac{{\Theta }_{i-1},(\forall x,\neg \varphi [x\left]\right)\vee \varphi \left[c_i\right]⊢}{{\Theta }_{i-1},(\forall x,\neg \varphi [x\left]\right)\vee \varphi \left[c_i\right]⊢Q}}{{\Theta }_{i-1}⊢Q}$$

We can set $Q=\neg (\forall x,\neg \varphi [x\left]\right)$, and see that ${\Theta }_{i-1},\neg (\forall x,\neg \varphi [x\left]\right),\neg \varphi \left[c_i\right]⊢\neg (\forall x,\neg \varphi [x\left]\right)$ follows from the assumption rule, in order to get ${\Theta }_{i-1}⊢\neg (\forall x,\neg \varphi [x\left]\right)$. Similarly we have ${\Theta }_{i-1}⊢\neg \varphi \left[c_i\right]$. Because $c_i$ does not appear in ${\Theta }_{i-1}$ or $\varphi \left[x\right]$, we have ${\Theta }_{i-1}⊢\forall x,\neg \varphi \left[x\right]$ using the right universal rule. But now it is clear that ${\Theta }_{i-1}$ is contradictory, i.e. $T_{i-1}$ is inconsistent.

So if $T_{i-1}$ is consistent then so is $T_i$. By induction each $T_i$ is consistent. Define ${\Theta }_{\omega }:={\bigcup }_i{\Theta }_i$, with $T_{\omega }$ being T with these axioms, and note that if $T_{\omega }$ were inconsistent, the proof would only use a finite number of assumptions, so some $T_i$ would be inconsistent, as we have disproven. So $T_{\omega }$ must be consistent as well.

Suppose we showed the model existence lemma for $T_{\omega }$. Suppose T is consistent. Then $T_{\omega }$ is consistent. So $T_{\omega }$ has a model. Clearly, this is a model of T since $T_{\omega }$ has strictly more axioms. So T would have a model, showing the model existence lemma for T. It is, then, sufficient to show the model existence lemma for Henkin theories.

Proving the model existence lemma for Henkin theories

Suppose T is a consistent Henkin theory. We wish to show that it has a model. This model will be a term model, meaning its domain of discourse is the set of closed terms. We need to assign a truth value to each closed sentence; number them as $P_1,P_2,\dots$.

Let the axioms of T be Θ. Define ${\Theta }_0:=\Theta$. Now define ${\Theta }_1,{\Theta }_2,\dots$ inductively:

${\Theta }_i:={\Theta }_{i-1},P_i$ if there is a proof of ${\Theta }_{i-1},\neg P_i⊢$.

${\Theta }_i:={\Theta }_{i-1},\neg P_i$ otherwise.

Let $T_i$ be the theory T but with the axioms ${\Theta }_i$. Assume $T_{i-1}$ is consistent (so there is no proof of ${\Theta }_{i-1}⊢$). Suppose there is a proof of ${\Theta }_{i-1},\neg P_i⊢$. Then there is no proof of ${\Theta }_{i-1},P_i⊢$ (using the derived contradiction rule). So $T_i$ would be be consistent. Suppose on the other hand there is no proof of ${\Theta }_{i-1},\neg P_i⊢$. Then clearly $T_i$ is consistent. Either way, if $T_{i-1}$ is consistent, so is $T_i$.

By induction, each $T_i$ is consistent. Using similar logic to before, the limit $T_{\omega }$ (with axioms ${\Theta }_{\omega }$) is consistent. This theory is complete in that for any closed sentence P, it either proves it or its negation. Accordingly it either proves or disproves each closed atomic sentence. From this we can derive a putative term model M by setting the interpretations of a predicate applied to some terms (which are the elements of the domain of discourse) to be true when the corresponding atomic sentence is provable in $T_{\omega }$.

We must check that this putative model actually satisfies the axioms of $T$. To do this, we will show by induction that each closed sentence P is true in M if and only if $T_{\omega }$ proves P (or equivalently, ${\Theta }_{\omega }⊢P$ is provable).

For atomic P, this is trivial.

Negations

Consider $P=\neg Q$. Assume Q is true in M if and only if ${\Theta }_{\omega }⊢Q$.

Suppose first that Q is true in M. Then we have ${\Theta }_{\omega }⊢Q$. So we don't have ${\Theta }_{\omega }⊢\neg Q$, else $T_{\omega }$ would be inconsistent. So P is false in M and not provable in $T_{\omega }$, as desired.

Suppose instead that Q is false in M. Then there is no proof of ${\Theta }_{\omega }⊢Q$, so there must be a proof of ${\Theta }_{\omega }⊢\neg Q$. So P is true in M and provable in $T_{\omega }$, as desired.

Conjunctions

Consider $P=Q\wedge R$. Assume Q is true in M if and only if ${\Theta }_{\omega }⊢Q$ is provable, and likewise for R.

Suppose first that both Q and R are true in M. Then both are provable in $T_{\omega }$. So we have ${\Theta }_{\omega }⊢Q\wedge R$ using the right conjunction rule. So P is true in M and provable in $T_{\omega }$, as desired.

Suppose Q is false in M. Then there is no proof of ${\Theta }_{\omega }⊢Q$. If ${\Theta }_{\omega }⊢P$ then we could prove ${\Theta }_{\omega }⊢Q$, a contradiction.

$$\frac{\frac{\frac{}{{\Theta }_{\omega },Q,R⊢Q}}{{\Theta }_{\omega },Q\wedge R⊢Q}\frac{{\Theta }_{\omega }⊢Q\wedge R}{{\Theta }_{\omega }⊢Q,Q\wedge R}}{{\Theta }_{\omega }⊢Q}$$

So P is false in M and not provable in $T_{\omega }$, as desired.

Suppose R is false in M. This is symmetric with Q.

Universals

Consider $P=\forall x,\varphi \left[x\right]$. Assume, for all closed terms t, that $\varphi \left[t\right]$ is true in M if and only if ${\Theta }_{\omega }⊢\varphi \left[t\right]$.

Suppose that $\varphi \left[t\right]$ is false in M for some t. Then there is no proof of ${\Theta }_{\omega }⊢\varphi \left[t\right]$. If there were a proof of ${\Theta }_{\omega }⊢P$, then there would be a proof of ${\Theta }_{\omega }⊢\varphi \left[t\right]$, a contradiction.

$$\frac{\frac{\frac{}{{\Theta }_{\omega },\varphi \left[t\right]⊢\varphi \left[t\right]}}{{\Theta }_{\omega },(\forall x,\varphi [x\left]\right)⊢\varphi \left[t\right]}\frac{{\Theta }_{\omega }⊢(\forall x,\varphi [x\left]\right)}{{\Theta }_{\omega }⊢\varphi \left[t\right],(\forall x,\varphi [x\left]\right)}}{{\Theta }_{\omega }⊢\varphi \left[t\right]}$$

So P is false in M and not provable in $T_{\omega }$, as desired.

Suppose instead that each $\varphi \left[t\right]$ is true in M. Since $T_{\omega }$ is Henkin (as T is), ${\Theta }_{\omega }⊢(\forall x,\neg \neg \varphi [x\left]\right)\vee \neg \varphi \left[c\right]$ for some constant c. By the inductive assumption, ${\Theta }_{\omega }⊢\varphi \left[c\right]$ is provable. Now we show a general fact about disjunctions:

$$\frac{\frac{\frac{\frac{}{\Gamma ,P⊢P}}{\Gamma ⊢P,\neg P}\frac{\frac{\Gamma ⊢Q}{\Gamma ⊢P,Q}}{\Gamma ⊢P,\neg \neg Q}}{\frac{\Gamma ⊢P,\neg P\wedge \neg \neg Q}{\Gamma ,P\vee \neg Q⊢P}}\frac{\Gamma ⊢P\vee \neg Q}{\Gamma ⊢P,P\vee \neg Q}}{\Gamma ⊢P}$$

Intuitively this says that if Q and $P\vee \neg Q$ are provable, so is P. So in particular we have ${\Theta }_{\omega }⊢(\forall x,\neg \neg \varphi [x\left]\right)$ (setting $\Gamma ={\Theta }_{\omega },P=(\forall x,\neg \neg \varphi [x\left]\right),Q=\varphi \left[c\right]$). Let d be a constant not appearing in $\varphi \left[x\right]$. Now we eliminate the double negation:

$$\frac{\frac{\frac{\frac{}{\varphi \left[d\right]⊢\varphi \left[d\right]}}{\frac{\neg \neg \varphi \left[d\right]⊢\varphi \left[d\right]}{(\forall x,\neg \neg \varphi [x\left]\right)⊢\varphi \left[d\right]}}}{\frac{(\forall x,\neg \neg \varphi [x\left]\right)⊢(\forall x,\varphi [x\left]\right))}{{\Theta }_{\omega },(\forall x,\neg \neg \varphi [x\left]\right)⊢(\forall x,\varphi [x\left]\right)}}\frac{{\Theta }_{\omega }⊢(\forall x,\neg \neg \varphi [x\left]\right)}{{\Theta }_{\omega }⊢(\forall x,\varphi [x\left]\right),(\forall x,\neg \neg \varphi [x\left]\right)}}{{\Theta }_{\omega }⊢(\forall x,\varphi [x\left]\right)}$$

So P is true and provable in $T_{\omega }$, as desired.

We have handled all cases by now. By induction, every closed sentence is true in M if and only if it is provable in $T_{\omega }$. Now consider some axiom of T. Clearly, it is provable in $T_{\omega }$. So it is true in M. Therefore, M really is a model of T (and indeed, of $T_{\omega }$).

Conclusion

Let's summarize the argument. We start with a first-order theory T and a proposition P. Since the sequent rules are sound, if T proves P, then P is true in all models of T. Suppose instead that T does not prove P. Then we create a modification of T with the additional axiom that $\neg P$, which remains consistent. Then we extend this to a consistent Henkin theory. We further extend the Henkin theory to be complete in the sense that for any proposition, the theory proves it or its negation. It is now straightforward to derive a model from the complete theory, by looking at what it proves about closed atomic propositions, and check that it is indeed a model by induction. This demonstrates the existence of a model of T in which P is false. Contrapositively, if P is true in all models of T, then T proves it.

If we wish to have equality in the theory, we introduce an equality predicate and axioms. The model will give truth values for the equality predicate (saying which terms are equal), and assign truth values to predicates in a way consistent with the equalities. It is now possible to construct equivalence classes of terms according to the equality predicate, to get a proper model of a first-order theory with equality. (I have skipped presenting the details of this construction.)

While it is non-standard to prove a universal $\forall x,\varphi \left[x\right]$ from its instantiation with a constant rather than a variable, it is difficult to prove the Henkin extension consistent without doing this. Generally, this means free variables are avoided in preference to constants. While it is inelegant to expand the theory to contain a countable infinite set of constants used in no axioms, it does not seem to be a major problem semantically or proof-theoretically.

I have previously shown that a consistent guessing oracle can create a propositional model (as in an assignment of truth values to sentences consistent with axioms) of a consistent first-order theory. While I have not shown it in this post, under some additional assumptions, I believe it is possible to create a first-order model of a first-order theory (without equality) using a consistent guessing oracle if the axioms of the theory are recursively enumerable. This is because the step of extending the Henkin theory to a complete theory can be done with a consistent guessing oracle, as with propositional models of first-order theories.

My current understanding of sequent calculus is that, other than the structural rules of cut and weakening and the left universal rule, all rules of sequent calculus are complete in addition to being sound, in that if a judgment is provable, it is provable by first applying the rule and then proving its top judgments (assuming the rule applies at all). The cut and weakening rules are relatively unproblematic, as cut and weakening can in general be eliminated. The left universal rule has two problems: it might need to be used more than once on the same universal, and it requires instantiating the universal with a specific term, whereas the domain of discourse may have elements that cannot be written as terms. The Henkin construction largely handles the second problem.

Studying Henkin theories may be illuminating for understanding non-standard models of first-order theories such as Peano Arithmetic and ZFC. The Henkin construction means there is a constant satisfying any predicate $\varphi$ whenever $\exists x,\varphi \left[x\right]$ is true. Non-standard models of Peano arithmetic can be understood as assigning non-standard numbers (that is, ones that cannot be reached by iterating the successor function on zero) to these Henkin constants.