\documentclass[%
version=last,%
a5paper,
10pt,%
headings=small,%
bibliography=totoc,%
index=totoc,%o
twoside,%
leqno,%
cleardoublepage=empty,%
%open=any,%
%parskip=half,%
%draft=false,%
draft=true,%
%DIV=classic,%
DIV=11,%
headinclude=true,%
pagesize]%{scrreprt}
{scrartcl}

%\usepackage[notref,notcite]{showkeys}
\renewcommand{\theequation}{\fnsymbol{equation}}

\usepackage[headsepline]{scrpage2}
\pagestyle{scrheadings}
\clearscrheadings
\ohead{\pagemark}
\ihead{G\"odel's Completeness Theorem}

\usepackage{hfoldsty}
\usepackage[neverdecrease]{paralist}
\usepackage{url}


\usepackage{relsize} % Here \smaller scales by 1/1.2; \relscale{X} scales by X

\renewenvironment{quote}{\begin{list}{}
{\relscale{.90}\setlength{\leftmargin}{0.05\textwidth}
\setlength{\rightmargin}{\leftmargin}}
\item[]}
{\end{list}}


\usepackage{amsmath,amsthm,amssymb,bm,upgreek,mathrsfs}
%\usepackage[all]{xy}

\usepackage{stmaryrd} % for \mapsfrom

\newcommand{\Forall}[1]{\forall#1\;}
\newcommand{\Exists}[1]{\exists#1\;}
\let\oldvec\vec
\renewcommand{\vec}[1]{\bm{#1}}
\newcommand{\N}{\mathbb N}


\usepackage[mathcal]{euscript}
\newcommand{\tf}[1]{\mathcal{#1}} % ``Tarski's font''

\newcommand{\F}{\mathbf F}
\newcommand{\EF}{\mathbf{EF}}
\newcommand{\AF}{\mathbf{AF}}
\newcommand{\AC}[1][]{\mathbf{AC}_{#1}}
\newcommand{\AT}{\mathbf{AT}}
\newcommand{\ACL}{\mathbf{ACL}}

\DeclareMathOperator{\spectrum}{Spec}
\newcommand{\spec}[1]{\spectrum(#1)}

\newcommand{\conc}{\mathbin{\hat{\ }}}
\newcommand{\sig}{\mathscr S}
\newcommand{\str}[1]{\mathfrak{#1}}
\newcommand{\size}[1]{\lvert#1\rvert}
\DeclareMathOperator{\setMod}{Mod}
\newcommand{\sMod}[1]{\setMod(#1)}
\newcommand{\Mod}[2][]{\mathbf{Mod}_{#1}(#2)}
\newcommand{\Moda}[1]{\mathbf{Mod}^*(#1)}
\newcommand{\Str}{\mathbf{Str}}
\DeclareMathOperator{\sentences}{Sen}
\newcommand{\Sen}{\sentences}
\newcommand{\modsim}{/\mathord{\sim}}
\newcommand{\pow}[1]{\mathscr P(#1)}
\newcommand{\inv}{{}^{-1}}

\newcommand{\Cat}[1]{\bm{\mathsf{#1}}}
\newcommand{\Top}{\Cat{Top}}
\newcommand{\Frm}{\Cat{Frm}}
\newcommand{\Loc}{\Cat{Loc}}
\newcommand{\Grp}{\Cat{Grp}}
\newcommand{\Set}{\Cat{Set}}
\DeclareMathOperator{\domain}{dom}
\newcommand{\dom}[1]{\domain(#1)}
\DeclareMathOperator{\points}{pt}
\newcommand{\pt}[1]{\points(#1)}
\DeclareMathOperator{\homoms}{Hom}
\newcommand{\Hom}[1]{\homoms(#1)}
\newcommand{\bel}[1]{\left[#1\right]}

\newcommand{\Sn}[1][\sig]{\sentences_{\sig}}
\newcommand{\Sna}[1][\sig]{\sentences^*_{\sig}}
\DeclareMathOperator{\formulas}{Fm}
\newcommand{\Fm}[1][\sig]{\formulas_{#1}}
\DeclareMathOperator{\freevariables}{fv}
\newcommand{\fv}[1]{\freevariables(#1)}
\DeclareMathOperator{\variables}{v}
\newcommand{\vr}[1]{\variables(#1)}
\DeclareMathOperator{\theory}{Th}
\newcommand{\Th}[1]{\theory(#1)}
\newcommand{\Tha}[1]{\theory^*(#1)}
\renewcommand{\emptyset}{\varnothing}
\renewcommand{\setminus}{\smallsetminus}
\renewcommand{\leq}{\leqslant}
\renewcommand{\nleq}{\nleqslant}
\renewcommand{\geq}{\geqslant}
\renewcommand{\phi}{\varphi}
%\newcommand{\Or}{\;\lor\;}
\newcommand{\Or}{\;\mathrel{\text{\textsc{or}}}\;}
\renewcommand{\models}{\vDash}
\newcommand{\nmodels}{\nvDash}
\newcommand{\included}{\subseteq}
\newcommand{\includes}{\supseteq}
\newcommand{\pincluded}{\subset}
\newcommand{\liff}{\leftrightarrow}
\newcommand{\lto}{\Rightarrow}



\newtheorem{theorem}{Theorem}
\newtheorem{definition}[theorem]{Definition}

\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{lemma}{Lemma}

\theoremstyle{definition}

\newtheorem{example}[theorem]{Example}

\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}

\begin{document}

\title{G\"odel's Completeness Theorem}
\author{David Pierce}
\date{June 18, 2015}
\publishers{Mimar Sinan Fine Arts University\\
Istanbul\\
\url{http://mat.msgsu.edu.tr/~dpierce/}}
\maketitle

Here are notes on Kurt G\"odel's 1930 paper,
``The completeness of the axioms of the functional calculus of logic,''
in the translation of Stefan Bauer-Mengelberg, 
as edited by Jean van Heijenoort
in the anthology, \emph{From Frege to G\"odel} \cite{Goedel-compl}.

I make these notes in preparation 
for a course of three lectures on the Compactness Theorem
to be presented in the school (June 20--24, 2015) 
of the 5th World Congress and School on Universal Logic in Istanbul
(the congress being June 25--30).

G\"odel's paper apparently represents the earliest explicit statement
of a version of the theorem that is now called the Compactness Theorem.
In G\"odel's version, the signature is countable (``denumerable'').

G\"odel defines a proof system and proves its completeness
in the sense that every sentence that cannot be disproved (``refuted'') 
has a model.
By means of the Compactness Theorem,
he derives the result that,
in a countable signature, 
an arbitrary set of sentences has a model, 
provided the set is consistent
(the conjunction of no finite subset can be disproved).

As G\"odel explains in his first paragraph,
the ``functional calculus'' of his title
is the \textbf{restricted functional calculus,}
which he defines in a footnote:
\begin{quote}
  In terminology and symbolism this paper follows 
\emph{Hilbert and Ackermann 1928.}%%%%%
\footnote{Van Heijenoort spells out the reference in his own bibliography:
David Hilbert and Wilhelm Ackermann, 
\emph{Grundz\"uge der theoretischen Logik} (Berlin: Springer, 1928).}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
According to that work, the restricted functional calculus 
contains the logical expressions 
that are constructed from propositional variables,
$X$, $Y$, $Z$, \dots, and functional variables
(that is, variables for properties and relations) of type I,
$F(x)$, $G(x,y)$, $H(x,y,z)$, \dots, 
by means of the operations $\lor$ (or), $\overline{\phantom X}$ (not),
$(x)$ (for all), $(Ex)$ (there exists),
with the variable in the prefixes $(x)$ or $(Ex)$
ranging over individuals \emph{only, not} over functions.
A formula of this kind is said to be valid (tautological)
if a true proposition results from every substitution
of specific propositions and functions for $X$, $Y$, $Z$, \dots,
and $F(x)$, $G(x,y)$, \dots, respectively (for example
$(x)[F(x)\lor\overline{F(x)}]$).
\end{quote}
Perhaps the expression \emph{type I} 
is the ancestor of our \emph{first order,}
and a \emph{function of type I} takes individuals as its arguments.
Such functions are our \emph{relations.}
A proposition can then be understood as a nullary relation.
I shall translate G\"odel's symbolism as follows:
\begin{equation*}\renewcommand{\arraystretch}{1.3}
  \begin{array}{cc}
    \text{G\"odel}&\text I\\\hline\hline
(x)&\forall x\\\hline
(Ex)&\exists x\\\hline
\overline{\phantom x}&\lnot\\\hline
\&&\land\\\hline
\bm{\sim}&\liff\\\hline
\rightarrow&\lto\\\hline\hline
  \end{array}
\end{equation*}
(I vacillate between using $\Rightarrow$ for implication, 
because the notion is different 
from a function's being from one set to another, 
and using $\rightarrow$ because it is easier to write by hand.)

The \emph{restricted} functional calculus is what Church \cite{MR18:631a}
calls the \emph{pure} functional calculus.
We just call it first-order logic.
But we have made a difference in emphasis.
We have a different first-order logic for each \emph{signature.}
G\"odel just supposes there are infinitely many $n$-ary functional variables
(relation symbols) for each $n$.

Perhaps for G\"odel, a \emph{property} is a singulary relation;
a \emph{relation,} a relation of more than one argument.
An $n$-ary relation on a set $A$
determines the function from $A^n$ to $2$
that takes the value $1$ at a point $\vec a$ of $A^n$
if and only if the relation actually holds at that point.

I shall quote G\"odel's ten numbered theorems \emph{verbatim,}
with my own commentary interspersed.

\textsc{Theorem I.}  
\emph{Every valid formula of the restricted functional calculus is provable.}

The proof of this will not be completed until after Theorem VI.

G\"odel explains validity in another footnote.
In our terminology,
$\phi(\vec x)$ is \textbf{valid}
if $\Forall{\vec x}\phi(\vec x)$ is true in every structure;
by ``well-known theorems'' (of L\"owenheim and Skolem, presumably),
it is enough to be true in every countable structure.

The formula $\phi(\vec x)$ is \textbf{satisfiable}
if $\Exists{\vec x}\phi(\vec x)$ is true in some structure.
Thus $\phi$ is valid if and only if $\lnot\phi$ is not satisfiable.

G\"odel's ``system of axioms'' is as follows.
Again I translate into current symbolism;
my convention on parentheses is Shoenfield's \cite[pp.\ 17--8]{MR1809685}:
$\lor$ is more binding than $\lto$, and of two occurrences of one of these,
the occurrence on the right is the more binding.

The ``undefined primitive notions'' 
are $\lor$, $\lnot$, and $\forall x$, and,
``By means of these, 
$\land$, $\lto$, $\liff$, and $\exists x$ 
can be defined in a well-known way.''
The axioms are:
\begin{enumerate}[1)]
\item 
$P\lor P\lto P$,
\item
$P\lto P\lor Q$,
\item
$P\lor Q\lto Q\lor P$,
\item
$(P\lto Q)\lto R\lor P\lto R\lor Q$,
\item
$\Forall xF(x)\lto F(y)$,
\item
$\Forall x(P\lor F(x))\lto P\lor\Forall xF(x)$.
\end{enumerate}
The rules of inference are:
\begin{description}
\item[Detachment:]
from $\phi$ and $\phi\lto\psi$, infer $\psi$.
\item[Substitution:]
``The rule of substitution for propositional and functional variables.''
Above, $P$, $Q$, and $R$ are propositional variables,
and $F(x)$ is a functional variable.
Church discusses this.
There are six axioms above;
by substitution we derive infinitely many validities.
Alternatively, we could replace the axioms with \emph{axiom schemes,}
and forget about the rule of substitution.
\item[Generalization:]
From $\phi(x)$, infer $\Forall x\phi(x)$.
\item[Change of variables:]
``Individual variables (free or bound) may be replaced by any others,
so long as this does not cause overlapping of the scopes of variables
denoted by the same sign.''
\end{description}
G\"odel points out in a note
that Russell and Whitehead do not formulate ``all of these'' explicitly.

G\"odel has noted in the first paragraph
that we already have completeness for propositional calculus.
Thus, I say, we might as well replace the first four axioms above
with one axiom scheme, giving us every tautology of the propositional calculus.
G\"odel himself will re-assert propositional completeness 
as one of the lemmas below.

We could be more explicit about change of variables:
\begin{itemize}
\item 
$\Forall x\phi(x)\lto\Forall y\phi(y)$ is an axiom 
($y$ being substitutable for $x$ in $\phi$).
\item
From $\phi(x)$, infer $\phi(y)$, 
provided $x$ is not a free variable of any hypotheses of a proof.
\end{itemize}
G\"odel states some lemmas without proof:
\begin{enumerate}
\item
  For every tuple $\vec x$ of variables,%%%%%
\footnote{As G\"odel explains, 
he uses lower-case German letters like 
$\mathfrak x$, $\mathfrak y$, $\mathfrak u$, $\mathfrak v$, ``and so on,''
for these tuples.}
\begin{gather*}
  \Forall{\vec x}\phi(\vec x)\lto\Exists{\vec x}\phi(\vec x),\\
  \Forall{\vec x}\phi(\vec x)\land\Exists{\vec x}\psi(\vec x)
\lto\Exists{\vec x}(\phi(\vec x)\land\psi(\vec x)),\\
\Forall{\vec x}\lnot\phi(\vec x)\liff\lnot\Exists{\vec x}\phi(\vec x).
\end{gather*}
Note that G\"odel has not formally explained the meaning of $\exists x$;
perhaps the ``well-known'' definition alluded to above is that 
$\Exists x\phi$ means $\lnot\Forall x\lnot\phi$.
\item
For every $n$ in $\upomega$, for every permutation $\sigma$ of $n$,
for every $n$-tuple $\vec x$ of variables,
\begin{equation*}
  \Exists{\vec x}\phi(\vec x)\lto\Exists{(\vec x\circ\sigma)}\phi(\vec x).
\end{equation*}
In my notation, $\vec x$ is a function from $n$ to the set of variables.
\item
Assuming $\vec x$ is injective as such a function,
even if $\vec y$ is not,
\begin{equation*}
  \Forall{\vec x}\phi(\vec x)\lto\Forall{\vec y}\phi(\vec y).
\end{equation*}
\item
{}[Blending of quantifiers in a conjunction or disjunction:
see the proof of Theorem III.
G\"odel apparently neglects to say that the variables must be distinct.]
\item
For every $\phi$ there is $\phi'$ in \emph{normal form} 
such that $\phi\liff\phi'$.
G\"odel does not define normal form,
but only refers again to Hilbert and Ackermann.
Evidently it is as defined by Skolem in his 1920 paper
\cite{Skolem-LS}:
in our terms, a formula is in \textbf{normal form}
if it is an \textbf{open} (quantifier-free) formula,
preceded by some (or no) existential quantifiers,
preceded by some (or no) universal quantifiers.
\item
If $\phi\liff\phi'$, then $\psi\liff\psi'$,
where $\phi$ is a subformula of $\psi$,
and $\psi'$ results from $\psi$ by replacing $\phi$ with $\phi'$.
\item
Completeness of the first four axioms for propositional calculus.
Note that G\"odel does not mention any rules of inference at this point.
\end{enumerate}

Theorem I is equivalent to:

\textsc{Theorem II.} \emph{Every formula of the restricted functional calculus
is either refutable or satisfiable} 
(and moreover satisfiable in the [\emph{sic}]
denumerable domain of individuals).

\textbf{Refutable} means having provable negation.

The ``class'' (set) $\mathfrak K$ consists of \emph{sentences}
in normal form of the more precise form
\begin{equation*}
  \Forall x\dots\;\Exists y\phi.
\end{equation*}
That is, 
the sentence must have at least one universal and one existential quantifier.

\textsc{Theorem III.}
\emph{If every $\mathfrak K$-expression is either refutable or satisfiable,
so is every expression.}

A note says the restriction to ``the denumerable domain of individuals''
will be implicit.

\begin{proof}
By definition, $\phi(\vec x)$ is satisfiable
if and only if $\Exists{\vec x}\phi(\vec x)$ is satisfiable.

  If $\phi(\vec x)$ is refutable,
this means $\lnot\phi(\vec x)$ is provable,
so $\Forall{\vec x}\lnot\phi(\vec x)$ is provable by Generalization,
so $\Exists{\vec x}\phi(\vec x)$ is refutable.

If $\Exists{\vec x}\phi(\vec x)$ is refutable,
this means $\lnot\Exists{\vec x}\phi(\vec x)$ is provable,
so that $\Forall{\vec x}\lnot\phi(\vec x)$ is provable,
and therefore $\lnot\phi(\vec x)$ is provable by Axiom 5,
that is, $\phi(\vec x)$ is refutable.

It is now enough to prove the claim for \emph{sentences.}

By Lemma 5, it is enough to prove the claim for \emph{normal sentences.}
Let $\mathsf Q\;\phi$ be such.
If $x$ and $y$ are distinct variables not occuring in $\mathsf Q$,
and $R$ is some singulary relation symbol, then the sentence
\begin{equation*}
  \Forall x\lnot Rx\lor\Exists yRy
\end{equation*}
is a tautology and is therefore provable by Lemma 7.
But by Lemma 4, the sentence
\begin{equation*}
  \Forall x\lnot Rx\lor\Exists yRy\liff
\Forall x\Exists y(\lnot Rx\lor Ry)
\end{equation*}
is provable, 
by Lemma 4, and therefore so are the following:
\begin{gather*}
\Forall x\Exists y(\lnot Rx\lor Ry),\\
  \mathsf Q\;\phi
\liff\mathsf Q\;\phi\land\Forall x\Exists y(\lnot Rx\lor Ry),\\
\mathsf Q\;\phi\land\Forall x\Exists y(\lnot Rx\lor Ry)
\liff\Forall x\mathsf Q\;\Exists y(\phi\land(\lnot Rx\lor Ry)),\\
\mathsf Q\;\phi
\liff\Forall x\mathsf Q\;\Exists y(\phi\land(\lnot Rx\lor Ry)).
\end{gather*}
The sentence $\Forall x\mathsf Q\;\Exists y(\phi\land(\lnot Rx\lor Ry))$
being in $\mathfrak K$, we are done.
\end{proof}

The \textbf{degree} of a sentence in $\mathfrak K$
is the number of blocks of universal quantifiers.

\textsc{Theorem IV.} \emph{If every expression of degree $k$
is either satisfiable or refutable,
so is every expression of degree $k+1$.}

\begin{proof}
Suppose $\sigma$ is the sentence
$\Forall{\vec x}\Exists{\vec y}\Forall{\vec u}\Exists{\vec v}\mathsf Q\;\phi$.
Suppose $R$ (taking arguments of the length of $\vec x\vec y$)
does not occur in $\phi$.  Then
\begin{equation*}
(R\vec x\vec y\lto\Forall{\vec u}\Exists{\vec v}\mathsf Q\;\phi)
\liff\Forall{\vec u}\Exists{\vec v}\mathsf Q\;(R\vec x\vec y\lto\phi).
\end{equation*}
We make the following abbreviations:
\begin{align*}
  \tau_1&\text{ is }  
\Forall{\vec x'}\Exists{\vec y'}R\vec x'\vec y'\land
\Forall{\vec x}\Forall{\vec y}
(R\vec x\vec y\lto\Forall{\vec u}\Exists{\vec v}\mathsf Q\;\phi),\\
\tau_2&\text{ is }
\Forall{\vec x'}\Exists{\vec y'}R\vec x'\vec y'\land
\Forall{\vec x}\Forall{\vec y}
\Forall{\vec u}\Exists{\vec v}\mathsf Q\;(R\vec x\vec y\lto\phi),\\
\tau_3&\text{ is }
\Forall{\vec x'}\Forall{\vec x}\Forall{\vec y}\Forall{\vec u}
\Exists{\vec y'}\Exists{\vec v}\mathsf Q\;
(R\vec x'\vec y'\land(R\vec x\vec y\lto\phi)).
\end{align*}
``Obviously'' $\tau_1\lto\sigma$.
By Lemma 6, $\tau_1\liff\tau_2$; by Lemma 4, $\tau_2\liff\tau_3$.
We may assume as an inductive hypothesis that $\tau_3$
is either satisfiable or refutable.
If $\tau_3$ is satisfiable, then so is $\sigma$.
If $\tau_3$ is refutable, then so is $\tau_1$.
In particular, 
taking $R\vec x\vec y$ to be $\Forall{\vec u}\Exists{\vec v}\mathsf Q\;\phi$, 
we have
\begin{equation*}
  \lnot
(\Forall{\vec x}\Exists{\vec y}
\Forall{\vec u}\Exists{\vec v}\mathsf Q\;\phi\land
\Forall{\vec x}\Forall{\vec y}
(\Forall{\vec u}\Exists{\vec v}\mathsf Q\;\phi
\lto\Forall{\vec u}\Exists{\vec v}\mathsf Q\;\phi)).
\end{equation*}
But
$\Forall{\vec x}\Forall{\vec y}
(\Forall{\vec u}\Exists{\vec v}\mathsf Q\;\phi
\lto\Forall{\vec u}\Exists{\vec v}\mathsf Q\;\phi)$,
and therefore $\lnot\sigma$.
\end{proof}

``It now remains only to prove''

\textsc{Theorem V.}
\emph{Every formula [\emph{sic}] 
of degree 1 is either satisfiable or refutable.}

Let $\Forall{\vec x}\Exists{\vec y}\phi(\vec x,\vec y)$ be such a formula,
that is, sentence, where $\vec x$ is an $r$-tuple, 
and $\vec y$ is an $s$-tuple,
of distinct variables.
All variables come from the sequence $(x_k\colon k\in\upomega)$.
Let
\begin{gather*}
  \phi_1\text{ be }\phi(\vec x^1,\vec y^1),\\
\phi_2\text{ be }\phi(\vec x^2,\vec y^2)\land\phi_1,\\
\makebox[4cm]{\dotfill}\\
\phi_n\text{ be }\phi(\vec x^n,\vec y^n)\land\phi_{n-1}.
\end{gather*}
Here $k\mapsto\vec x^k$ is the bijection from $\N$
to the set of $r$-tuples of variables such that,
writing $\vec x^k$ as $(x_{k(i)}\colon i<r)$,
we have that the map
\begin{equation*}
k\mapsto(k(0),\dots,k(r-1),k(0)+\dots+k(r-1))
\end{equation*}
is an order-preserving bijection from $\N$ onto $\upomega^r$,
where the latter has the right lexicographic ordering.
In particular,
\begin{align*}
  \vec x^1&=(x_0,\dots,x_0),&
\vec x^2&=(x_1,x_0,\dots,x_0),&
\vec x^3&=(x_0,x_1,x_0,\dots,x_0).
\end{align*}
We also let
\begin{equation*}
  \vec y^k=(x_{(k-1)s+1},x_{(k-1)s+2},\dots,x_{(k-1)s+s}).
\end{equation*}

\textsc{Theorem VI.}
\emph{For every $n$}
\begin{equation*}
[\Forall{\vec x}\Exists{\vec y}\phi\lto\exists{x_0}\cdots\Exists{x_{ns}}\phi_n]
\end{equation*}
\emph{is provable.}

\begin{proof}
  Use induction.
By Lemma 3,
\begin{equation*}
  \Forall{\vec x}\Exists{\vec y}\phi(\vec x,\vec y)
\lto\Forall{\vec x_1}\Exists{\vec y}\phi(\vec x_1,\vec y),
\end{equation*}
and by Inference Rule 4,
\begin{equation*}
  \Exists{\vec y}\phi(\vec x_1,\vec y)\liff
\Exists{\vec y_1}\phi(\vec x_1,\vec y_1),
\end{equation*}
so
\begin{equation*}
  \Forall{\vec x}\Exists{\vec y}\phi(\vec x,\vec y)
\lto\Forall{\vec x_1}\Exists{\vec y_1}\phi(\vec x_1,\vec y_1).
\end{equation*}
By Lemma 1,
\begin{equation*}
  \Forall{\vec x_1}\Exists{\vec y_1}\phi(\vec x_1,\vec y_1)
\lto\Exists{\vec x_1}\Exists{\vec y_1}\phi(\vec x_1,\vec y_1).
\end{equation*}
This is just the claim when $n=1$.

Similarly
\begin{equation*}
  \Forall{\vec x}\Exists{\vec y}\phi(\vec x,\vec y)
\lto
\Forall{\vec x_{n+1}}\Exists{\vec y_{n+1}}\phi(\vec x_{n+1},\vec y_{n+1}).
\end{equation*}
Now let
\begin{equation*}
\vec z_n=(x_i\colon i\leq ns\And x_i\text{ is not an entry of }\vec x_{n+1}).
\end{equation*}
By Lemma 2,
\begin{equation*}
  \exists{x_0}\cdots\Exists{x_{sn}}\phi_n
\lto\Exists{\vec x_{n+1}}\Exists{\vec z_n}\phi_n.
\end{equation*}
By Lemma 1,
\begin{multline*}
  \Forall{\vec x_{n+1}}\Exists{\vec y_{n+1}}\phi(\vec x_{n+1},\vec y_{n+1})
\land
\Exists{\vec x_{n+1}}\Exists{\vec z_n}\phi_n\\
\lto
  \Exists{\vec x_{n+1}}(\Exists{\vec y_{n+1}}\phi(\vec x_{n+1},\vec y_{n+1})
\land\Exists{\vec z_n}\phi_n).
\end{multline*}
Thus
\begin{multline*}
  \Forall{\vec x}\Exists{\vec y}\phi(\vec x,\vec y)
\land  
\exists{x_0}\cdots\Exists{x_{sn}}\phi_n\\
\lto
  \Exists{\vec x_{n+1}}(\Exists{\vec y_{n+1}}\phi(\vec x_{n+1},\vec y_{n+1})
\land\Exists{\vec z_n}\phi_n).
\end{multline*}
By Lemmas 4, 6, and 2,
\begin{equation*}
  \Exists{\vec x_{n+1}}(\Exists{\vec y_{n+1}}\phi(\vec x_{n+1},\vec y_{n+1})
\land\Exists{\vec z_n}\phi_n)
\lto
\exists{x_0}\cdots\Exists{x_{s(n+1)}}\phi_{n+1}.
\end{equation*}
By induction, this establishes the claim for all $n$.
\end{proof}

Let $F_n$ be the propositional formula
that results from replacing the atomic (``elementary'') components of $\phi_n$
with distinct propositional variables (or nullary relation symbols).

If some $F_n$ is refutable,
then so is $\exists{x_0}\cdots\Exists{x_{ns}}\phi_n$
(by Rules 2 and 3 and Lemma 1).
By the last theorem then, $\Forall{\vec x}\Exists{\vec y}\phi(\vec x,\vec y)$
is refutable.

Suppose now no $F_n$ is refutable.
Then all are satisfiable.
Then for all $n$, there is a structure $\str A_n$
with universe $\upomega$
in which $\phi_n$ is satisfied by $(0,\dots,ns)$.
``By familiar arguments''
we may assume that, for all relation symbols $R$ appearing in $\phi$,
for all $\vec a$ with entries from $\{0,\dots,ns\}$,
\begin{equation*}
  \str A_n\models R\vec a\iff\str A_{n+1}\models R\vec a.
\end{equation*}
Now define $\str B$ with universe $\upomega$ so that
\begin{equation*}
  \str B\models R\vec a\iff\text{ for sufficiently large $n$, }
\str A_n\models R\vec a.
\end{equation*}
``Then it is evident at once that'' 
$\str B\models\Forall{\vec x}\Exists{\vec y}\phi$. 
This concludes the proof of Theorem I.
\begin{quote}
  Let us note that the equivalence now proved, ``valid = provable'',
contains, for the decision problem,
a reduction of hte nondenumerable to the denumerable,
since ``valid'' refers to the nondenumerable totality of functions,
while ``provable'' presupposes only the denumerable totality of formal proofs.
\end{quote}

We can incorporate identity between individuals.
Then we get \textsc{Theorem VII} and \textsc{Theorem VIII,}
analogues of Theorems I and II.

\textsc{Theorem IX.}
\emph{Every denumerably infinite set of formulas 
of the restricted functional calculus either is satisfiable 
(\emph{that is, all formulas of the system are simultaneously satisfiable}) 
or possesses a finite subsystem whose logical product is refutable.}

``IX follows immediately from'' the following,
which is our \textbf{Compactness Theorem}
for countable signatures:

\textsc{Theorem X.}
\emph{For a denumerably infinite system of formulas to be satisfiable
it is necessary and sufficient that every finite subsystem be satisfiable.}

To prove this,
it is enough to look at normal sentences of degree one.
Suppose we have a system of sentences
\begin{equation*}
  \Forall{\vec x_k}\Exists{\vec y_k}\phi_k(\vec x_k,\vec y_k),
\end{equation*}
where $\vec x_k$ is an $r_k$-tuple,
and $\vec y_k$ is an $s_k$-tuple.
Obtain a bijection $j\mapsto\vec x^k_j$ as before,
each $\vec x^k_j$ being an $r_k$-tuple.
Let $\vec y^k_j$ be an $s_k$-tuple, and suppose the sequence
\begin{equation*}
\vec y^1_1,\vec y^1_2,\vec y^2_1,\vec y^1_3,\vec y^2_2,\vec y^3_1,\vec y^1_4,\dots
\end{equation*}
gives the $x_j$ in order.
Now define
\begin{gather*}
  \psi_1=\phi_1(\vec x^1_1,\vec y^1_1),\\
\psi_n=\psi_{n-1}\land\phi_1(\vec x^1_n,\vec y^1_n)
\land\dots\land\phi_n(\vec x^n_1,\vec y^n_1).
\end{gather*}
Then
\begin{equation*}
\bigwedge_{1\leq k\leq n}\Forall{\vec x_k}\Exists{\vec y_k}\phi_k(\vec x_k,\vec y_k)
\lto
\Exists{(\vec y^i_j\colon 2\leq i+j\leq n+1)}\psi_n.
\end{equation*}
If each $\psi_n$ is satisfiable,
then so is the system of all of them.
But in this case the original system is satisfiable.

\begin{quote}
  We can also give a somewhat different turn to Theorem IX\dots
\end{quote}

The final two paragraphs concern independence of the axioms.

%\bibliographystyle{plain}
%\bibliography{../references}

\begin{thebibliography}{1}

\bibitem{MR18:631a}
Alonzo Church.
\newblock {\em Introduction to mathematical logic. {V}ol. {I}}.
\newblock Princeton University Press, Princeton, N.~J., 1956.

\bibitem{Goedel-compl}
Kurt G{\"o}del.
\newblock The completeness of the axioms of the functional calculus of logic.
\newblock In van Heijenoort \cite{MR1890980}, pages 582--91.
\newblock First published 1930.

\bibitem{MR1809685}
Joseph~R. Shoenfield.
\newblock {\em Mathematical logic}.
\newblock Association for Symbolic Logic, Urbana, IL, 2001.
\newblock reprint of the 1973 second printing.

\bibitem{Skolem-LS}
Thoralf Skolem.
\newblock Logico-combinatorial investigations in the satisfiability or
  provability of mathematical propositions: {A} simplified proof of a theorem
  by {L}. {L}{\"o}wenheim and generalizations of the theorem.
\newblock In van Heijenoort \cite{MR1890980}, pages 252--63.
\newblock First published 1920.

\bibitem{MR1890980}
Jean van Heijenoort, editor.
\newblock {\em From {F}rege to {G}\"odel: {A} source book in mathematical
  logic, 1879--1931}.
\newblock Harvard University Press, Cambridge, MA, 2002.

\end{thebibliography}



\end{document}
