\documentclass[a4paper,twoside,10pt]{article}
\input{/home/david/math/abbreviations}

\title{Elements of the theory of models}
\author{David Pierce}
\date{\today}

\pagestyle{myheadings}
\markboth{Elements of model-theory, David Pierce, \today}
{Elements of model-theory, David Pierce, \today}

\newcommand{\pvar}{V}
\DeclareMathOperator{\PF}{PF} % set of propositional formulas
\newcommand{\pfx}{\PF(\pvar)}
\newcommand{\hatchf}[1]{\hat{\chi}_{#1}}
  
\newcommand{\ivar}{X}
\newcommand{\interp}{\mathrm{int}}

\newcommand{\cl}[1]{\overline{#1}}  

\newcommand{\modelled}{\mathrel{=\!\!\!|}}
\newcommand{\lequiv}{\models\;\modelled}

\begin{document}
\maketitle
\thispagestyle{empty}
\tableofcontents
\setcounter{section}{-1}
\section{Preface}

These notes are written according
to my own understanding and preferences, and they should be considered
only as a rough draft.  I aim to present some logic as
mathematics, and I assume that the reader already has some experience
with mathematics.  I claim no originality, but
I do not happen to know of a published treatment that is quite like
mine.  However, \S~\ref{sect:prop} in particular is
influenced by \cite{MR91c:03026} and \cite{Kueker}; most model-theory
texts seem not to deal specifically with propositional logic.  For the
model-theoretic development of first-order logic, see also the early
parts of \cite{MR94e:03002}, \cite{MR2001a:03072} or \cite{MR1924282}.
Books on logic itself that I have found useful are \cite{MR18:631a}
and \cite{Burris}. 

Technical terms in boldface are being defined, perhaps implicitly.
Mathematical propositions (theorems, lemmas) whose proofs are not
supplied are to be proved by the reader.

\section{Conventions}
In these notes, the symbol $\Iff$ is just an abbreviation for the
words `if and only if'.

Let us denote the set $\{0,1,2,\dots\}$ of natural numbers by $\varN$.
It is notationally convenient to consider this as the smallest set of
sets
that contains $\emptyset$ and is closed under the successor-operation,
namely 
\begin{equation*}
  A\mapsto A\cup\{A\}.
\end{equation*}
So $\varN$ contains $\emptyset$, $\{\emptyset\}$ and
$\{\emptyset,\{\emptyset\}\}$, denoted $0$, $1$ and $2$ respectively.
Thus, $2$ is $\{0,1\}$, which we shall consider as the underlying
set---the \tech{universe}---of the $2$-element field, $\F_2$.  We can
write any $n$ in $\varN$ as
\begin{equation*}
  \{0,\dots,n-1\}.
\end{equation*}

Suppose $M$ is a set, and $I$ is a finite set.  We shall denote the
set of functions from $I$ to $M$ by
$\mapset IM$.
Elements of this are \defn{$I$-tuples}; a typical $I$-tuple can be
written
\begin{equation*}
  (a_j:j\in I)
\end{equation*}
or just $\tuple a$.  If $I=n$ for some $n$ in $\varN$, then we may
write $\tuple a$ as
$(a_0,\dots,a_{n-1})$
or as the \defn{string} $a_0\dots a_{n-1}$.  As a special case, we
have
$\mapset 0M=\{0\}=1$.


\section{Propositional model-theory}\label{sect:prop}

We first select a set $\pvar$, and we shall refer to its
members as \defn{variables}.  Usually, $\pvar$ is countably infinite,
but this will not be required in any definitions.  If $A\included
\pvar$, then we may refer to
the ordered pair $(A,\pvar)$ as a \defn{(propositional) structure (for
$\pvar$)} and denote it by
\begin{equation*}
  \str A.
\end{equation*}
The structure $\str A$ determines, and is determined
by, the characteristic function $\chf {\str A}\colon \pvar\to2$, which is given by
\begin{equation*}
  \chf {\str A}(P)=
  \begin{cases}
    0,&\text{ if }P\in \pvar\setminus A;\\
    1,&\text{ if }P\in A.
  \end{cases}
\end{equation*}
We may call such a characteristic function a \defn{truth-assignment
  for $\pvar$}, reading $0$ as `false', and $1$ as `true'.

\begin{remark}
Instead of $\chf{\str A}$, one may write $\chf A$ if the
  domain of the function is clear.
\end{remark}

Next, we introduce a set
\begin{equation*}
  \{\land,\lor,\mathord{\lnot},\to,\iff\}
\end{equation*}
of \defn{Boolean connectives}, along with a pair $\{\mathord
(,\mathord)\}$ of
\defn{brackets}.  We assume that the Boolean connectives and the
brackets are not variables.  We define the \defn{(propositional)
  formulas (for $\pvar$)} to be the members of the
smallest set $\Phi$ of strings of elements of
$\pvar\cup\{\land,\mathord{\lor},\lnot,\to,\iff\}\cup\{(,)\}$ such that
\begin{enumerate}\setcounter{enumi}{-1}
  \item
$\pvar\included\Phi$;
\item
if $F\in\Phi$, then $\lnot F\in\Phi$;
\item
if $F,G\in\Phi$, and $*\in\{\land,\lor,\to,\iff\}$, then
$(F*G)\in\Phi$. 
\end{enumerate}
So, we can call $\lnot$ a \defn{unary} connective; the other connectives are
\defn{binary}.   
Let us denote the set of propositional formulas in $\pvar$ by $\pfx$.  The
definition of $\pfx$ obviously allows proof by induction.  That is, if
$\Phi\included\pfx$, and if $\Phi$ satisfies the three enumerated
conditions in the definition of $\pfx$, then $\Phi=\pfx$.

\begin{remark}
The symbols $\land$, $\lor$, $\lnot$, $\to$ and $\iff$ can be read
  `and', `or', `not', `implies' and `if and only if', respectively.
  We could avoid brackets by using the so-called \defn{Polish notation},
  in which we would write $*FG$ instead of $(F*G)$; using
  \defn{reverse} Polish notation, we would write $FG*$.  Note that the
  formulation $FG\mathord{\land}$ in reverse Polish notation could be
  read as `$F$, $G$ too,' or in Turkish as `$F$, $G$ de'.
\end{remark}

\begin{lemma}[unique readability]\label{lem:prop:ur}
  Any propositional formula that is not a variable is the application
  of exactly one connective in exactly one way, that is, if $F$, $F'$,
  $G$, $G'$ and $H$ are formulas, then $F*G$ and $\lnot H$ cannot be
  the same formula, and if $F*G$ and $F'*'G'$ are the same formula,
  then $F$ and $F'$ are the same formula.
\end{lemma}

\begin{lemma}[definition by recursion]\label{lem:prop:rec}
  Functions on $\pfx$ can be defined recursively.  To be precise,
  suppose $S$ is a set, and $f_{\lnot}$ is a function from $S$ to
  itself, and $f_*$ is a function from $S\times S$ to $S$ for each
  binary Boolean connective $*$. 
  Then for every function $g\colon \pvar\to S$, there is a
  \emph{unique} extension $\hat g\colon \pfx\to S$ such that
  \begin{enumerate}
    \item
$\hat g(\lnot F)=f_{\lnot}(\hat g(F))$ for all $F$ in $\pfx$;
\item
$\hat g(F*G)=f_*(\hat g(F),\hat g(G))$ for all $F$ and $G$ in $\pfx$
  and each binary Boolean connective $*$.
  \end{enumerate}
\end{lemma}

\begin{proof}
  Let $\PF_n(\pvar)$ be the set of elements of $\pfx$ of length at
  most $n$.  Suppose $h_n$ and $h_n'$ have the desired properties of
  $\hat g$, but are defined only on $\PF_n(\pvar)$.  By induction, the
  set
  \begin{equation*}
    \{F\in\pfx\colon h_n(F)=h_n'(F) \text{ or } F\notin\PF_n(V)\}
  \end{equation*}
is just $\pfx$, so $h_n=h_n'$.

Also, in the obvious way, by Lemma \ref{lem:prop:ur}, we can extend
$h_n$ to a function $h_{n+1}$ on $\PF_{n+1}(V)$ having the properties
of $\hat g$.  Finally, $h_0=\emptyset$; so $h_n$ exists uniquely for
all $n$ in $\varN$, and we can let $\hat g=\bigcup_{n\in\varN}h_n$.
\end{proof}

For a first application of Lemma \ref{lem:prop:rec}, we can define
a function 
\begin{equation*}
  F\mapsto\pvar_F\colon\pfx\to \pow{\pvar}
\end{equation*}
by the requirements:
\begin{enumerate}\setcounter{enumi}{-1}
\item
$\pvar_P=\{P\}$ if $P\in\pvar$;
\item
$\pvar_{\lnot F}=\pvar_F$;
  \item
$\pvar_{F*G}=\pvar_F\cup\pvar_G$.
\end{enumerate}

\begin{theorem}
  $\pvar_F$ is the set of variables that actually appear in $F$.  In
  particular, if also $F\in\PF(\pvar')$, then $\pvar_F=\pvar'_F$.
\end{theorem}

For a second application of Lemma \ref{lem:prop:rec}, letting $S$ be
the universe of $\F_2$, we can define
\begin{align*}
  f_{\lnot}(x)&=1+x,\\
f_{\land}(x,y)&=xy,\\
f_{\lor}(x,y)&=x+y+xy,\\
f_{\to}(x,y)&=1+x+xy,\\
f_{\iff}(x,y)&=1+x+y.
\end{align*}
Letting $g$ be a truth-assignment $\chf {\str A}$, we get an extension
$\hatchf {\str A}\colon \pfx\to 2$\label{defn:prop:hatchf}.  

\begin{lemma}\label{lem:prop:ind}
  $\hatchf{\str A}(F)$ depends only on $F$ and $A\cap\pvar_F$, that is,
  \begin{equation*}
     \hatchf{\str A}(F)=\hatchf{\str A'}(F),
  \end{equation*}
where $\str A'=(A',\pvar')$ and $F\in\pfx\cap\PF(\pvar')$, provided
  $A\cap\pvar_F =A'\cap\pvar'_F$. 
\end{lemma}

If $\hatchf {\str A}(F)=1$, we say
that ${\str A}$ is a 
\defn{model} of $F$ and write
\begin{equation*}
  {\str A}\models F.
\end{equation*}
If every structure for $\pvar$ is a model of $F$, then we say $F$ is a
\defn{validity for $\pvar$} and write
\begin{equation*}
\models_{\pvar} F.
\end{equation*}
The \defn{truth-table for $F$} is the function
\begin{equation*}
  A\mapsto\hatchf{\str A}(F)\colon \pow{\pvar_F}\to 2;
\end{equation*}
this is well-defined by Lemma \ref{lem:prop:ind}.
If this function is identically $1$, then we say that $F$ is a
\defn{tautology} and write
\begin{equation*}
  \proves F.
\end{equation*}

\begin{theorem}[Completeness]\label{thm:prop:completeness}
For all $F$ in $\pfx$,
\begin{equation*}
  \models_{\pvar} F\Iff{}\proves F.
\end{equation*}
\end{theorem}
Hence we may write the single symbol $\models$ in place of
$\models_{\pvar}$ and
$\proves$.  If $\Phi\included\pfx$, and $\str A$ is a model of every
formula in $\Phi$, then $\str A$ is a \defn{model} of $F$, and we can
write
\begin{equation*}
  \str A\models\Phi.
\end{equation*}

\begin{theorem}[Compactness]\label{thm:prop:compactness}
A set $\Phi$ of propositional formulas for a countable set of variables has a
model if and only if each finite subset of $\Phi$ has a model.
\end{theorem}

If every model of a set $\Phi$ of formulas is a model of some formula
$F$, then $F$ is a 
\defn{(logical) consequence} of $\Phi$, and we can write
\begin{equation*}
  \Phi\models F.
\end{equation*}
Also, $F\models G$ means $\{F\}\models G$.  In this case, if also
$G\models F$, then $F$ and $G$ are \defn{(logically) equivalent}, and
we may write 
\begin{equation*}
  F\lequiv G.
\end{equation*}

\begin{lemma}\label{lem:prop:iff}
  For all $F$ and $G$ in $\pfx$,
  \begin{equation*}
    F\lequiv G\Iff \models F\iff G.
  \end{equation*}
\end{lemma}

\begin{lemma}\label{lem:prop:simp}
  For all $F$ and $G$ in $\pfx$,
  \begin{align*}
    (F\lor G)&\lequiv\lnot(\lnot F\land\lnot G),\\
(F\to G)&\lequiv(\lnot F\lor G),\\
(F\iff G)&\lequiv((F\to G)\land (G\to F)).
  \end{align*}
\end{lemma}

\begin{remark}\label{rem:prop:sh}
  By Lemma \ref{lem:prop:simp}, one can show that every
  equivalence-class of formulas 
  contains a formula 
  whose only Boolean connectives are $\lnot$ and $\land$.  
\end{remark}


\begin{theorem}[Adequacy]
  Let $A$ be a finite non-empty set of variables.  Every function from
  $\pow A$ to $2$ is the truth-table for some propositional formula.
\end{theorem}

\begin{proof}
  We shall use induction on the size of $A$.  If $A=\{P\}$, then the
  truth-tables of $P$, $\lnot P$, $(P\land\lnot P)$ and $(P\lor\lnot
  P)$ are just the $4$ possible functions from $\pow A$ to $2$.

Suppose $A$ has size $n$, and $P$ is a variable not in $A$, and $f$ is
a function from $\pow{A\cup\{P\}}$ to $2$.  Let $f_0$ be the
restriction of $f$ to $\pow A$, and let $f_1$ be the function
\begin{equation*}
  B\mapsto f(B\cup\{P\})\colon \pow A\to 2.
\end{equation*}
Then for all $B$ in $\pow{A\cup\{P\}}$ we have
\begin{equation*}
  f(B)=
  \begin{cases}
    f_0(B\setminus\{P\}),& \text{ if }P\notin B;\\
f_1(B\setminus\{P\}),& \text{ if }P\in B.
  \end{cases}
\end{equation*}
Now let $F$ be a formula
$((F_0\land\lnot P)\lor(F_1\land P))$,
where $F_0$ and $F_1$ are formulas whose variables are from $A$.  If
$B\included A\cup\{P\}$, then
\begin{equation*}
  \hatchf B(F)=
  \begin{cases}
    \hatchf{B\setminus\{P\}}(F_0),&\text{ if }P\notin B;\\
\hatchf{B\setminus\{P\}}(F_1),&\text{ if }P\in B.
  \end{cases}
\end{equation*}
Hence, if $f_0$ and $f_1$ are the truth-tables for $F_0$ and $F_1$
respectively, then $f$ is the truth-table for $F$.
\end{proof}

\begin{remark}
We might define \defn{propositional logic} as the use of formulas to
  represent functions from the power-sets of finite sets to $2$.
  We may then say that our particular propositional logic uses the
  \defn{signature} $\{\land,\lor,\lnot{},\to,\iff\}$.  The last
  theorem shows that this signature is \defn{adequate} to the task of
  representing these functions; in fact, the theorem shows that
  $\{\land,\lor,\lnot\}$ is adequate.  We then have, by Remark
  \ref{rem:prop:sh}, 
  that the signature $\{\land,\lnot\}$ is adequate.
In fact,
  one could get by with a single connective, namely the binary connective
  $\shstroke$ such that
  \begin{equation*}
    F\shstroke G\lequiv\lnot(F\land G);
  \end{equation*}
this connective is called the \defn{Sheffer stroke}, although Church
in \cite[n.~207, pp.~133 f.]{MR18:631a} says that Sheffer never used
the stroke this way.
\end{remark}

\section{First-order logic}

We now define \defn{first-order structures} and their signatures.  The
structures are primary in interest, but in giving definitions, it is
easier to start with signatures.

\begin{remark}\label{rem:1:R}
  A standard example of a first-order structure is $\R$, considered as
  the $7$-tuple $(R,+,-,\cdot,0,1,\leq)$, where $R$ is the \emph{set} of
  real numbers.  A group is a first-order structure when considered as
  the ordered quadruple $(G,\cdot,{}\inv,1)$; but it is \emph{not}
  first-order when one considers it to be equipped also with the
  operation $S\mapsto\langle S\rangle$ that assigns to each subset the
  subgroup that it generates.
\end{remark}

A \defn{(first-order) signature} is a set, each of whose members
can be uniquely
recognized as a \defn{function-}, \defn{relation-} or
\defn{constant-symbol}.  Each of the func\-tion- and relation-symbols
has an \defn{arity}: each of these symbols is \defn{$n$-ary} for some
unique positive integer $n$. 

Let $\lang$ be a signature.  Let $f$, $R$ and $c$ be arbitrary
function-, relation- and constant-symbols, respectively, of $\lang$,
and let $n$ stand for the arity of $f$ or $R$.
An \defn{$\lang$-structure} is an ordered pair
\begin{equation*}
  (M,\interp),
\end{equation*}
where $M$ is a non-empty set, and $\interp$ is a function
$s\mapsto s^{\str M}$ on $\lang$ such that
\begin{itemize}
  \item
$f^{\str M}$ is a $n$-ary operation on $M$, that is, a function from
    $M^n$ to $M$;
\item
$R^{\str M}$ is an $n$-ary relation on $M$, that is, a subset of $M^n$;
\item
$c^{\str M}\in M$.
\end{itemize}
The structure itself can be denoted $\str M$.  The set $M$ is the
\defn{universe} of $\str M$, and each image $s^{\str M}$
is the \defn{interpretation} of $s$ in $\str M$.  

\begin{remark}
A structure can be considered as its universe together with the
interpretations of the symbols in its signature.  This is how $\R$ was
presented in Remark \ref{rem:1:R}.  A structure without any relations
can be called an \defn{algebra}.  Theorem \ref{lem:prop:rec} involves
an algebra, namely
$(S,f_{\land},f_{\lor},f_{\lnot},f_{\to},f_{\iff})$.  The natural
numbers compose the algebra $(\varN,{}\vscr{},0)$, where
${}\vscr{}$ is the successor-operation.  The complete set of
propositional formulas in some set
of variables is the universe of an algebra in an obvious way. 
\end{remark}

Subsets of $M^0$ are \defn{nullary} relations.  There are only two of
these, namely $0$ and $1$, which we may read as before as `false' and
`true'.



Let $\ivar$ be set of new symbols, called \defn{(individual-)
  variables}.  We shall
develop a \defn{language}, which we might denote
\begin{equation*}
  \lang^{\ivar}.
\end{equation*}
The symbols of $\lang^{\ivar}$ will compose the disjoint union
\begin{equation*}
  \ivar\cup\lang\cup\{=\}\cup S\cup\{\exists x:x\in \ivar\},
\end{equation*}
where $S$ is an adequate signature for a propositional logic (along
with brackets, if one is using them).  Let us consider $S$ to be the
signature $\{\land,\lnot\}$.
Note that each $\exists x$ is an indivisible symbol, in which, however, the
original $x$ can be recognized.
The symbols that are not in $X\cup\lang$ are
\defn{logical} symbols.
In every $\lang$-structure $\str M$, each symbol $s$ of
$\lang^{\ivar}$ has an interpretation (rather, a 
family of interpretations)
$s^{\str M}$.  We have defined the interpretations of the
elements of $\lang$.
The interpretations of the rest of the symbols of $\lang^{\ivar}$ are
certain operations or, in one case, a relation, associated with
appropriate finite subsets $I$ of $\ivar$: 
\begin{itemize}
  \item
If $x\in I$, then $x^{\str M}$ is $\tuple a\mapsto a_x\colon \mapset IM\to M$.
\item
$=^{\str M}$ is equality, a subset of $M^2$.
\item
$\land^{\str M}$ is $(A,B)\mapsto A\cap B\colon \pow {\mapset
  IM}\times\pow{\mapset IM}\to \pow{\mapset IM}$ for any $I$. 
\item
$\lnot^{\str M}$ is $A\mapsto A\comp\colon \pow{\mapset IM}\to\pow{\mapset
  IM}$ for any $I$.
\item
$\exists x^{\str M}$ is, for any $I$, the map from $\pow{\mapset IM}$
  to $\pow{M^{I\setminus\{x\}}}$ induced by the projection 
$\tuple a\mapsto (a_i:i\in I\setminus\{x\}):\mapset IM\to
M^{I\setminus\{x\}}$.
\end{itemize}
The symbols of $\lang^{\ivar}$ compose strings of various kinds, and each
of these strings has a family of interpretations.
Certain strings are called \defn{terms}, and their interpretations are
functions.  For each term $t$
and for each finite set $I$ of variables that contains the variables in
$t$, there will be an interpretation $t^{\str M}:\mapset IM\to M$.
The precise definitions are thus: 
\begin{itemize}
  \item
Each $c$ is a term, and $c^{\str M}$, besides being an element of $M$,
can also be understood as the constant-function $\tuple
a\mapsto c^{\str M}\colon \mapset IM\to M$. 
\item
Each variable $x$ is a term, interpreted as above.
\item
If $t_0$, \dots, $t_{n-1}$ are terms, then
$ft_0\dots t_{n-1}$ is a term, with interpretation 
\begin{equation*}
  \tuple a\mapsto
f^{\str M}(t_0^{\str M}(\tuple a),\dots,t_{n-1}^{\str M}(\tuple
a))\colon \mapset IM\to M.
\end{equation*}
\end{itemize}

The \defn{formulas} are certain strings whose interpretations are
relations. 
For any \defn{atomic} formula $\alpha$ and any finite set $I$ of
variables that contains the variables appearing in $\alpha$, there
will be an interpretation $\alpha^{\str M}$ that is a subset of
$\mapset IM$.  The precise definitions are:
\begin{itemize}
  \item
If $t_0$, \dots, $t_{n-1}$ are terms, then
$Rt_0\dots t_{n-1}$ is an atomic formula, with interpretation
$\{\tuple a\in \mapset IM:(t_0^{\str M}(\tuple a),\dots,t_{n-1}^{\str
  M}(\tuple a))\in R^{\str M}\}$.
\item
If $t_0$ and $t_1$ are terms, then $t_0=t_1$ is an atomic formula,
with interpretation $\{\tuple a\in\mapset IM:t_0^{\str
  M}(\tuple a)=t_1^{\str M}(\tuple a)\}$.
\end{itemize}
The formulas in general are built up using the remaining logical symbols:
The atomic formulas are formulas, and if $\phi$ and $\psi$ are
formulas, then so are $(\phi\land\psi)$, $\lnot\phi$ and
$\Exists x\phi$ for any $x$ in $\ivar$.  The interpretations are
obvious:
\begin{itemize}
  \item
$(\phi\land\psi)^{\str M}=\phi^{\str M}\cap\psi^{\str M}$;
\item
$\lnot\phi^{\str M}=(\phi^{\str M})\comp$;\
\item
$\Exists x\phi^{\str M}=\exists x^{\str M}(\phi^{\str M})$.
\end{itemize}
In particular, if $\phi^{\str M}$ is a well-defined
subset of $\mapset IM$, then $\Exists x\phi^{\str M}$ is a
  well-defined subset of $\mapset{I\setminus\{x\}}M$.  Thus, the
  nullary relations $0$ and $1$ can arise as
  interpretations.  To say precisely when they can arise, we recursively
  define the set $\fv{\phi}$ of \defn{free variables} of an arbitrary
  formula $\phi$:
  \begin{itemize}
    \item
$\fv{\alpha}$ is the set of variables appearing in $\alpha$, if
      $\alpha$ is atomic;
\item
$\fv{\lnot\phi}=\fv{\phi}$;
\item
$\fv{\phi\land\psi}=\fv{\phi}\cup\fv{\psi}$;
\item
$\fv{\Exists x\phi}=\fv{\phi}\setminus\{x\}$.
  \end{itemize}
Then $\phi^{\str M}$ is defined as a subset of $\mapset IM$, provided
$\fv{\phi}\included I$.

\begin{theorem}[Substitution]
Suppose the following:
\begin{itemize}
  \item
$\phi$ is a formula of $\lang^{\ivar}$;
\item
 $I$ is a finite
  subset of $\ivar$ such that $\fv{\phi}\included I$;
\item
 $\tuple u$ is an $I$-tuple of terms of $\lang^{\ivar}$;
\item
$J$ is a finite subset of $\ivar$ that contains all variables in the entries
  in $\tuple u$.  
\end{itemize}
Then there is a formula $\phi(\tuple u)$ of
  $\lang^{\ivar}$ such that $\fv{\phi(\tuple u)}\included J$ and, for
  every $\lang$-structure $\str M$, and for all $\tuple a$ in $\mapset
  JM$, 
  \begin{equation*}
    \tuple a\in\phi(\tuple u)^{\str M}\Iff (u_i^{\str M}(\tuple
    a):i\in I)\in\phi^{\str M}.
  \end{equation*}
\end{theorem}

\begin{example}
  If $\fv{\phi}\included I$, and $\tuple x$ is the identity on $I$ (so
  $\tuple x=(x:x\in I)$), then we may assume that $\phi(\tuple x)$ is
  the same formula as $\tuple x$.
\end{example}

A \defn{sentence} is a formula with no free variables.  If
$\sigma$ is a sentence of $\lang^{\ivar}$, and $\sigma^{\str
  M}=1$, then we say that $\str M$ is a \defn{model} of $\sigma$.

\begin{example}
  If $\fv{\phi}\included I$, and $\tuple a$ is an $I$-tuple of
  constant-symbols, then $\phi(\tuple c)$ is a sentence $\sigma$ such
  that
  \begin{equation*}
    \sigma^{\str M}=1\Iff \tuple c^{\str M}\in\phi^{\str M},
  \end{equation*}
where $\tuple c^{\str M}$ is $(c_i^{\str M}:i\in I)$.
\end{example}

We can also allow structures to be models of arbitrary formulas.
Suppose $\phi$ is a formula of $\lang^{\ivar}$ and
$\fv{\phi}\included I$.  If $\tuple c$ is an $I$-tuple of
constant-symbols that are \emph{not} in $\lang$, and $\tuple a$ is an
$I$-tuple from $M$, then $(\str M,\tuple a)$ is a structure of
$\lang\cup\{c_x:x\in I\}$ in the obvious way.  Then $\str M$ is a
model of $\phi$, provided $(\str M,\tuple a)$ is a model of
$\phi(\tuple c)$ for \emph{some} tuple $\tuple a$.

The notations of \S~\ref{sect:prop} involving $\models$ now make sense
in the present context.  If $\str M\models\phi$, we say also that
$\str M$ \defn{satisfies} $\phi$.

We may let $\lang(M)$ be the disjoint union $\lang\sqcup M$, where each
element of $M$ is understood as a constant-symbol whose interpretation
in $\str M$
is itself.  Then we may ask whether $\str M$ is a model of a formula
of $\lang(M)^{\ivar}$.

In the following, $\exists\tuple x$ is an abbreviation for
\begin{equation*}
  \Exists{x_0}\Exists{x_1}\dots \Exists{x_{n-1}},
\end{equation*}
where $I=\{x_0,\dots,x_{n-1}\}$.

\begin{lemma}
Suppose $\str M$ is an $\lang$-structure, and $\fv{\phi}\included I$.
  The following are equivalent:
  \begin{enumerate}\setcounter{enumi}{-1}
    \item
$\str M$ satisfies $\phi$;
\item
$\str M\models\phi(\tuple a)$ for some $\tuple a$ in $\mapset IM$;
\item
$\str M\models\Exists{\tuple x}\phi(\tuple x)$.
  \end{enumerate}
\end{lemma}

\section{Types}

Now suppose that the set $\ivar$ of individual-variables is
$\{x_i:i\in\varN\}$, and write $\lang^{\ivar}$ just as $\lang$.  On
the set of formulas of $\lang$ with free variables in $\{x_i:i<n\}$,
the relation $\lequiv$ is an equivalence-relation; let us denote the
set \modulo\ the relation by
\begin{equation*}
  \Fm n(\lang).
\end{equation*}
Then $\land$ and $\lnot$ (and hence $\lor$) are well-defined
operations on $\Fm n(\lang)$, which is also partially ordered by
$\models$ and, with respect to this, has a greatest element $\true$
and a least element $\false$.

An \defn{$n$-type of $\lang$} is a subset $\Gamma$ of $\Fm n(\lang)$
  such that
  \begin{itemize}
    \item
$\phi,\psi\in\Gamma\implies \phi\land\psi\in\Gamma$;
\item
$\phi\in\Gamma\mathrel{\&}\phi\models\psi\implies\psi\in\Gamma$;
\item
$\true\in\Gamma$;
  \end{itemize}
the type is \defn{proper} if 
$\false\notin\Gamma$; if proper,
the type is \defn{complete} if
\begin{itemize}
  \item
$\phi\in\Fm n(\lang)\setminus\Gamma\implies \lnot\phi\in\Gamma$.
\end{itemize}
The unique \defn{improper} $n$-type is $\Fm n(\lang)$
itself.  Every subset of $\Fm n(\lang)$ generates a
type, possibly improper.  The subset itself can be called
\defn{consistent} or \defn{finitely satisfiable} if for every finite
subset $\{\phi_i:i<m\}$ there is a structure satisfying
$\bigwedge_{i<m}\phi_i$. 

\begin{lemma}
A subset of $\Fm n(\lang)$ is finitely satisfiable if and only if it
  generates a proper type.
\end{lemma}

In fact the structure $(\Fm
n(\lang),\land,\lor,\lnot,\false,\true,\models)$ is a \tech{Boolean
  algebra}.  A standard Boolean algebra is
\begin{equation*}
  (\pow{X},\cap,\cup,{}\comp,\emptyset,X,\included),
\end{equation*}
where $X$ is a set.  One way to give a formal definition is the
following.   A \defn{Boolean ring} is a (unital, associative) ring
satisfying $\Forall x x\cdot x=x$.

\begin{lemma}
  Boolean rings are commutative and are of characteristic $2$.
\end{lemma}

\begin{example}
  $\F_2$ is a Boolean ring.
\end{example}

Let $(B,+,\cdot,0,1)$ be a Boolean ring, and define new operations and
a relation on $B$ by the following rules (which should be compared
with the definition of $\hatchf{\str A}$ on
p.~\pageref{defn:prop:hatchf}): 
\begin{itemize}
  \item
$x\land y=xy$;
\item
$x\lor y=x+y+xy$;
\item
$\lnot x=1+x$;
\item
$x\leq y \Iff x\land y=x$;
\item
$\false=0$ and $\true=1$.
\end{itemize}
The structure $(B,\land,\lor,\lnot,\false,\true,\leq)$ arising thus is
a \defn{Boolean algebra}.

\begin{lemma}
  If $(B,\land,\lor,\lnot,\false,\true,\leq)$ is a Boolean algebra,
  then the Boolean ring from which it arises is given by
  \begin{itemize}
    \item
$xy=x\land y$;
\item
$x+y=\lnot(\lnot x\land\lnot y)\land\lnot(x\land y)$;
\item
 $\true=1$ and $\false=0$.
  \end{itemize}
\end{lemma}

\begin{lemma}
  $\Fm n(\lang)$ is a Boolean algebra.
\end{lemma}

A subset $F$ of a Boolean algebra is a \defn{filter} if the set
$\{x:\lnot x\in F\}$ is an ideal of the corresponding ring; $F$ is
\defn{principal} if $I$ is principal; $F$ is an
\defn{ultra-filter} if $I$ is maximal.  (The unique improper filter is
the algebra itself; an ultra-filter must be proper.)

\begin{lemma}
  Types of $\Fm n(\lang)$ are just filters; complete types are just
  ultra-filters. 
\end{lemma}

The set of ultra-filters of a Boolean algebra $\str B$ is denoted
\begin{equation*}
  \Stone{\str B}
\end{equation*}
and called its \defn{Stone space}, because of the following.  If $x\in
B$, let
\begin{equation*}
  [x]
\end{equation*}
be the subset $\{F:x\in F\}$ of $\Stone{\str B}$.

\begin{theorem}[Stone Representation]
If $\str B$ be a Boolean algebra, then the map 
  \begin{equation*}
      x\mapsto[x]:\str
  B\to\pow{\Stone{\str B}}
  \end{equation*}
 is an embedding of Boolean algebras.  
\end{theorem}

\begin{corollary}\label{cor:Sc}
  The subsets $[x]$ of $\Stone{\str B}$ compose a basis of open sets
  and of closed sets for a topology on $\Stone{\str B}$, which topology is
  compact and Hausdorff.
\end{corollary}

  For every subset $X$ of $B$, let $\cl X$ be
  the subset
  $\bigcap_{x\in X}[x]$ of $\Stone{\str B}$.  

  \begin{lemma}
Suppose $\str B$ is a Boolean algebra.
\begin{enumerate}\setcounter{enumi}{-1}
\item
The map
  \begin{equation*}
    X\mapsto \cl X:\pow{B}\to\pow{\Stone{\str B}}
  \end{equation*}
is inclusion-reversing and takes unions to intersections, and its
range is the set of closed subsets of $\Stone{\str B}$.
\item
The map
\begin{equation*}
  Y\mapsto\bigcap Y:\pow{\Stone{\str B}}\to\pow{\str B}
\end{equation*}
is inclusion-reversing and takes unions to intersections, and its
range is the set of filters of $\str B$.
\item
If $X\included B$, then $\bigcap\cl X$ is the filter of $\str B$
generated by $X$.
\item
If $Y\included\Stone{\str B}$, then $\cl{\bigcap Y}$ is the
topological closure of $Y$.
\end{enumerate}
hence $X\mapsto\cl X$ gives a one-to-one correspondence, with inverse
$Y\mapsto\bigcap Y$, between filters of $\str B$ and closed subsets of
$\Stone{\str B}$.
  \end{lemma}

So the complete $n$-types of $\lang$ compose a compact Hausdorff space,
denoted
\begin{equation*}
  \ts n{\lang},
\end{equation*}
whose closed subsets are just the sets $\cl{\Gamma}$ determined by
arbitrary $n$-types $\Gamma$.

A \defn{theory} of $\lang$ is a $0$-type  The improper $0$-type of
$\lang$ is the unique \defn{inconsistent} theory of $\lang$.

Since $\Fm
0(\lang)$ embeds in $\Fm n(\lang)$, a theory $T$ of $\lang$ determines
a closed subset of $\ts n{\lang}$, denoted
\begin{equation*}
  \ts n T.
\end{equation*}
Then an arbitrary $n$-type $\Gamma$ is 
\defn{consistent with $T$} if $\Gamma\cup T$ is consistent,
equivalently, $\cl{\Gamma}\cap\ts nT\neq0$.

\begin{theorem}[Compactness]
  Every consistent theory has a model.
\end{theorem}

\begin{proof}
  Let $T$ be a theory of $\lang$.  The proof that $T$ has a model has
  three parts:
  \begin{enumerate}\setcounter{enumi}{-1}
    \item
There is a signature $\lang'$ such that
$\lang\included\lang'$, and $\lang'\setminus\lang$ consists of
constant-symbols, and there is a bijection
\begin{equation*}
  \phi\mapsto c_{\phi}:\Fm 1(\lang')\to\lang'\setminus\lang.
\end{equation*}
  \end{enumerate}
Now let $H(T)$ be the set
\begin{math}
\ts 0T\cap\bigcap_{\phi\in\Fm 1(\lang')}[\Exists
  {x_0}\phi\to\phi(c_{\phi})]  
\end{math}.
\begin{enumerate}\setcounter{enumi}{0}
\item
Let $T'$ be an element of $H(T)$.
Then $T'$ has a \defn{canonical model}, whose
  universe is $\lang'\setminus\lang$ \modulo\ the equivalence-relation
 $\sim$ given by
  \begin{equation*}
    c\sim d\Iff T'\models c=d.
  \end{equation*}
  \item
$H(T)$ is non-empty.
  \end{enumerate}
Note that $H(T)$ is non-empty by Corollary \ref{cor:Sc}, in
particular, compactness of $\ts 0T$.
\end{proof}

If $\Gamma$ is an $n$-type, and $\tuple c$ is an $n$-tuple of
constant-symbols, then the set $\{\phi(\tuple c):\phi\in\Gamma\}$ can
be denoted
\begin{equation*}
  \Gamma(\tuple c).
\end{equation*}
A structure $\str M$ \defn{realizes} $\Gamma$ if $\str
M\models\Gamma(\tuple a)$ for some tuple
$\tuple a$ from $M$; otherwise the structure \defn{omits} the type.

An complete type $p$ is: \defn{isolated}, if $\{p\}$ is open;
\defn{limit}, if not.  These definitions can be understood absolutely,
as stated, or \defn{over} some theory $T$.  

\begin{lemma}
  The isolated types are precisely the principal complete types.
  Every type included in a principal type over a \emph{complete}
  theory $T$ is realized in every model of $T$.  If $\Gamma$ is a type
  consistent with an (arbitrary) theory $T$, then the following are
  equivalent:
  \begin{enumerate}\setcounter{enumi}{-1}
\item
$\Gamma$ is not included in a principal type over $T$;
\item
$\cl{\Gamma}$ has empty interior in $\ts nT$;
\item
$\cl{\Gamma}\comp$ is a dense open subset of $\ts nT$.
  \end{enumerate}
\end{lemma}

\begin{example}
  Let $\lang$ be $\{c_n:n\in\varN\}\cup\{P\}$, where the $c_n$ are
  constant-symbols and $P$ is a unary relation-symbol.  Let $T$ be the
  theory generated by $\{Pc_n:n\in\varN\}$.  Then
  \begin{equation*}
    T\models \lnot Px\to x\neq c_n
  \end{equation*}
for each $n$, so the principal type generated by $\lnot Px$ includes
the type generated by $\{x\neq c_n:n\in\varN\}$; but the latter type
is not principal.
\end{example}

A partial converse is the Omitting-Types Theorem below, whose proof is
based on \cite[ch.\ 10]{MR2001a:03072}.  First:

\begin{lemma}\label{lem:Baire}
The intersection of countably dense open subsets of a
compact Hausdorff space is also dense.  
\end{lemma}

\begin{proof}
  Suppose $X$ is a compact Hausdorff space.  Then $X$ is locally
  compact, that is, every neighborhood of every point includes a
  compact neighborhood.  Indeed, let $U$ be an open neighborhood of
  $P$.  For each $x$ in $U\comp$ there are disjoint open neighborhoods
  $V_x$ and $U_x$ of $x$ and $P$ respectively.  Some finite union of
  sets $V_x$ covers $U\comp$; the complement is included in $U$ and is
  a closed---hence compact---neighborhood of $P$, since it includes
  the corresponding intersection of sets $U_x$.

Now suppose $\{O_n:n\in\varN\}$ is a collection of dense open subsets
of $X$.  We can recursively define a decreasing chain
  $U_0\includes K_0\includes U_1\includes K_1\includes
U_2\includes\dots$ of sets,
and at the same time a sequence $(P_n:n\in\varN)$ of points, such
that: 
\begin{itemize}
\item  
$U_0=U$;
\item
$U_n$ is open;
\item
$P_n\in U_n\cap O_n$;
\item
$K_n$ is compact, and $P_n\in K_n\included U_n\cap O_n$; 
\item
$P_n\in U_{n+1}\included K_n$. 
\end{itemize}
Then $\bigcap_{n\in\varN}K_n$ is a nonempty subset of $U$ included in
each set $O_n$.
\end{proof}

\begin{theorem}[Omitting Types]
  Let $T$ be a consistent theory of a countable signature $\lang$.  For every
  countable collection of types $\Gamma$, none included in a principal
  type,
  $T$ has a countable model omitting each $\Gamma$.
\end{theorem}

\begin{proof}
  To the proof of the Compactness Theorem, we add a step:
  \begin{enumerate}\setcounter{enumi}{2}
    \item
$H(T)$ has an element $T'$ such that, for each tuple $\tuple c$ of
      elements of $\lang'\setminus\lang$, and for each $\Gamma$,
      \begin{equation*}
	T'\notin\cl{\Gamma(\tuple c)},
      \end{equation*}
that is, $\Gamma(\tuple c)\not\included T'$.
  \end{enumerate}
To prove this, by Lemma \ref{lem:Baire}, it is enough to show that
each closed set 
$\cl{\Gamma(\tuple c)}$ has dense complement in $H(T)$, since then the
intersection of these complements is dense and so non-empty.

Every open subset of $H(T)$ is a union of sets $[\psi(\tuple d)]\cap H(T)$,
where $\psi$ is a formula of $\lang$, and $\tuple d$ is a tuple of
elements of $\lang'\setminus\lang$.  Supposing 
\begin{equation*}
  T'\in[\psi(\tuple d)]\cap H(T),
\end{equation*}
 we shall derive an element $T^*$ of
$[\psi(\tuple d)]\cap H(T)\setminus\cl{\Gamma(\tuple c)}$.

Each entry of $(\tuple c,\tuple d)$ is $c_{\phi^0}$ for some formula
$\phi^0$, which contains finitely many constant-symbols $c_{\phi^1}$;
each $\phi^1$ contains finitely many
constant-symbols $c_{\phi^2}$, and so on.  The constant-symbols
arising in this way form a finitely branching tree with no infinite
branches; hence they are finitely numerous and compose a tuple $\tuple
e$.

Hence if $c_{\phi}$ is one of the terms of $(\tuple c,\tuple d,\tuple
e)$, then the constant-symbols used in $\phi$ also appear in  $(\tuple
c,\tuple d,\tuple e)$.  Hence there is a formula $\theta$ of $\lang$
such that $\theta(\tuple c,\tuple d,\tuple e)$ is the conjunction of
$\psi(\tuple d)$ and the sentences
\begin{equation*}
  \exists x_0\phi\to\phi(c_{\phi})
\end{equation*}
such that $c_{\phi}$ appears in $(\tuple c,\tuple d,\tuple e)$.

Let $\str M$ be the canonical model of $T'$.  Then $\str
M\models\theta(\tuple c,\tuple d, \tuple e)$.  The open set
$[\Exists{\tuple y}\Exists{\tuple z}\theta(\tuple x,\tuple y,\tuple
  z)]$ is therefore a non-empty subset of $\ts nT$, so it is not
included in $\cl{\Gamma}$.  Suppose
\begin{equation*}
  p\in [\Exists{\tuple y}\Exists{\tuple z}\theta(\tuple x,\tuple y,\tuple
  z)]\setminus\cl{\Gamma}. 
\end{equation*}
By the Compactness Theorem, $T$ has a countable model $\str N$
realizing $p$ with some tuple $\tuple a$.  There is a bijection $f$
between $\lang'\setminus \lang$ and $N$ such that $f(\tuple c)=\tuple
a$ and
\begin{equation*}
  \str N\models\theta(f(\tuple c,\tuple d,\tuple e)).
\end{equation*}
This bijection determines the desired $T^*$.
\end{proof}



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

\newpage

\section*{Hints}
\begin{itemize}
  \item
Lemma \ref{lem:prop:rec}:  Prove that for each $n$ there is a unique
such function on the set of formulas of length at most $n$.
\item
Theorem \ref{thm:prop:completeness}:  It's a simple chain of
equivalences, justified by Lemma \ref{lem:prop:ind}.
\item
Theorem \ref{thm:prop:compactness}:  Say $\pvar=\{P_n:n\in\varN\}$.
Define $\pvar_n=\{P_i:i<n\}$.  Let $T$ be the set of structures on the
various $\pvar_n$.  Order $T$ by the rule
\begin{equation*}
  (A,\pvar_m)\leq(B,\pvar_n)\Iff m\leq n\land A=\pvar_m\cap B.
\end{equation*}
Then $(T,\leq)$ is a tree.  Consider the set comprising those
$(A,\pvar_m)$ such that, for all $F$ in $\Phi$, if
$\pvar_F\included\pvar_m$, then $(A,\pvar_m)\models F$.  This set
forms an infinite sub-tree of $T$.  Hence the sub-tree includes an
infinite chain.
\item
Lemma \ref{lem:prop:iff}:  Use $f_{\iff}$.
\item
Lemma \ref{lem:prop:simp}:  Use the various $f_*$.
\end{itemize}


\end{document}