% LaTex2e
\documentclass[12pt]{article}
\usepackage{amssymb,latexsym}

\def\moda{{\mathfrak A}}
\def\rr{{\mathbb R}}
\def\aa{{\mathbb A}}
\def\cc{{\mathbb C}}
\def\qq{{\mathbb Q}}
\def\nn{{\mathbb N}}
\def\zz{{\mathbb Z}}
\def\famf{{\mathcal F}}
\def\famc{{\mathcal C}}
\def\ll{{\mathcal L}}
\def\proves{\vdash}
\def\rmiff{\mbox{ iff }}
\def\rmand{\mbox{ and }}
\def\rmor{\mbox{ or }}
\def\define{\par\noindent{\bf Definition}: }
\newtheorem{theorem}{Theorem} %[section]
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{lemma}[theorem]{Lemma}

\def\res{{\upharpoonright}}
\def\qed{{\par\noindent $\Box$}\par}

\def\proof{{\par\noindent proof:\par}}

\def\disj{\vee}
\def\conj{\wedge}
\def\implies{\to}
\def\iff{\leftrightarrow}

\def\axiom#1{{\par\bigskip \bf #1\par\bigskip}}

\begin{document}

\begin{flushright}
  A.Miller\\
M571\\
Spring 2002
\end{flushright}

\begin{center}
  G\"odel's Completeness Theorem
\end{center}

We only consider countable languages $\ll$ for first order logic
with equality which have only predicate symbols and constant symbols.
We regard the symbols ``$\exists x$''' as an abbreviation for
``$\neg\forall x\neg $'' or vice-versa if you prefer.


\axiom{Propositional Tautologies}

We take all propositional tautologies as Logical Axioms. For
example, for any $\ll$-formula $\theta$ the formula
 $$(\theta\disj\neg\theta)$$
is a logical axiom. More generally, for any proposition tautology we replace
the propositional letters with $\ll$-formulas and get a Logical Axiom.

\bigskip

The other axioms are axiom schemas, i.e, all formulas of a certain
syntactical form.

\axiom{Equality Axioms}

All formulas of the form:

$u=u$

$u=v\implies v=u$

$(u=v\conj v=w)\implies u=w$

\noindent $(u_1=v_1\conj u_2=v_2 \conj\cdots\conj u_n=v_n)\implies
(R(u_1,u_2,\ldots,u_n)\iff R(v_1,v_2,\ldots,v_n))$

are Logical Axioms. Here $u,v,w,u_i,v_i$ are terms, i.e., either variables or
constant symbols in any mix and $R$ is an $n$-ary predicate symbol.


\axiom{Substitution Axioms}

For any formula $\theta(x)$ and constant symbol $c$ the
axiom:

$$(\forall x\theta(x))\implies \theta(c)$$

where $\theta(c)$ is the formula which results from substituting
$c$ for all free occurrences of $x$ in $\theta(x)$.

And the axiom:
$$(\forall x\theta(x))\implies \theta(y)$$
where $y$ is variable that does not occur in $\theta(x)$ at all.

\axiom{Henkin Axioms}

These aren't in Enderton, so we probably don't need them.
However they make the proof of Lemma \ref{Henkin}
easier so why not add them.
For any formula $\theta(x)$ and variable $y$ which doesn't occur
in $\theta(x)$ at all we have the axiom:

$$\exists y[(\exists x\theta(x))\implies \theta(y)]$$

\axiom{Generalization Axioms}

These axioms are used to prove a weak form of the generalization Lemma (see
the Claim in the proof of Lemma \ref{Henkin}). They are needed because we
have not taken Generalization as a proof rule.  Which on the other hand
makes the Deduction Lemma easier to prove.

For all formulas $\theta$ and $\psi$ and variables $x$ the following is a
logical axiom:

$$[\forall x (\theta(x)\implies\psi(x))]\implies
[(\forall x\theta(x)) \implies(\forall x \psi(x))]$$

and for all formulas $\rho$ and variables $y$ such that
$y$ does not occur in $\rho$ at all (free or bound) the
axiom:
$$\rho \implies \forall y \rho$$

Finally, (like Enderton) for any Logical Axiom  we can and put as
many $\forall x_1\forall x_2..$ as we want in front of it
and we get another Logical
Axiom. This concludes our list of logical axioms.

\newpage

\begin{center}
 Summary of the Logical Axioms
\end{center}


(P) All propositional tautologies

\medskip
(E1) $u=u$

(E2) $u=v\implies v=u$

(E3) $(u=v\conj v=w)\implies u=w$

(E4)$(u_1=v_1\conj \cdots\conj u_n=v_n)\implies
(R(u_1,u_2,\ldots,u_n)\iff R(v_1,v_2,\ldots,v_n))$

\hspace{1in} $u,v,w,u_i,v_i$ are terms (constant symbols or variables)

\medskip
(S1) $(\forall x\theta(x))\implies \theta(c)$ where $c$ constant symbol

(S2) $(\forall x\theta(x))\implies \theta(y)$
where $y$ is a variable that does not occur in $\theta(x)$

\medskip
(H) $\exists y[(\exists x\theta(x))\implies \theta(y)]$ for any variable
$y$ that
does not occur in $\theta(x)$

\medskip
(G1) $[\forall x (\theta(x)\implies\psi(x))]\implies
[(\forall x\theta(x)) \implies(\forall x \psi(x))]$

(G2) $\rho \implies \forall y \rho$ where $y$ does not occur $\rho$

(G3) If $\theta$ any Logical Axiom, so is $\forall x\theta$

\bigskip
\define For $\Sigma$ a set of $\ll$-sentences and
$\theta$ a $\ll$-formula $\Sigma\proves\theta$ iff there is
a finite sequence of $\ll$-formulas
$\theta_1,\;\theta_2\;\ldots\;\theta_n$ such that
$\theta=\theta_n$ and
each $\theta_k$ is either a logical axiom or member of
$\Sigma$ or follows from previous $\theta_i$ using Modus Ponens.

\bigskip
\define $Th(\Sigma)=\{\theta $ an $\ll$-formula $: \Sigma\proves\theta\}$.

Note that $Th(\Sigma)$ can also be characterized as the smallest family
of $\ll$-formulas which contain $\Sigma\cup$Logical Axioms and is
closed under Modus Ponens.


\bigskip
The Deduction Lemma only depends on the fact that we
have included all propositional tautologies as logical axioms and
that our only proof rule is Modus Ponens.

\begin{lemma}
 (Deduction Lemma)  For any set $\Sigma\cup\{\theta\}$ of $\ll$-sentences
and $\psi$ an $\ll$-formula
$$\Sigma \proves \theta\implies\psi \;\;\;\;\rmiff \;\;\;\;
\Sigma \cup \{\theta\} \proves \psi$$
\end{lemma}
\proof

\noindent The direction $\rightarrow$ is easy from Modus Ponens.

\noindent For the direction $\leftarrow$ we prove it by showing
that the set of all $\psi$ such that
$$\Sigma \proves \theta\implies\psi$$
contains $\Sigma\cup\{\theta\}\cup$Logical Axioms and is closed
under Modus Ponens.

(1) Given $\psi$ note that $\psi\implies(\theta\implies\psi)$
is a propositional tautology. Hence if $\psi\in\Sigma$ or
if $\psi$ is a logical axiom, then
$\Sigma\proves \theta\implies\psi$
by using Modus Ponens.

(2)
Note that
$$(\theta\implies\psi_1)\implies [ (\theta\implies(\psi_1\implies\psi_2))
\implies(\theta\implies\psi_2)]$$
is a propositional tautology.
Hence if
$\Sigma \proves \theta\implies\psi_1$
and
$\Sigma \proves \theta\implies(\psi_1\implies\psi_2)$
then by two uses of Modus Ponens,
$\Sigma\proves \theta\implies\psi_2$.

\bigskip
It follows from (1) and (2) that:
$$Th(\Sigma\cup\{\theta\})\subseteq \{\psi\;:\;\Sigma
\proves \theta\implies\psi \}$$

\qed

\define $\Sigma$ is an inconsistent set of $\ll$-sentences iff
$\Sigma\proves\#$ where $\#$ is some propositional contradiction,
for example, $\#$ could be
$$\#\;\;=\;\;P\conj\neg P\;\;=\;\;(\exists x\;\;x=x)\conj\neg(\exists x\;\; x=x)$$


\define $\Sigma$ is consistent iff $\Sigma$ is not inconsistent.

Note that since $(\#\implies\theta)$ is a propositional tautology for any
formula $\theta$, by Modus Ponens, if $\Sigma\proves\#$ then $\Sigma$ proves
$\theta$.  Hence inconsistent $\Sigma$ prove everything, i.e.,
$Th(\Sigma)$ is the set of all $\ll$-formulas.  An equivalent definition
of $\Sigma$ is inconsistent is that for some $\ll$-formula $\theta$
both $\Sigma\proves\theta$ and $\Sigma\proves\neg\theta$.  This
is because $\theta\implies(\neg\theta\implies\#)$ is a propositional
tautology and therefor by Modus Ponens twice $\Sigma\proves\#$.

The next couple of lemmas only use the deduction lemma.

\begin{lemma} \label{complete}
  The following two forms of the completeness theorem are equivalent:

\noindent (a) For every set $\Sigma\cup\{\theta\}$ of $\ll$-sentences
\par if every model of $\Sigma$ is a model of $\theta$, then
$\Sigma\proves\theta$.

\noindent (b) Every consistent set $\Gamma$ of $\ll$-sentences has a model.
\end{lemma}

\proof
Suppose (a).  If $\Gamma$ has no model, then every model of
$\Gamma$ is a model of $\#$. But then $\Gamma\proves\#$, hence
it is inconsistent.

Suppose (b) and every model of $\Sigma$ is a model of
$\theta$.  Then $\Gamma=\Sigma\cup\{\neg\theta\}$ has no
model and so is inconsistent by (b).
Hence $\Gamma=\Sigma\cup\{\neg\theta\}\proves \#$.

Now according to the deduction lemma:

$$\Sigma\proves (\neg\theta\implies\#)$$

But $(\neg\theta\implies\#)\implies \theta$ is a propositional
tautology.  So by Modus Ponens
$$\Sigma\proves \theta$$
\qed

The above proof also shows that:

\begin{lemma}\label{contrad}
If $\Sigma\cup\{\theta\}$ is an inconsistent set of $\ll$-sentences,
then $\Sigma\proves\neg\theta$.
\end{lemma}
\proof
If $\Sigma\cup{\theta}\proves\#$ then by the Deduction Lemma,
$\Sigma\proves{\theta}\implies\#$. But
$$({\theta}\implies\#)\implies\neg\theta$$
is a propositional tautology and so by Modus Ponens,
$\Sigma\proves\neg\theta$.
\qed


It also follows from the Deduction Lemma that:

\begin{lemma}\label{completion}
For any consistent $\Sigma$ and sentence $\theta$
either $\Sigma\cup\{\theta\}$ is consistent or $\Sigma\cup\{\neg\theta\}$
is consistent.
\end{lemma}
\proof
Otherwise by the Deduction Lemma
$\Sigma\proves \theta\implies\#$ and $\Sigma\proves \neg\theta\implies\#$.
But
$$(\neg\theta\implies\#)\implies(\theta\implies \#)$$
is a propositional
tautology and so by Modus Ponens twice $\Sigma\proves\#$.
\qed

The next lemma shows that adding new constant symbols can't hurt.

\begin{lemma}\label{constant}
  Suppose $\Sigma$ is a consistent set of $\ll$-sentences and
$c$ is a new constant symbol not appearing in $\ll$.  Then
$\Sigma$ is a consistent set of $\ll\cup\{c\}$-sentences.
\end{lemma}
\proof
Suppose
$$\theta_1(c),\theta_2(c),\ldots,\theta_n(c)$$
is a proof from $\Sigma$ of $\#$.   Let $y$ be any variable that does not
occur in any of the $\theta_i(c)$.  Then we claim
$$\theta_1(y),\theta_2(y),\ldots,\theta_n(y)$$
is a proof of $\#$ from $\Sigma$ in $\ll$.  This is because

(1) if $\theta_i(c)\in\Sigma$ then $c$ does not occur in
$\theta_i(c)$, so $\theta(c)=\theta(y)$.

(2) If $\theta_i(c)$ is a logical axiom and $y$ is any variable that
does not occur in $\theta_i(c)$, then $\theta_i(y)$ is a logical axiom.
(Note that an instance of S1 may turn into an instance of S2.)

(3)  Modus Ponens transfers over: e.g.

From $\theta(c)$ and $\theta(c)\implies \psi(c)$ infer $\psi(c)$.

From $\theta(y)$ and $\theta(y)\implies \psi(c)$ infer $\psi(y)$.
\qed

\begin{lemma} \label{Henkin}
Suppose $\Sigma$ is a consistent set of $\ll$-sentences and
$\theta(x)$ is an $\ll$-formula with one free variable $x$.
Let $c$ be a new constant symbol not appearing $\ll$.
Then $\Sigma\cup\{(\exists x\theta(x))\implies\theta(c)\}$ is
a consistent set of $\ll\cup\{c\}$-sentences.
\end{lemma}

\proof

The following claim is why we need the generalization axioms.
It says basically that proving some statement about an arbitrary new constant
is the same as proving for all $y$ the statement holds.

\bigskip
\noindent {\bf Claim}. Suppose that $\rho(c)$ is any $\ll\cup\{c\}$-sentence
such that $\Sigma\proves \rho(c)$.  Then for all but finitely many
variables $y$
we have that $\Sigma\proves \forall y\rho(y)$.

\proof
It is enough to prove that the set of such $\rho$ which satisfy the
claim contain $\Sigma$ and the Logical Axioms, and they are closed under
Modus Ponens.

Case 1. $\rho(c)$ is a logical axiom.
In this case $\rho(y)$ is also a logical axiom provided
that $y$ does not occur in $\rho$.  By (G3) closure under
universal quantification, $\forall y\rho(y)$ is also a logical axiom.

Case 2. $\rho(c)\in\Sigma$.
In this case $c$ does not appear in $\rho=\rho(c)$.  And so
 $$\rho\implies\forall y\rho$$
is a logical axiom and by
Modus Ponens $\Sigma\proves\forall y\rho$.

Case 3. $\rho(c)$ is obtained by Modus Ponens from
formulas, $\psi(c)\implies\rho(c)$ and $\psi(c)$
which $\Sigma$ proves.  By induction we assume that
for all but finitely many variables $y$ that
$$\Sigma\proves\forall y\;(\psi(y)\implies\rho(y))$$
and
$$\Sigma\proves\forall y \;\psi(y)$$
Now using the generalization axiom $G1$ and Modus Ponens
we get that $(\forall y(\psi(y))\implies(\forall y\rho(y)))$
and so by Modus Ponens again we get $\forall y\rho(y)$.

\noindent This ends the proof of the Claim.

\bigskip

To prove the Lemma assume for contradiction that
$\Sigma\cup\{(\exists x\theta(x))\implies\theta(c)\}$ is inconsistent.
Then by Lemma \ref{contrad} we have that
$$\Sigma\proves \rho(c)$$
where $\rho(c)= \neg[(\exists x\theta(x))\implies\theta(c)]$.
By the claim for all but finitely many variables $y$
$$\Sigma\proves \forall y\rho(y)$$
But this is exactly the negation of the Axiom H:
$$[\exists y[(\exists x\theta(x))\implies \theta(y)]$$
is the same as
$$[\neg\forall y \neg [(\exists x\theta(x))\implies \theta(y)]$$
which is the same as
$$ \neg\forall y\rho(y)$$
Thus $\Sigma$ is inconsistent as a $\ll\cup\{c\}$-theory and
hence by Lemma \ref{constant} an inconsistent $\ll$-theory.
\qed

Finally we prove part (b) of Lemma \ref{complete}.

\begin{theorem}
(G\"odel's Completeness
Theorem) Any consistent set $\Sigma$ of $\ll$-sentences has
a model.
\end{theorem}
\proof

The first step is to add to $\ll$ infinitely many new constant symbols.
Let $\ll'=\ll\cup\{c_n:n\in\omega\}$.  By an  induction on
$N$ Lemma \ref{constant} shows that $\Sigma$ is a consistent set of
$\ll\cup\{c_n:n<N\}$-sentences.  Since proofs are finite
it must be that $\Sigma$ is a consistent set of $\ll'$-sentences.

Now let $\{\psi_n:n\in\omega\}$ be the set of all $\ll'$-sentences
and let the set of all
$\ll'$-formulas with exactly one free variable be
$\{\theta_n(x_{k_n}):n\in\omega\}$.  These sets are countable because
$\ll'$ is.
Construct an increasing sequence $\Sigma_n$ of consistent $\ll'$-sentences
as follows.

Set $\Sigma_0=\Sigma$.

For even $n=2m$ put $\Sigma_{n+1}$ to be
either $\Sigma_n\cup\{\psi_m\}$ or $\Sigma_n\cup\{\neg\psi_m\}$ whichever
is consistent.  One of the two must be consistent by Lemma \ref{completion}.

For odd $n=2m+1$.  Let $c$ be a constant not appearing in any of the
sentences in $\Sigma_n$ or in $\theta_m(x)$ and let
$$\Sigma_{n+1}=\Sigma_n\cup\{(\exists x_m\theta_m(x))\implies\theta_m(c)\}$$
This is consistent by Lemma \ref{Henkin}.

Now let
$$\Gamma=\cup_{n\in\omega}\Sigma_n$$
Since the notion of proof
is finite the union of an increasing sequence of consistent sets of sentences
must be consistent.  By construction $\Gamma$ satisfies:

(1) $\Gamma$ is consistent

(2) $\Gamma$ is complete, i.e., for every $\ll'$-sentence $\psi$ either
$\psi\in\Gamma$ or $\neg\psi\in\Gamma$

(3) $\Gamma$ has the constant witness property: for any
$\ll'$-formula $\theta(x)$ with
one free variable $x$, there is a constant $c$ such that
$(\exists x\theta(x))\implies\theta(c)$ is in $\Gamma$.

Since $\Gamma$ is a complete consistent theory it
must contain all Logical Axioms which are sentences
and it must contain exactly
one of  $\theta$ or $\neg\theta$ for each sentence $\theta$.

Now we build the canonical model $\moda$ from $\Gamma$ and prove
that for every $\ll'$-sentence $\theta$ that
$$\moda\models\theta \rmiff \theta\in\Gamma$$

Let $\famc$ be the set of constant symbols in the language
$\ll'$.  Define a binary relation on $\famc$ by
$c\approx d$ iff $c=d\in\Gamma$.
Notice that the equality axioms E1,E2,E3 imply that $\approx$ is an
equivalence relation. Since $\Gamma$ is consistent and complete it must
contain all Logical axioms which are sentences, in particular the
E1,E2,E3,E4 when the terms involved are constant symbols.
It follows from E1,E2,E3 that $\approx$ is an equivalence
relation. We define the universe $A$ of the canonical model $\moda$ to be
set of equivalence classes of $\approx$: $$A=\famc/\approx$$ For each
constant symbol $c$ we define $$c_A=[c]=\{d\in\famc\;:\; c\equiv d\}$$ the
equivalence class containing $c$.

It follows from E4 and that
of $\Gamma$ that

if
$c_1\approx d_1$, $c_2\approx d_2$, $\ldots$, and $c_n\approx d_n$,

then $R(c_1,c_2,\ldots,c_n)\in\Gamma$ iff
$R(d_1,d_2,\ldots,d_n)\in\Gamma$.

Thus we may define the relation $R_A$ on $A^n$ by
$$([c_1], [c_2],\ldots,[c_n])\in R_A\rmiff R(c_1,c_2,\ldots,c_n)\in \Gamma$$

This definition of the canonical model guarantees that for any atomic
$\ll'$-sentence $\theta$:
$$\moda\models\theta \rmiff \theta\in\Gamma$$

Inductive steps

\bigskip
$\neg\theta$:
$$\moda\models\neg\theta \rmiff \mbox{ not }\moda\models\theta\rmiff
\theta\notin\Gamma \rmiff\neg\theta\in\Gamma$$
The last ``iff'' requires proof. If $\theta\notin\Gamma$ then
$\neg\theta\in\Gamma$ since $\Gamma$ is complete. If
$\neg\theta\in\Gamma$, then $\theta\notin\Gamma$ because otherwise
$\Gamma$ is inconsistent.

\bigskip
$(\theta_1\disj\theta_2)$:
$$\moda\models\theta_1\disj\theta_2 \rmiff (\moda\models\theta_1
\rmor\moda\models\theta_2)
\rmiff (\theta_1\in\Gamma \rmor \theta_2\in\Gamma)
\rmiff (\theta_1\disj\theta_2)\in\Gamma)$$
The last ``iff'' is because $\Gamma$ is complete and consistent, otherwise
one would get a propositional contradiction in $\Gamma$.

\bigskip
$\exists x\theta(x)$:

\noindent If $\moda\models\exists x\theta(x)$, then
for some constant symbol $c$ we have that
$\moda\models\theta(c)$. By inductive hypothesis $\theta(c)\in\Gamma$.
Since $\Gamma$ is complete either $\exists x\theta(x)\in\Gamma$
or $\neg\exists x\theta(x)\in\Gamma$.  If that latter is the case,
then $\neg\neg\forall x\neg\theta(x)\in\Gamma$ and we may drop the
double negation, since $\neg\neg A\implies A$ is propositional
tautology.  Buy by the substitution axiom S1 we would have
$\neg\theta(c)$ provable from $\Gamma$ and therefore it would be
inconsistent.

Conversely suppose that $\exists x\theta(x)\in\Gamma$.  Now by the
constant witness
property $(\exists x\theta(x))\implies\theta(c)\in\Gamma$ for
some constant $c$.  So by Modus ponens $\theta(c)\in\Gamma$ and
by inductive hypothesis $\moda\models\theta(c)$ and
so $\moda\models \exists x\theta(x)$.

This completes the proof of the completeness theorem.





\end{document}