\documentclass[twoside,a4paper,12pt,draft]{article}
\usepackage{amssymb,amsmath,amsthm}
\title{Model-theory homework}
\date{2001, fall}
\author{Math 736---David Pierce}
\pagestyle{myheadings}
 \markboth{Model-theory homework III}{Math 736, fall 2001}

 \addtolength{\voffset}{-2cm}
 \addtolength{\textheight}{4cm}

 \newtheorem{lemma}{Lemma}
 %\setcounter{lemma}{-1}
 \theoremstyle{definition}
 \newtheorem{problem}{Problem}


\newcommand{\Z}{\mathbf Z}          % the integers
\newcommand{\Q}{\mathbf Q}          % the rationals
%\newcommand{\A}{\mathbf A}          % affine space
\newcommand{\R}{\mathbf R}          % the reals
\newcommand{\N}{\mathbf{N}}         % the naturals
\newcommand{\C}{\mathbf{C}}         % the complex numbers
\newcommand{\F}{\mathbf{F}}         % (finite) field

\newcommand{\id}{\mathrm{id}}       % identity-function

\newcommand{\unit}[1]{{#1}^{\times}} % group of units of a ring

\newcommand{\stroke}{\mathrel{|}}   % stroke for semi-group example

\newcommand{\str}[1]{\mathcal{#1}}  % structure with universe #1

%I don't like the standard loose inequalities
\renewcommand{\leq}{\leqslant}
\renewcommand{\nleq}{\nleqslant}
\renewcommand{\geq}{\geqslant}

%I don't much like the standard here either:
\renewcommand{\setminus}{-}

%I don't want epsilon to look like `is an element of'
\renewcommand{\epsilon}{\varepsilon}

\newcommand{\To}{\longrightarrow}

\newcommand{\mapset}[2]{#2^{#1}}

\newcommand{\Mod}{\mathfrak{Mod}}
\DeclareMathOperator{\Th}{Th}
\newcommand{\pow}{\mathcal{P}}
\newcommand{\K}{\mathcal{K}}
\newcommand{\arity}[1]{\textrm{arity}(#1)}
\newcommand{\proj}{\pi}
\newcommand{\inv}{^{-1}}
\newcommand{\Fm}[1]{\mathrm{Fm}^{#1}}
\newcommand{\Fmo}[1]{\mathrm{Fm}^{#1}_0}
\newcommand{\2}{\mathbf{F}_2}

\newcommand{\abs}[1]{\lvert#1\rvert}
\newcommand{\elsub}{\preccurlyeq}
\newcommand{\Ba}{\mathcal{M}^\mathrm{a}}  % a Boolean algebra
\newcommand{\Br}{\mathcal{M}^\mathrm{r}}  % a Boolean ring

\DeclareMathOperator{\diag}{diag}   % Robinson diagram of a structure

\DeclareMathOperator{\sgn}{sgn}     % signum of a permutation

\newcommand{\included}{\subseteq}   % the name suggests the meaning here
\newcommand{\lang}{\mathcal L}      % a language
\newcommand{\SL}{\mathrm{PL}}       % Propositional (was sentential) logic
\newcommand{\pairing}[1]{\langle#1\rangle} % pairing

\newtheorem*{theorem}{Theorem}
%\newtheorem*{lemma}{Lemma}
\newtheorem*{corollary}{Corollary}

\theoremstyle{remark}
\newtheorem*{remark}{Remark}
\newtheorem*{example}{Example}
\newtheorem*{examples}{Examples}

%  For distinguishing claims made and proved within proofs
%\newtheoremstyle{subclaim}{0pt}{0pt}{\itshape}{}{\bfseries}{}{0em}{}
%\theoremstyle{subclaim}
%\newtheorem*{claim}{}

\newcommand{\tuple}{\mathbf}
\newcommand{\reduct}{\overline}

%  Should the word `modulo' be italicized?
\newcommand{\modulo}{\emph{modulo}\ }

%  To distinguish terms being defined
\newcommand{\defn}[1]{{\bf#1}}

\begin{document}
%\maketitle
\thispagestyle{empty}

\noindent\emph{Homework III, Math 736, Model-Theory.}

These notes present an alternative approach to compactness and
completeness.  The proofs of the lemmas are exercises (not necessarily to
be turned in).

Let $\Fm{n}(\lang)$ comprise the $n$-ary formulas of $\lang$, defined as
in the notes (`Homework II') as strings of symbols, but with formulas
$(\phi\to\psi)$ allowed as well, with $(\phi\to\psi)^{\str
M}=(\lnot\phi\lor\psi)^{\str M}$.  We may leave off outer brackets when
writing formulas, and write $\phi_0\land\phi_1*\phi_2$ for
$(\phi_0\land\phi_1)*\phi_2$, where $*$ is $\land$ or $\to$.  Let
$\Fm{}(\lang)$ be the union of the chain
$\Fm{0}(\lang)\included\Fm{1}(\lang)\included\dots$. We shall assume that
all tuples, terms and formulas have the arities they must, for what we
say to make sense.

Let $\Gamma$ be a subset of $\Fm{}(\lang)$, and let $\phi$ be in
$\Fm{}(\lang)$.  We can define
\begin{equation*}
  \Gamma\models\phi
\end{equation*}
to mean that, for every $\str M$ in $\Mod(\lang)$, and for every sequence
$(a_i:i\in\omega)$ of elements of $M$, if $\str M\models\psi(\tuple a)$
for each $\psi$ in $\Gamma$, then $\str M\models\phi(\tuple a)$.  This
agrees with the definition given in class when all formulas are
sentences. We can also say that $\str M$ is a \defn{model} of $\Gamma$,
writing
\begin{equation*}
  \str M\models\Gamma,
\end{equation*}
if there is \emph{some} sequence $(a_i:i\in\omega)$ of elements of $M$
such that $\str M\models\psi(\tuple a)$ for each $\psi$ in $\Gamma$.


We now define
\begin{equation*}
  \Gamma\vdash\phi
\end{equation*}
to mean that $\phi$ is \defn{derivable} from $\Gamma$, in a sense to be
specified presently.  The point of these notes will be to prove that this
definition agrees with the one given in class.  That $\phi$ is derivable
from $\Gamma$ will mean that there is a \defn{proof} of $\phi$ from
$\Gamma$, namely a finite sequence of formulas, ending with $\phi$, of
which each formula:
\begin{itemize}
\item
 is in $\Gamma$,
  \item
 is an \defn{axiom}, or
\item
 follows from
previous formulas in the sequence by a \defn{rule of inference}.
\end{itemize}
Before naming the axioms and rule(s) of inference, we can already check
the following.

\begin{lemma}
If $\Gamma\vdash\phi$, then $\phi$ is derivable from a finite subset of
$\Gamma$.
\end{lemma}

\begin{lemma}
Derivability is \defn{transitive}, in the sense that, if each formula in
a set $\Theta$ is derivable from $\Gamma$, and $\phi$ is derivable from
$\Theta$, then $\Gamma\vdash\phi$.
\end{lemma}

We shall use a single rule of inference, namely \defn{\emph{Modus
Ponens}}:
\begin{equation*}
  \{\phi,(\phi\to\psi)\}\vdash\psi.
\end{equation*}
Our axioms will be the following (where, throughout, $t_i$, $u_i$, $t$,
$u$ and $v$ are terms, and $\phi$ and $\psi$ are formulas of appropriate
arities):
\begin{itemize}
  \item
  the \defn{tautologies}, namely formulas $F(\phi_0,\dots,\phi_{n-1})$,
  where $F$ is a
  \emph{tautologous} $n$-ary
  propositional formula (an $n$-ary term of the language of Boolean algebras whose
  interpretation in $\2$ is the constant-function $1$);
  \item
  the \defn{axioms of equality}, namely:
  \begin{itemize}
  \item
  $(t_0=u_0)\land\dots\land
  (t_{n-1}=u_{n-1})\to(\phi(\tuple t)\to\phi(\tuple u))$;
  \item
  $t=t$;
  \item
  $(t=u)\to (u=t)$;
  \item
  $(t=u)\land(u=v)\to(t=v)$;
  \end{itemize}
  \item
  the \defn{axioms of quantification}, namely:
  \begin{itemize}
  \item
  $\phi(\tuple x,t)\to\exists x_n\,\phi$;
  \item
  $\forall x_n\,\lnot\phi\to\lnot\exists x_n\,\phi$;
  \item
  $\phi\to\forall x_n\,\phi$, where $\phi$ is $n$-ary;
  \item
  $\forall x_n\,(\phi\to\psi)\to(\forall x_n\,\phi\to\forall x_n\,\psi)$;
  \item
  $\forall x_n\,\phi$, where $\phi$ is an axiom.
  \end{itemize}
\end{itemize}

\begin{lemma}
$\Gamma\vdash\phi\implies\Gamma\models\phi$.
\end{lemma}

Changing a notation used in class, let us write
\begin{equation*}
  \phi\approx\psi
\end{equation*}
if $\phi^{\str M}=\phi^{\str M}$ for all $\str M$, and let us now use
\begin{equation*}
  \phi\sim\psi
\end{equation*}
to mean that $\{\phi\}\vdash\psi$ and $\{\psi\}\vdash\phi$.  Both
$\approx$ and $\sim$ are equivalence-relations (and will turn out to be
the same).

\begin{lemma}
$\phi\sim\psi\implies\phi\approx\psi$.
\end{lemma}

\begin{lemma}
If $\Gamma\vdash\phi$, then $\Gamma'\vdash\phi'$, where $\Gamma'$ is got
from $\Gamma$ by replacing each an element with a $\sim$-equivalent one,
and $\phi'\sim\phi$.
\end{lemma}

So, as far as derivability and interpretations are concerned, we can
identify formulas with their $\sim$-classes.  One point of doing this is
the following.

\begin{lemma}
$\Fm{}(\lang)/\!\!\sim$ is naturally the universe of a Boolean algebra.
\end{lemma}

Now define
\begin{equation*}
  \langle\Gamma\rangle=\{\phi:\Gamma\vdash\phi\}.
\end{equation*}
Say that $\Gamma$ is \defn{consistent} if
$\bot\notin\langle\Gamma\rangle$.

\begin{lemma}
If $\Gamma$ is consistent, then the image of $\langle\Gamma\rangle$ in
$\Fm{}(\lang)/\!\!\sim$ is the smallest filter containing the images of
the formulas in $\Gamma$.
\end{lemma}

Now we can prove compactness---that every consistent set of formulas has
a model---just as in class; but we have to do more work at some points.

Derivability depends \emph{a priori} on signature.  We must rule out the
possibility that there is a proof of $\phi$ from $\Gamma$ in a signature
larger than $\lang$, but not in $\lang$ itself.

\begin{lemma}
Suppose $\Gamma\included\Fm{n}(\lang)$, and
$\phi\included\Fm{n+k+1}(\lang)$, and $c$ is a $k+1$-tuple of
constant-symbols not in $\lang$.
\begin{itemize}
  \item
  If $\Gamma\vdash\phi$, then $\Gamma\vdash\forall x_n\dots\forall
  x_{n+k}\,\phi$.
  \item
  If $\Gamma\vdash\phi(\tuple x,\tuple c)$ in $\lang\cup\{c_0,\dots,c_k\}$, then
  $\Gamma\vdash\forall x_n\dots\forall
  x_{n+k}\,\phi$ in $\lang$.
\end{itemize}
\end{lemma}

Suppose $\lang\included\lang'$, and $\lang'\setminus\lang$ contains only
constant-symbols.

\begin{lemma}
The inclusion of $\Fm{}(\lang)$ in
$\Fm{}(\lang')$ induces an embedding of $\Fm{}(\lang)/\!\!\sim$ in
$\Fm{}(\lang')/\!\!\sim$.
\end{lemma}

For any consistent set $T$ of formulas of $\lang'$, there is a relation
on constant-symbols given by
\begin{equation*}
  c\sim d\iff T\vdash c=d.
\end{equation*}
(This is distinct from the relation $\sim$ on \emph{formulas}.)

\begin{lemma}
The relation $\sim$ on constant-symbols is an equivalence-relation.
\end{lemma}

Suppose in particular that $\lang$ has a constant-symbol $c_{\phi}$ for
each unary formula $\phi$, and suppose $\Gamma$ is a consistent set of
formulas of $\lang$.

\begin{lemma}
There is a consistent set $T$ of formulas of $\lang'$ such that:
\begin{itemize}
  \item
  $\Gamma\included T$;
  \item
  $T\vdash\exists x_0\,\phi\to\phi(c_{\phi})$ for
each unary formula $\phi$;
  \item
  $T$ is \emph{maximally} consistent:
  the image of $\langle T\rangle$ in $\Fm{}(\lang')/\!\!\sim$ is an
  ultrafilter.
  \end{itemize}
\end{lemma}

\begin{lemma}
Suppose $T$ is a maximally consistent set of formulas of $\lang'$ such
that $T\vdash\exists x_0\,\phi\to\phi(c_{\phi})$ for each unary formula
$\phi$.  Then:
\begin{itemize}
\item
  There is a unique model $\str M$ of $T$ whose universe $M$ comprises the
$\sim$-classes of the constant-symbols $c_{\phi}$, and such that
\begin{itemize}
  \item
  $c^{\str M}=c/\!\!\sim$ for each constant-symbol $c$,
  \item
  $f^{\str M}(\tuple c/\!\!\sim)=d/\!\!\sim$ if $T\vdash fc_0\dots
  c_{n-1}=d$, for all function-symbols $f$, and
  \item
  $(\tuple c/\!\!\sim)\in R^{\str M}$ if $T\vdash Rc_0\dots
  c_{n-1}$, for all relation-symbols $R$.
\end{itemize}
  \item
  If $\str M$ is this model, then
  $\phi^{\str M}=\{(\tuple c/\!\!\sim):T\vdash\phi(\tuple c)\}$ for all
  formulas $\phi$.
\end{itemize}
\end{lemma}

\end{document}