\chapter{Completeness}

We now aim to establish a complete proof-system for first-order
logic.  The result is Theorem~\ref{thm:completeness} on
p.~\pageref{thm:completeness}.  The proof of this theorem follows the
pattern of our proof of Compactness.

First-order logic is based on propositional logic.  It will be useful
to have a general description of \tech{logics} that encompasses both
propositional and first-order logic.  So, this is where we begin.  All
sections following \S~\ref{sect:1st} concern first-order logic, unless
otherwise noted.

There are a few exercises, on
pp.~\pageref{ex1},
\pageref{ex2},~\pageref{ex3},~\pageref{ex4},~\pageref{ex5},~\pageref{ex6}
and~\pageref{ex7}. 

\section{Logic in general}

A logic has an \defn{alphabet},
which is just a certain non-empty set; the members of this set can be
called the \defn{symbols} of the logic.  These symbols can be put
together to form \defn{strings}.  If we want a formal definition, we
can say that such a string is a \defn{finite, non-empty sequence} of
symbols of the logic;
that is, the string is a function $k\mapsto s_k$ from
$\{0,1,\dots,n\}$ into the alphabet, for some $n$ in $\varN$.  We
usually write this function as
\begin{equation*}
  s_0s_1\dotsb s_n;
\end{equation*}
this the result of \defn{juxtaposing} the symbols $s_k$ in the
prescribed order.
Such a string has \defn{sub-strings}, namely the strings
\begin{equation*}
  s_\ell s_{\ell+1}\dotsb s_{m},
\end{equation*}
where $0\leq \ell\leq m\leq n$; the sub-string is \defn{proper} if
$0<\ell$ or $m<n$.
Certain strings will be \tech{formulas} of the logic.  In particular,
certain strings will be \defn{atomic} formulas.  Some \defn{rules of
  construction} are specified
for converting certain finite sets of strings into other strings.
Then a \defn{formula} of the logic is a member of the smallest set $X$ of
strings such that:
\begin{mylist}
  \item
all atomic formulas are in $X$; and
\item
$X$ contains
every string that results from applying a rule of construction to a
set of elements of $X$.
\end{mylist}
Hence
properties of all formulas can be proved by \tech{induction}.

Moreoever, it is required that, for every formula that is not atomic,
there is exactly one rule of construction and one set of formulas such
that the original formula results from applying that rule to that set.
This is the principle of \defn{uniquely readability} as formulas; it
makes possible the
\tech{recursive} definition of functions on the set of formulas.


For any logic,
a \defn{proof-system} consists of:
\begin{mylist}
  \item
\defn{axioms}, which are just certain formulas of the logic;
\item
\defn{rules of inference}, that is, ways of inferring certain formulas
from certain \emph{finite} sets of formulas.
\end{mylist}
So the notions of \tech{axiom} and \tech{rule of inference} are
parallel to the notions of \tech{atomic formula} and \tech{rule of
  construction}.  However, in a proof-system, there is no requirement
corresponding to unique readability.

Let $\psys S$ be proof-system.
A \defn{deduction} or \defn{formal proof in $\psys S$ of} the formula
$\phi$ \defn{from} the set $\Phi$ of formulas is a sequence
\begin{equation*}
  \psi_0,\dots,\psi_n
\end{equation*}
of formulas where $\psi_n$ is $\phi$, and for each $k$
such that $k\leq n$, one of the following holds:
\begin{mylist}
  \item
$\psi_k\in\Phi$, or
\item
$\psi_k$ is an axiom of $\psys S$, or 
\item
$\psi_k$ follows from some subset of $\{\psi_j:j<k\}$ by one of the
rules of inference of $\psys S$.  
\end{mylist}
To denote that such a deduction
exists, we can write
\begin{equation*}
  \Phi\proves [S]\phi.
\end{equation*}
Then we can say that $\phi$ is \defn{deducible} from $\Phi$ in $\psys
S$. 
In case $\Phi$ is empty, we can just write
\begin{equation*}
  \proves[S]\phi,
\end{equation*}
and we can call $\phi$ a \defn{theorem} of $\psys S$.

Here are some basic facts:

\begin{lemma}\label{lem:gen}
\mbox{}  
\begin{mylist}
  \item
Every non-empty initial segment of a deduction is also
a deduction;
\item
if $\Phi\proves[S]\phi$ and
$\Phi\included\Phi^*$, then $\Phi^*\proves[S]\phi$;
\item
if $\Phi\proves[S]\phi$, then $\Phi_0\proves[S]\phi$ for some
\emph{finite} subset $\Phi_0$ of $\Phi$;
\item
if $\Phi\proves[S]\psi$ for each $\psi$ in $\Psi$, and
$\Psi\proves[S]\chi$, then $\Phi\proves[S]\chi$.
\end{mylist}
\end{lemma}

\begin{proof}
  \textbf{Exercise.}\label{ex1}
\end{proof}

\section{Propositional logic}

We shall work here with the propositional logic whose alphabet
consists of: 
\begin{mylist}
  \item
the propositional variables $P_k$, where $k\in\varN$; 
\item
the connectives $\lnot$ and $\to$; 
\item
the left bracket $($ and the right bracket $)$.
\end{mylist}
 The atomic formulas are then the propositional variables.  There are
 two rules of construction:
 \begin{mylist}
   \item
From the string $A$, construct $\lnot A$.
\item
From the strings $A$ and $B$, construct $(A\to B)$.
 \end{mylist}
Note that the same formula might be both $(A\to B)$ and $(C\to D)$ for
some \emph{strings} $A$, $B$, $C$ and $D$ such that $A$ is not $C$.
But if all of these strings are \emph{formulas}, then (as one can
prove) $A$ must be $C$.  We use $F$ and $G$ and $H$ as syntactical
variables for propositional formulas.

In propositional logic, there is a notion of \defn{truth}, which we
can develop as follows.
If $S\included\varN$, let $2^S$ be the set of
functions from $S$ to $2$.
We can consider $2$ as the universe of the field $\F_2$; then a
ring-structure on $2^S$ is induced.
If $F$ is a propositional formula, and all variables
appearing in $F$ are in $S$, then there is a function $\hat F$ from
$2^S$ into $2$, as given by the following recursive definition:
\begin{mylist}
  \item
If $F$ is $P_k$, then $\hat F(\alpha)=\alpha(k)$ for all
$\alpha$ in $2^{\varN}$.
\item
If $F$ is $\lnot G$, then $\hat F=1+\hat G$.
\item
If $F$ is $(G\to H)$, then $\hat F=1+\hat G\cdot(1+\hat H)$.
\end{mylist}
Suppose $S$ is the set of variables actually appearing in $F$, and
$\hat F(\alpha)=1$ for all $\alpha$ in $2^S$; then $F$ is called a
\defn{tautology}. 

An element $\alpha$ of $2^{\varN}$ can be called a \defn{structure}
for propositional logic.  (Alternatively, the set
$\{P_n:\alpha(n)=1\}$ can be called the structure; each one determines
the other.)  Then a formula $F$ is \defn{true in} $\alpha$
if $\hat F(\alpha)=1$.  
If every formula in a set $\Phi$ of formulas is true in a structure $\alpha$,
then $\alpha$ is a \defn{model} of $\Phi$.  If $F$ is true in every
model of $\Phi$, 
 then we say that
$F$ is a \defn{logical consequence} of $\Phi$, or that $\Phi$
\defn{entails} $F$, and we write
\begin{equation*}
  \Phi\models F.
\end{equation*}
  A formula $F$ is \defn{valid}, or is a \defn{validity}, if it is true
in all structures; in that case, we write
\begin{equation*}
  \models F.
\end{equation*}

A proof-system $\psys S$ for propositional logic is called:
\begin{mylist}
\item
\defn{sound}, if
  $\Phi\models\phi$
whenever $\Phi\proves[S]\phi$;
\item
\defn{complete}, if $\Phi\proves[S]\phi$
whenever $\Phi\models\phi$.
\end{mylist}


\begin{lemma}\label{lem:sound}
  Let $\psys S$ be a proof-system for propositional logic.  Then
  $\psys S$ is sound 
  if and only if:
  \begin{mylist}
    \item
each axiom of $\psys S$ is valid;
\item
$\Phi\models\phi$ whenever $\phi$ can be inferred from $\Phi$
  by one of the rules of inference of $\psys S$.
  \end{mylist}
\end{lemma}

\begin{proof}
  Suppose $\psys S$ is sound.  If $\phi$ is an axiom of $\psys S$,
  then the one-term sequence $\phi$ is a deduction of $\phi$ from
  $\emptyset$, so $\proves [S]\phi$ and therefore $\models\phi$.
Suppose, instead, that $\phi$ can be inferred from $\Phi$ by one of the
  rules of inference of $\psys S$.  Then $\Phi$ is a finite set
  $\{\psi_0,\dots,\psi_{n}\}$, so the sequence
  \begin{equation*}
    \psi_0,\dots,\psi_n,\phi
  \end{equation*}
is a deduction of $\phi$ from $\Phi$ in $\psys S$.  Hence
$\Phi\proves[S]\phi$, and therefore $\Phi\models\phi$.

The converse is proved by induction on the lengths of deductions.
Suppose that each axiom of $\psys S$ is valid, and
$\Phi\models\phi$ whenever $\phi$ can be inferred from $\Phi$
  by one of the rules of inference of $\psys S$.  As an inductive
  hypothesis, suppose $\Phi\models\phi$ whenever $\phi$ has a
  deduction in $\psys S$ from $\Phi$ of length less than $n+1$.  Now
  say the sequence
  \begin{equation*}
    \psi_0,\dots,\psi_{n-1},\phi
  \end{equation*}
of length $n+1$ is a deduction in $\psys S$ from $\Phi$.  If
$\phi\in\Phi$, then
$\Phi\models\phi$ trivially.  If $\phi$ is an axiom of $\psys
S$, then $\models\phi$ by assumption, so $\Phi\models\phi$.  The
remaining possibility is that $\phi$ can be
inferred from some subset $\Gamma$ of $\{\psi_k:k<n\}$ by a
rule of inference of $\psys S$.  Then $\Gamma\models\phi$ by
assumption.  Also, $\Phi\models\psi_k$ for each $\psi_k$ in $\Gamma$
by inductive hypothesis, since each $\psi_k$ has a proof from $\Phi$
of length $k+1$, namely 
\begin{equation*}
  \psi_0,\dots,\psi_k.  
\end{equation*}
Hence every model of
$\Phi$ is a 
model of $\Gamma$, and so $\phi$ is true in this model; that is,
$\Phi\models\phi$. 
\end{proof}

Let us also note that if a proof-system is complete, then so is every
proof-system obtained by addition of new axioms or rules of inference.





In the only proof-system for first-order logic
that we shall consider,
\begin{mylist}
  \item
the axioms are just the tautologies;
\item
the only rule of inference is \emph{modus ponens}, that is, $G$ can be
inferred from $\{F,(F\to G)\}$.
\end{mylist}
If, in this system, $F$ is deducible from the set $\Phi$ of formulas,
then we can just write 
\begin{equation*}
  \Phi\proves F
\end{equation*}
(since we shall consider no other proof-systems for propositional
logic).  
We have proved (in class) that this system is sound and complete.

\section{First-order logic}\label{sect:1st}

The foregoing notions in propositional logic generalize to first-order
logic.  
For us, the alphabet for a first-order logic will consist of:
\begin{mylist}
  \item
the symbols in a signature $\lang$ for the logic;
\item
individual variables $v_k$, where $k\in\varN$;
\item
the Boolean connectives $\lnot$ and $\to$;
\item
the quantifier $\exists$;
\item
the brackets $($ and $)$.
\end{mylist}
The set of formulas of the resulting logic can be denoted
\begin{equation*}
  \Fmla.
\end{equation*}
Certain formulas are \tech{sentences}; the set of them is
\begin{equation*}
  \Sn.
\end{equation*}
We do not have proof by induction on this set, since sentences can be
constructed from formulas that are not sentences.  However, we can
still define
proof-systems for $\Sn$.  (Alternatively, we could define a
proof-system for $\Fmla$.)

There are \defn{$\lang$-structures} $\str A$, and then for each
sentence $\sigma$ of $\lang$, there is an element $\sigma^{\str A}$ of
$2$.  Then $\sigma$ is \defn{true in} $\str A$ if $\sigma^{\str A}=1$.
The notions of \defn{model},
\defn{entailment}, \defn{validity}, \defn{soundness} and
\defn{completeness} can now be defined as for propositional logic.
Hence we have Lemma~\ref{lem:sound} for $\Sn$ in addition to
propositional logic.

To \emph{prove} that a certain proof-system for $\Sn$ is complete, we
shall use the method
first expounded by Leon Henkin, in \cite{MR0033781}.  (Henkin's proof
was a part of his doctoral thesis; see \cite{MR1396852}.  We have
already used Henkin's method to prove Compactness.)  The
particular treatment in these notes owes something to Shoenfield's in
\cite{MR0225631}.  I introduce the notions of \tech{tautological} and
\tech{deductive} completeness  merely to make our ultimate
proof-system seem natural. 

If $F$ is an $n$-ary formula $F(P_0,\dots,P_{n-1})$ of propositional
logic, and $\sigma_k\in\Sn$,
then by substitution we can form the sentence
\begin{equation*}
  F(\sigma_0,\dots,\sigma_{n-1})
\end{equation*}
of $\lang$.
If $F$ is a tautology, then $F(\sigma_0,\dots,\sigma_{n-1})$ can be
called a \defn{tautology} of $\Sn$.

\begin{lemma}\label{lem:validities}
  Tautologies of $\Sn$ are validities.
\end{lemma}

\begin{proof}
We can prove by induction on propositional formulas $F$ that, if $F$
is $F(P_0,\dots,P_{n-1})$, then for all sentences 
$\sigma_k$ of $\Sn$, and all $\lang$-structure $\str A$,
\begin{equation*}
  F(\sigma_0,\dots,\sigma_{n-1})^{\str A}=\hat F(\sigma_0{}^{\str
  A},\dots,\sigma_{n-1}{}^{\str A}).
\end{equation*}
(Details are an \textbf{exercise}.\label{ex2})  The claim follows immediately
from this. 
\end{proof}

\section{Tautological completeness}

Suppose $\psys S$ is a proof-system for $\Sn$ such that, if
 $F_0$, \dots, $F_k$ are $n$-ary {propositional}
 formulas, and
 \begin{equation}\label{eqn:prop-ent}
   \{F_0,\dots,F_{k-1}\}\models F_k,
 \end{equation}
and $\sigma_0,\dots, \sigma_{n-1}\in\Sn$, then
\begin{equation}\label{eqn:1-ent}
\{F_0(\sigma_0,\dots,\sigma_{n-1}),\dots,
  F_{k-1}(\sigma_0,\dots,\sigma_{n-1})\}\proves[S]
  F_k(\sigma_0,\dots,\sigma_{n-1});
\end{equation}
let us say then that  $\psys S$ is \defn{tautologically complete}.



\begin{lemma}\label{lem:1}
  Let $\psys S$ be a proof-system for $\Sn$.  Then $\psys S$ is
  tautologically complete if and only if:
  \begin{mylist}
    \item
  $\proves[S]\sigma$ for all tautologies $\sigma$ of $\Sn$, and 
\item
$\{\sigma,\sigma\to\tau\}\proves[S]\tau$
for all $\sigma$ and $\tau$ in $\Sn$.
  \end{mylist}
\end{lemma}

\begin{proof}
If $\psys S$ is tautologically complete, then immediately all
tautologies are theorems; the other condition follows since
$\{P_0,P_0\to P_1\}\models P_1$. 

To prove the converse, we can use our complete proof-system for
propositional logic:  Suppose we have \eqref{eqn:prop-ent} above.
Then $F_k$ has a a formal proof from $\{F_0,\dots,F_{k-1}\}$.  Say
this proof is
\begin{equation*}
  G_0,\dots,G_m.
\end{equation*}
Then $G_m$ is $F_k$.  We proceed by induction on $m$.  
There are three possibilities:
\begin{mylist}
  \item
If $F_k\in\{F_0,\dots,F_{k-1}\}$, then trivially \eqref{eqn:1-ent}
follows.
\item
If $F_k$ is a tautology, then
$\proves[S]F_k(\tuple{\sigma})$ by assumption, so
\eqref{eqn:1-ent}. 
\item
If $G_j$ is $(G_i\to F_k)$ for some $i$ and $j$ in $m$, then, by
inductive hypothesis, we have
\begin{align*}
\{F_0(\tuple{\sigma}),\dots,
  F_{k-1}(\tuple{\sigma})\}&\proves[S]
  G_i(\tuple{\sigma});\\
\{F_0(\tuple{\sigma}),\dots,
  F_{k-1}(\tuple{\sigma})\}&\proves[S]
  G_j(\tuple{\sigma});
\end{align*}
hence \eqref{eqn:1-ent} by assumption (and Lemma~\ref{lem:gen}).  
\end{mylist}
In all cases then, \eqref{eqn:1-ent} follows.
\end{proof}

It should be clear that a complete proof-system is tautologically
complete.  The converse fails:

\begin{example}
  The proof-system in which all tautologies are axioms and
  \emph{modus ponens} is the only rule of inference is not complete,
  since it cannot be used to prove the validity $\Exists x x=x$.
  Indeed, the
  theorems of this proof-system are just the tautologies (as one can
  show); but $\Exists xx=x$ is not a tautology.
\end{example}

Let $\bot$ be the negation of a tautology, say
\begin{equation*}
  \lnot(\Exists xx=x\to\Exists xx=x).
\end{equation*}
Henceforth, let $\Sigma\included\Sn$ and $\sigma\in\Sn$.

\begin{lemma}\label{lem:2}
  In a tautologically complete proof-system $\psys S$, the following are
  equivalent:
  \begin{mylist}
    \item
$\Sigma\proves\lnot\sigma$ for some $\sigma$ in $\Sigma$;
\item
$\Sigma\proves\sigma$ and $\Sigma\proves\lnot\sigma$ for some $\sigma$
  in $\Sn$;
\item
$\Sigma\proves\sigma$ for every $\sigma$ in $\Sn$;
\item
$\Sigma\proves\bot$.
  \end{mylist}
\end{lemma}

\begin{proof}
  \textbf{Exercise.}\label{ex3}  (There is a corresponding lemma for
  propositional 
  logic.)
\end{proof}

If $\Sigma\proves[S]\bot$, then $\Sigma$ is
\defn{inconsistent} in $\psys S$; otherwise, it is \defn{consistent}.

\begin{lemma}
  In a complete proof-system, every consistent subset of
  $\Sn$ has a model.
\end{lemma}

\begin{proof}
  If $\psys S$ is complete, but $\Sigma$ has no model, then
  $\Sigma\models\bot$, so
  $\Sigma\proves[S]\bot$ by completeness, so $\Sigma$ is inconsistent. 
\end{proof}

The converse of the lemma may fail, even if the proof-system is
required to be tautologically complete:

\begin{example}
  Let the axioms of a proof-system $\psys S$ be the tautologies, and
  let the
  rules of inference be \emph{modus ponens}, along with the rule that
  $\bot$ can be inferred from every finite set that has no model.
  (Note however that this is not a \emph{syntactical} rule: it is not
  based directly on the form of sentences.)  By
  the Compactness Theorem of first-order logic, \emph{every} set with no
  model is inconsistent in this
  theory; therefore all consistent sets have models.  However,
  the validity $\Exists xx=x$ is not a theorem of~$\psys S$.
  (\textbf{Exercise:}\label{ex4} show this.)
\end{example}

\section{Deductive completeness}

Let a proof-system $\psys S$ be called \defn{deductively complete} if
$\Sigma\proves[S](\sigma\to\tau)$ whenever
$\Sigma\cup\{\sigma\}\proves[S]\tau$. 

\begin{lemma}\label{lem:4}
  A tautologically and deductively complete proof-system in which
  every consistent set has a model is complete.
\end{lemma}

\begin{proof}
Suppose $\psys S$ is such a system,
 and  $\Sigma\cup\{\lnot\sigma\}$ is 
  inconsistent in $\psys S$.  Then
 $\Sigma\cup\{\lnot\sigma\}\proves[S] \sigma$ by 
  Lemma~\ref{lem:2}, so $\Sigma\proves[S](\lnot\sigma\to\sigma)$ by deductive
  completeness.
But $(\lnot\sigma\to\sigma)\to\sigma$ is a tautology, so
  $\Sigma\proves[S]\sigma$ by tautological completeness.  

Therefore, if $\Sigma\not\proves[S]\sigma$, then
 $\Sigma\cup\{\lnot\sigma\}$ is 
  consistent, so it has a model by assumption; this shows
 $\Sigma\not\models\sigma$. 
\end{proof}

\begin{lemma}\label{lem:5}
A tautologically complete proof-system whose only rule of inference is
\emph{modus ponens} is deductively complete.
\end{lemma}

\begin{proof}
\textbf{Exercise.}\label{ex5}  (See the Deduction Theorem of
propositional logic.) 
\end{proof}


\begin{lemma}
  Suppose $\Sigma\included\Sn$ and $\Sigma$ is consistent in a
  tautologically and deductively complete proof-system.
The following are equivalent:
\begin{mylist}
  \item
If $\Sigma\included\Gamma\included\Sn$ and $\Gamma$ is consistent,
then $\Gamma=\Sigma$.
\item
$\lnot\sigma\in\Sigma\Iff\sigma\notin\Sigma$ for all $\sigma$ in
  $\Sn$. 
\end{mylist}
\end{lemma}

\begin{proof}
  \textbf{Exercise.}\label{ex6}
\end{proof}

A set $\Sigma$ meeting one of the conditions in the lemma can be
called \defn{maximally} consistent.

\section{Completeness}

By Lemma~\ref{lem:1}, we know of one tautologically complete
proof-system, namely, 
the system whose axioms are the tautologies, and whose rule of
inference is \emph{modus ponens}.  Let $\psys S$ be this system.  Then
$\psys S$ is deductively
complete, by Lemma~\ref{lem:5}, and is sound, by
Lemmas~\ref{lem:sound} and~\ref{lem:validities}.  Moreover, soundness
and deductive 
completeness are 
preserved if we add new valid
axioms to $\psys S$.  Now we shall see which valid axioms we can add
in order to ensure 
that every consistent set has a model; then we shall have a complete
system by Lemma~\ref{lem:4}. 

We follow the proof of the Compactness Theorem, replacing `finitely
satisfiable'
with `consistent'.  We assume that $\lang$ is countable.  Suppose
$\Sigma$ is a consistent subset of $\Sn$.
We introduce an infinite set $C$ of new constants and enumerate
$\Sn[\lang\cup C]$ as $\{\sigma_n:n\in\varN\}$.  We construct a chain
\begin{equation*}
  \Sigma=\Sigma_0\included\Sigma_1\included\Sigma_2\included\dotsb
\end{equation*}
where
\begin{equation*}
  \Sigma_{2n+1}=
  \begin{cases}
    \Sigma_{2n}\cup\{\sigma_n\},& \text{ if this is consistent;}\\
\Sigma_{2n}, & \text{ otherwise.}
  \end{cases}
\end{equation*}
If $\sigma_n$ is $\Exists x\phi$, and this is in $\Sigma_{2n+1}$, then
we want to define $\Sigma_{2n+2}$ as 
\begin{equation*}
  \Sigma_{2n+1}\cup\{\phi_c^x\},
\end{equation*}
where $c$ is a variable not used in $\Sigma_{2n+1}$.  But we need to
know that this set is consistent.
For this we assume, as axioms of $\psys S$, the sentences
\begin{equation}\label{eqn:axiom-E}
  (\phi_c^x\to\chi)\to\Exists x\phi\to \chi,
\end{equation}
where $c$ is a variable not appearing in $\chi$.  Note that these
axioms are valid.  We now have:

\begin{lemma}
  If $\Gamma$ is consistent and contains $\Exists x\phi$, and $c$ does
  not appear in $\Gamma$, then $\Gamma\cup\{\phi_c^x\}$ is consistent.
\end{lemma}

\begin{proof}
Suppose it's not.  Then 
\begin{equation*}
  \{\psi_0,\dots,\psi_{k-1}\}\cup\{\phi_c^x\}\proves[S]\bot
\end{equation*}
for some $\psi_i$ in $\Gamma$.
By deductive completeness, 
\begin{equation}\label{eqn:to-bot}
 \proves[S] \phi_c^x\to\psi_0\to\dotsb\to\psi_{k-1}\to\bot,
\end{equation}
where the notational convention is that a terminal string
$\chi_0\to\chi_1\to\chi_2$ 
stands for the formula $(\chi_0\to(\chi_1\to\chi_2))$.
We can re-write \eqref{eqn:to-bot} as
\begin{equation}\label{eqn:to-bot-again}
  \proves[S]\phi_c^x\to\chi,
\end{equation}
where $\chi$ is $\psi_0\to\dotsb\to\psi_{k-1}\to\bot$.
Then from \eqref{eqn:axiom-E} we have
\begin{equation*}
  \proves[S]\Exists x\phi\to\chi
\end{equation*}
by \emph{modus ponens}; that is,
\begin{equation*}
\proves[S]  \Exists x\phi\to\psi_0\to\dotsb\to\psi_{k-1}\to\bot.
\end{equation*}
Then $k+1$ applications of \emph{modus ponens} show
\begin{equation*}
  \Gamma\proves[S]\bot,
\end{equation*}
which contradicts the assumption that $\Gamma$ is consistent.
\end{proof}



So now, given a consistent subset $\Sigma$ of $\Sn$, we can construct
a consistent subset $\Sigma^*$ of 
$\Sn[\lang\cup C]$ such that
\begin{mylist}
\item
$\Sigma\included\Sigma^*$;
\item
$\Sigma^*$ is maximally consistent;
  \item
if $(\Exists x\phi)\in\Sigma$, then $\phi_c^x\in\Sigma$ for some $c$
in $C$, that is, $\Sigma^*$ \defn{has witnesses}.
\end{mylist}

As in the proof of Compactness, we want to use $\Sigma^*$ to define a
model $\str A$ of itself.

For the sake of defining the universe of $\str A$, we assume now that
$\psys S$ has the axioms
\begin{gather}\label{eqn:equality}
  c=c,\\ \label{eqn:more-equality}
c=c'\to d=d'\to c=d\to c'=d',
\end{gather}
where $c$, $c'$, $d$ and $d'$ range over $C$.
Let $E$ be the relation
\begin{equation*}
  \{(c,d)\in C^2:(c=d)\in\Sigma^*\}.
\end{equation*}
We can now show:

\begin{lemma}
The relation
$E$ is an equivalence-relation.
\end{lemma}

\begin{proof}
We first show
\begin{gather}\label{eqn:=1}
  \proves[S] c=c,\\ \label{eqn:=2}
\proves[S] c=d\to d=c,\\ \label{eqn:=3}
\proves[S] c=d\to d=e\to c=e
\end{gather}
for all constants $c$, $d$ and $e$ in $C$.

Now, we have \eqref{eqn:=1} trivially by \eqref{eqn:equality}.  An
  instance of 
  \eqref{eqn:more-equality} is
  \begin{equation*}
    c=d\to c=c\to c=c\to d=c;
  \end{equation*}
then \eqref{eqn:=2} follows by tautological completeness.  Another
instance of \eqref{eqn:more-equality} is
\begin{equation*}
  c=c\to d=e\to c=d\to c=e;
\end{equation*}
then \eqref{eqn:=3} follows by tautological completeness.

By its maximal consistency then, $\Sigma^*$ contains $c=c$; and if
$\Sigma^*$ contains $c=d$ and $d=e$, then it contains $d=c$ and $c=e$. 
\end{proof}
We define $A$ to
be $C/E$.  We now define $R^{\str A}$ (for each
$n$-ary predicate $R$ in $\lang$)
as the set
\begin{equation*}
  \{([c_0],\dotsb,[c_{n-1}])\in A^n:  (Rc_0\dotsb
  c_{n-1})\in\Sigma^*\}.
\end{equation*}
Then we have
\begin{equation*}
  (Rc_0\dotsb c_{n-1})\in\Sigma^*\implies
  ([c_0],\dotsb,[c_{n-1}])\in R^{\str A}, 
\end{equation*}
but perhaps not the converse.
Possibly then both
$Rc_0\dotsb c_{n-1}$ and $\lnot Rc_0'\dotsb c_{n-1}'$ are in
$\Sigma^*$, although $(c_k=c_k')\in\Sigma^*$ in each
  case.  To prevent this, as as axioms of $\psys S$ we assume
\begin{equation}\label{eqn:R}
  c_0=c_0'\to \dotsb \to c_{n-1}=c_{n-1}'\to Rc_0\dotsb
  c_{n-1}\to Rc_0'\dotsb c_{n-1}'.
\end{equation}
We now have:

\begin{lemma}
$([c_0],\dotsb,[c_{n-1}])\in R^{\str A}\Iff (Rc_0\dotsb
  c_{n-1})\in\Sigma^*$.
\end{lemma}

\begin{proof}
  \textbf{Exercise.}\label{ex7}
\end{proof}

Finally, suppose $f$ is an $n$-ary function-symbol (where possibly
$n=0$, in which case $f$ is a constant.)  We want
to be able to
define $f^{\str A}$.  (If $c\in C$, then $c^{\str A}=[c]$; but there
might be constants of $\lang$ as well.)  To define $f^{\str A}$, we
first need some lemmas, which are 
based on another axiom: 
\begin{equation}\label{eqn:t}
  \phi_t^x\to \Exists x\phi,
\end{equation}
where $\fv{\phi}\included\{x\}$ and $t$ is a term with no variables.
Let us assume that this is an axiom of $\psys S$.
Then we have:


\begin{lemma}[Substitution]
If $\fv{\phi}\included\{x\}$, and the constant $c$ does not appear in
$\phi$, then
\begin{equation*}
  \proves[S] \phi_c^x\to\phi_t^x
\end{equation*}
for all constant terms $t$.
\end{lemma}

\begin{proof}
We have
  \begin{align*}
    &\proves[S] \lnot\phi_t^x\to\Exists x\lnot \phi, &&\text{[by
    \eqref{eqn:t}]}\\ 
&\proves[S] \lnot\Exists x\lnot\phi\to\phi_t^x, &&\text{[by tautological
    completeness]}\\
&\proves[S] (\lnot\phi_c^x\to\bot)\to\Exists
    x\lnot\phi\to\bot,&&\text{[by \eqref{eqn:axiom-E}]}\\
&\proves[S] \phi_c^x\to\lnot\Exists x\lnot \phi,&&\text{[by tautological
    completeness]}
  \end{align*}
and hence
$\proves[S] \phi_c^x\to\phi_t^x$ by \emph{modus ponens}.
\end{proof}

\begin{lemma}
  $\proves[S] t=t$ for all terms $t$. 
\end{lemma}

\begin{proof}
  We have
  \begin{align*}
    &\proves[S] c=c,&&\text{[by \eqref{eqn:equality}]}\\
&\proves[S] c=c\to t=t,&&\text{[by the Substitution Lemma]}
  \end{align*}
and hence
$\proves[S] t=t$ by \emph{modus ponens}.
\end{proof}

\begin{lemma}
  $\proves[S] \Exists xfc_0\dotsb c_{n-1}=x$.   
\end{lemma}

\begin{proof}
  We have
  \begin{align*}
  &  \proves[S] fc_0\dotsb c_{n-1}=fc_0\dotsb c_{n-1},&&\text{[by the
  last lemma]}\\
&\proves[S] fc_0\dotsb c_{n-1}=fc_0\dotsb c_{n-1}\to \Exists x fc_0\dotsb
  c_{n-1}=x, &&\text{[by \eqref{eqn:t}]}
  \end{align*}
hence
$\proves[S] \Exists xfc_0\dotsb c_{n-1}=x$ by \emph{modus ponens}.
\end{proof}


Finally, we assume as axioms of $\psys S$ the sentences
\begin{equation}\label{eqn:f}
  c_0=c_0'\to\dotsb\to c_{n-1}=c_{n-1}'\to fc_0\dotsb
c_{n-1}=fc_0'\dotsb c_{n-1}'.
\end{equation}
This enables us to define $f^{\str A}$:

\begin{lemma}
  For each $n$-ary function-symbol $f$, there is an $n$-ary operation
  $f^{\str A}$ on $A$ given by
\begin{equation}\label{eqn:function}
  f^{\str A}([c_0],\dots,[c_{n-1}])=[d]\Iff (fc_0\dotsb
  c_{n-1}=d)\in\Sigma^*. 
\end{equation}
\end{lemma}

\begin{proof}
Since $\Sigma^*$ is maximally consistent, we now have
\begin{equation*}
  \Exists xfc_0\dotsb c_{n-1}=x\in\Sigma^*.
\end{equation*}
Since $\Sigma^*$ has witnesses, we have
\begin{equation*}
  fc_0\dotsb c_{n-1}=d\in\Sigma^*
\end{equation*}
for some constant $d$.  This gives us a value for $f^{\str
  A}([c_0],\dotsb,[c_{n-1}])$; we have to show that this value is
  unique.  For this, it is enough to show
\begin{multline*}
  \proves[S] c_0=c_0'\to\dotsb\to c_{n-1}=c_{n-1}'\to \\d=d'\to fc_0\dotsb
c_{n-1}=d\to fc_0'\dotsb c_{n-1}'=d'
\end{multline*}
for all $c_k$ and $c_k'$ and $d$
and $d'$ in $C$.  By \eqref{eqn:f} and tautological completeness, it
is enough to show
\begin{equation*}
  \proves[S] fc_0\dotsb c_{n-1}=fc_0'\dotsb c_{n-1}'\to d=d'\to
  fc_0\dotsb c_{n-1}=d\to fc_0'\dotsb c_{n-1}'=d'.
\end{equation*}
In the axiom \eqref{eqn:more-equality}, we may assume that $c$ is not
one of the variables $c'$, $d$ or 
$d'$. Then by the
Substitution Lemma, we have
\begin{equation*}
  \proves[S]fc_0\dotsb c_{n-1}=c'\to d=d'\to fc_0\dotsb c_{n-1}=d\to c'=d'.
\end{equation*}
We may also assume that $c'$ is not one of the variables $c_k$, $d$ or
$d'$.  Applying the Substitution Lemma again gives what we want.
\end{proof}

The structure $\str A$ is now determined and is a model of $\Sigma$,
by the proof of the Compactness Theorem.
In sum, what we have shown is:

\begin{theorem}[Completeness for first-order logic]\label{thm:completeness}
  That proof-system for $\Sn$ is complete whose only rule of inference
  is \emph{modus ponens}, and whose axioms are the following:
  \begin{mylist}
    \item
the tautologies;
\item
$(\phi_c^x\to\chi)\to\Exists x\phi\to \chi$, where
  $c$ does not appear in $\chi$;
\item
$c=c$;
\item
$c=c'\to d=d'\to c=d\to c'=d'$;
\item
$c_0=c_0'\to\dots c_{n-1}=c_{n-1}'\to Rc_0\dotsb c_{n-1}\to
  Rc_0'\dotsb c_{n-1}'$;
\item
$\phi_t^x\to\Exists x\phi$;
\item
$c_0=c_0'\to\dotsb\to c_{n-1}=c_{n-1}'\to fc_0\dotsb
  c_{n-1}=fc_0'\dotsb c_{n-1}'$.
  \end{mylist}
Here the notation is as follows:
\begin{myitem}
\item
$x$ is a variable;
  \item
$\phi$ is a formula such that $\fv{\phi}\included\{x\}$; 
\item
$\chi$ is a sentence;
\item
$t$ is a constant term;
\item
  $c$, $c'$, $c_k$, $c_k'$, $d$ and $d'$ are constants; 
\item
$n\in\varN$;
\item
  $R$ is an $n$-ary predicate if $n>0$; and 
\item$f$ is an $n$-ary
  function-symbol (or a constant, if $n=0$).
\end{myitem}
\end{theorem}