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

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

%\theoremstyle{definition}
\newtheorem{problem}{Problem}
\setcounter{problem}{4}
\newtheorem*{lemma}{Lemma}

\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{\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]{\textrm{Fm}^{#1}}
\newcommand{\Fmo}[1]{\textrm{Fm}^{#1}_0}
\newcommand{\Fmp}[1]{\textrm{Fm}_{\textrm{p}}^{#1}}
\newcommand{\Tm}[1]{\textrm{Tm}^{#1}}

\newcommand{\comp}{^\mathrm{c}}  % set-theoretic complement

\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



%  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{Math 736, Model-Theory, 2001, fall.  Here are some
additional notes on terms and formulas; Problems 5 and 6 constitute
Homework II.  Revised, 25 October 2001.}

Fix a signature $\lang$.  Let $c$, $f$ and $R$ range respectively over
the constant-, function- and relation-symbols of $\lang$; let $\str M$
range over $\Mod(\lang)$; let $i$, $k$, $m$, and $n$ range over $\omega$.

For each $n$, we want to define a set $\Tm{n}(\lang)$, of \defn{$n$-ary
terms of $\lang$}.  Each $t$ in $\Tm{n}(\lang)$ should have, for each
$\str M$, an interpretation $t^{\str M}$, which is an $n$-ary function on
$M$. We want the terms and their interpretations to satisfy the following
requirements.
\begin{enumerate}\setcounter{enumi}{-1}
  \item
  For each $c$, there is $t$ in $\Tm{0}(\lang)$ such that $t^{\str M}$ is
  $c^{\str M}$ for each $\str M$.
  \item
  If $f$ is $n$-ary, then there is $t$ in $\Tm{n}(\lang)$ such that
  $t^{\str M}$ is $f^{\str M}$ for each $\str M$.
  \item
  There is $t$ in $\Tm{1}(\lang)$ such that $t^{\str M}$ is $\id_M$ for
  each $\str M$.
  \item
  For every function $\sigma:m\to n$, and for every $u$ in
  $\Tm{m}(\lang)$,
  there is $t$ in $\Tm{n}(\lang)$ such that $t^{\str M}$ is
  \begin{equation*}
    \tuple a\mapsto u^{\str M}(a_{\sigma(0)},\dots,a_{\sigma(m-1)}):M^n\to M
  \end{equation*}
  for each $\str M$.
  \item
  For each $u$ in $\Tm{m}(\lang)$, and for any $t_0$, \dots, $t_{m-1}$ in
  $\Tm{n}(\lang)$, there is $t$ in $\Tm{n}(\lang)$ such that $t^{\str M}$
  is $u^{\str M}\circ(t_0^{\str M},\dots,t_{m-1}^{\str M})$ for each $\str M$.
  \item
  No terms $t$ exist whose interpretations $t^{\str M}$ are not required
  by the preceding clauses.
\end{enumerate}
Then the sets $\Tm{n}(\lang)$ of $n$-ary terms $t$, and their
interpretations $t^{\str M}$, can be defined as follows.
\begin{enumerate}\renewcommand{\labelenumi}{(\alph{enumi})}
  \item
  $\Tm{0}(\lang)$ contains the symbols $c$ (each a string of length 1).
  \item
  $\Tm{i+1}(\lang)$ contains the symbol $x_i$ (a string of length 1).
  \item
  $\Tm{n+1}(\lang)$ includes $\Tm{n}(\lang)$.
  \item
  If $f$ is $m$-ary, and $u_0$, \dots, $u_{m-1}$ are in $\Tm{n}(\lang)$,
  then $\Tm{n}(\lang)$ contains $fu_0\cdots u_{m-1}$ (the concatenation
  of the strings $f$, $u_0$, \dots, $u_{m-1}$).
  \item
  $\Tm{n}(\lang)$ contains no other strings than those required by the
  preceding clauses, and if $t\in\Tm{n}(\lang)$, then for every $\str M$,
  the interpretation $t^{\str M}$ is:
\begin{itemize}
  \item
  $\tuple a\mapsto c^{\str M}$, if $t$ is $c$;
  \item
  $\tuple a\mapsto a_i$, if $t$ is $x_i$;
  \item
  $f^{\str M}\circ(u_0^{\str M},\dots, u_{m-1}^{\str M})$, if $t$ is $fu_0\cdots
  u_{m-1}$ (where $f$ is $m$-ary and the $u_i$ are in $\Tm{n}(\lang)$).
\end{itemize}
\end{enumerate}
The definition of the interpretations of terms depends on how terms can
be analyzed; so the validity of the definition must be checked.  To do
this, one can use the following.

\begin{lemma}
A proper initial segment of a term is not a term; that is, if a string
$\alpha_0\alpha_1\cdots\alpha_n$ of symbols $\alpha_i$ is a term, and
$m<n$, then $\alpha_0\alpha_1\dots\alpha_m$ is not a term.
\end{lemma}

\begin{proof}
The claim is trivially true for terms of length 1.  Suppose it is false
for a term $t$ of length $k+1$.  Then $t$ is $ft_0\cdots t_{n-1}$ for
some terms $t_i$, but $t$ has a proper initial segment of the form
$fu_0\cdots u_{m-1}$, where the $u_i$ are terms.  Then there is some
least $i$ such that $t_i$ is not $u_i$; but then also one of these is an
initial segment of the other.  Thus the claim fails for a term of length
$k$ or less---if it fails for a term of length $k+1$.  By induction, the
claim holds for terms of all lengths.
\end{proof}

\begin{lemma}[unique readability of terms]
Every term is uniquely of the form $c$, $x_i$ or $ft_0\cdots t_{n-1}$,
where the $t_i$ are terms.
\end{lemma}

\begin{proof}
If the analysis of a term as $ft_0\cdots t_{n-1}$ is not unique, then (as
in the proof of the previous lemma) one of the $t_i$ can be assumed to be
a proper initial segment of another term.
\end{proof}

Finally, by induction on the length of terms, every $n$-ary term is also
$n+1$-ary and has an interpretation as such.  So terms and their
interpretations are well-defined. Now we can check that the several
numbered requirements of terms are met:
\begin{enumerate}\setcounter{enumi}{-1}
  \item
  Let $t$ be $c$.
  \item
  Let $t$ be $fx_0\cdots x_{n-1}$.
  \item
  Let $t$ be $x_0$.
  \item
  The required term $t$ can be denoted
  $u(x_{\sigma(0)},\dots,x_{\sigma(m-1)})$, and can be defined inductively:
  \begin{itemize}
    \item
  If $u$ is $c$, then $t$ is $c$.
    \item
  If $u$ is $x_i$, then $t$ is $x_{\sigma(i)}$.
    \item
  If $u$ is $fu_0\cdots u_{k-1}$, then $t$ is $ft_0\cdots t_{k-1}$, where
  $t_i$ is\\
  $u_i(x_{\sigma(0)},\dots,x_{\sigma(m-1)})$.
  \end{itemize}
  \item
  The required term $t$ can be denoted
  $u(t_0,\dots,t_{m-1})$, and can be defined inductively:
  \begin{itemize}
    \item
  If $u$ is $c$, then $t$ is $c$.
    \item
  If $u$ is $x_i$, then $t$ is $t_i$.
    \item
  If $u$ is $fu_0\cdots u_{k-1}$, then $t$ is $fv_0\cdots v_{k-1}$, where
  $v_i$ is\\
  $u_i(t_0,\dots,t_{m-1})$.
  \end{itemize}
  \item
  Every interpretation $t^{\str M}$ satisfies one of the requirements:
  \begin{enumerate}\renewcommand{\labelenumii}{(\alph{enumii})}
    \item
    The nullary term $c$ is a term $t$ such that $t^{\str M}=c^{\str M}$.
  \item
  Let $u$ be the unary term $x_0$ (whose interpretation in $\str M$, or
  $\id_M$, is required); let $\sigma$ be the map from $1$ to $i+1$ such
  that $\sigma(0)=i$; then $x_i$ is an $i+1$-ary term $t$ such that
  $t^{\str M}$ is $\tuple a\mapsto u^{\str M}(a_{\sigma(0)})$.
  \item
  if an $n$-ary term $t$ has a required interpretation, then the
  interpretation of $t$ as an $n+1$-ary term is also required, since this
  interpretation is $\tuple a\mapsto t^{\str
  M}(a_{\sigma(0)},\dots,a_{\sigma(n-1)})$, where $\sigma$ is the
  inclusion of $n$ in $n+1$.
  \item
  Let $u$ be $fx_0\cdots x_{m-1}$; then its interpretation in $\str M$, namely
  $f^{\str M}$, is required.  Suppose the interpretations of  the terms $t_i$ are
  required; then so is the interpretation of $ft_0\cdots t_{m-1}$, since this
  interpretation is $u^{\str M}\circ(t_0^{\str M},\dots,t_{m-1}^{\str
  M})$.
\end{enumerate}
\end{enumerate}

Now we can move on to \emph{formulas}.  For each $n$, we want to define a
set $\Fm{n}(\lang)$, comprising the
\defn{$n$-ary formulas of $\lang$}.  Each $\phi$ in $\Fm{n}(\lang)$ should
have, for each $\str M$, an interpretation $\phi^{\str M}$, which is an
$n$-ary relation on $M$.  We want the formulas and their interpretations
to satisfy the following requirements.
\begin{enumerate}\setcounter{enumi}{-1}
  \item
  There is $\phi$ in $\Fm{2}(\lang)$ such that $\phi^{\str M}$ is
  $\{(a,b)\in M^2:a=b\}$ for each $\str M$.
  \item
  If $R$ is $n$-ary, then there is $\phi$ in $\Fm{n}(\lang)$ such that
  $\phi^{\str M}$ is $R^{\str M}$ for each $\str M$.
  \item
  For any $m$-ary term $F$ of the signature of Boolean algebras, and for
  any $\psi_0$, \dots, $\psi_{m-1}$ in $\Fm{n}(\lang)$, there is $\phi$ in
  $\Fm{n}(\lang)$ such that $\phi^{\str M}$ is
  $F^{\pow(M^n)}(\psi_0^{\str M},\dots,\psi_{m-1}^{\str M})$ for each
  $\str M$.
  \item
  For any $t_0$, \dots, $t_{m-1}$ in $\Tm{n}(\lang)$, and for any $\psi$ in
  $\Fm{m}(\lang)$, there is $\phi$ in $\Fm{n}(\lang)$ such that
  $\phi^{\str M}$ is
\begin{equation*}
  \{\tuple a\in M^n:(t_0^{\str M}(\tuple a),\dots,t_{m-1}^{\str M}(\tuple
  a))\in \psi^{\str M}\}
\end{equation*}
for each $\str M$.
  \item
  For any $u_0$, \dots, $u_{n-1}$ in $\Tm{m}(\lang)$, and for any $\psi$ in
  $\Fm{m}(\lang)$, there is $\phi$ in $\Fm{n}(\lang)$ such that
  $\phi^{\str M}$ is
\begin{equation*}
  \{(u_0^{\str M}(\tuple a),\dots,
  u_{n-1}^{\str M}(\tuple a))\in M^n:\tuple a\in \psi^{\str M}\}
\end{equation*}
for each $\str M$.
  \item
  No formulas $\phi$ exist whose interpretations $\phi^{\str M}$ are not
  required by the preceding clauses.
\end{enumerate}

To meet these requirements,  we propose to define the sets
$\Fm{n}(\lang)$ of $n$-ary formulas $\phi$, and their interpretations
$\phi^{\str M}$, as follows.
\begin{enumerate}\renewcommand{\labelenumi}{(\alph{enumi})}
  \item
  $\Fm{n}(\lang)$ contains $(t=u)$ whenever $t$ and $u$ are in
  $\Tm{n}(\lang)$.
  \item
 $\Fm{n}(\lang)$ contains $Rt_0\cdots t_{m-1}$ whenever $R$ is $m$-ary
  and $t_0$, \dots, $t_{m-1}$ are in $\Tm{n}(\lang)$.
  \item
  $\Fm{0}(\lang)$ contains $\bot$ and $\top$; and
  $\Fm{n}(\lang)$ contains $\lnot\psi$ and $(\psi\land\chi)$ and
  $(\psi\lor\chi)$ whenever $\psi,\chi\in\Fm{n}(\lang)$.  (The symbols
  $\bot$ and $\top$ and $\lnot$ and $\land$ and $\lor$ can be supposed distinct from any
  symbols in $\lang$.)
  \item
  $\Fm{n}(\lang)$ contains $\exists x_n\,\psi$ and $\forall x_n\,\psi$ whenever
  $\psi\in\Fm{n+1}(\lang)$.
  \item
  $\Fm{n}(\lang)$ contains no other strings of symbols than those
  required by the preceding clauses, and if $\phi\in\Fm{n}(\lang)$, then
  for every $\str M$ the interpretation $\phi^{\str M}$ is:
\begin{itemize}
  \item
  $\{\tuple a\in M^n:t^{\str M}(\tuple a)=u^{\str M}(\tuple a)\}$, if
  $\phi$ is $(t=u)$;
  \item
  $\{\tuple a\in M^n:(t_0^{\str M}(\tuple a),\dots,t_{m-1}^{\str M}(\tuple a))
  \in R^{\str M}\}$, if $\phi$ is $Rt_0\cdots t_{m-1}$;
  \item
  $\emptyset$, if $\phi$ is $\bot$;
  \item
  $\emptyset\comp$, if $\phi$ is $\top$;
  \item
  $(\psi^{\str M})\comp$, if $\phi$ is $\lnot\psi$;
  \item
  $\psi^{\str M}\cap\chi^{\str M}$, if $\phi$ is $(\psi\land\chi)$;
  \item
  $(\lnot(\lnot\psi\land\lnot\chi))^{\str M}$, if $\phi$ is $(\psi\lor\chi)$;
  \item
  $\{\tuple a\in M^n:(\tuple a,b)\in \psi^{\str M}, \text{ some $b$ in
  }M\}$, if $\phi$ is $\exists x_n\,\psi$;
  \item
  $(\lnot\exists x_n\,\lnot\psi)^{\str M}$, if $\phi$ is $\forall x_n\,\psi$.
\end{itemize}
\end{enumerate}

\begin{problem}
Show that the proposed definition of $\Fm{n}(\lang)$ is valid and meets
the requirements.
\end{problem}

Now let $\Fmo{n}(\lang)$ be the smallest subset of $\Fm{n}(\lang)$ that
contains the formulas $Rt_0\cdots t_{m-1}$ and $(t=u)$ and that contains
$\lnot\psi$ and $(\psi\land\chi)$ and $(\psi\lor\chi)$ when it contains
$\psi$ and $\chi$.  Let $\Fmp{n}(\lang)$ be the smallest subset of
$\Fm{n}(\lang)$ such that:
\begin{itemize}
  \item
  $\Fmo{n}(\lang)\included\Fmp{n}(\lang)$;
  \item
  $\Fmp{n}(\lang)$ contains $\bot$ and $\top$;
  \item
  $\Fmp{n}(\lang)$ contains $\exists x_n\,\psi$ and $\forall x_n\,\psi$
  when $\psi\in\Fmp{n+1}(\lang)$.
\end{itemize}
(The subscript \emph{p} stands for \emph{prenex}, which describes the
elements of $\Fmp{n}(\lang)$.)  Say that $n$-ary formulas $\phi$ and
$\psi$ are
\defn{equivalent} if their interpretations in $\str M$ are the same, for
every $\str M$.

\begin{problem}
Show that for every formula in $\Fm{n}(\lang)$ there is an equivalent
formula in $\Fmp{n}(\lang)$.
\end{problem}

\end{document}