partial-iso.tex

% Part: first-order-logic
% Chapter: model-theory
% Section: partial-iso

\documentclass[../../../include/open-logic-section]{subfiles}

\begin{document}

\olfileid{mod}{bas}{pis}
\section{Partial Isomorphisms}

\begin{defn}
  Given two !!{structure}s $\Struct{M}$ and $\Struct{N}$, a
  \emph{partial isomorphism} from $\Struct{M}$ to $\Struct{N}$ is a
  finite partial function $p$ taking arguments in $\Domain M$ and returning
  values in $\Domain N$, which satisfies the isomorphism conditions from
  \olref[iso]{defn:isomorphism} on its domain:
  \begin{enumerate}
  \item $p$ is !!{injective};
  \item for every !!{constant}~$c$: if $p(\Assign{c}{M})$ is defined,
    then $p(\Assign{c}{M}) = \Assign{c}{N}$;
  \item for every $n$-place !!{predicate} $P$: if $a_1$, \dots, $a_n$
    are in the domain of $p$, then $\langle a_1, \dots, a_n\rangle \in
    \Assign P M$ if and only if $\langle p(a_1), \dots, p(a_n) \rangle
    \in \Assign P N$;
  \item for every $n$-place !!{function} $f$: if $a_1$, \dots, $a_n$
    are in the domain of $p$, then $p(\Assign f M (a_1, \dots,a_n))
    = \Assign f N (p(a_1), \ dots, p(a_n))$.
  \end{enumerate}
  That $p$ is finite means that $\dom{p}$ is finite.
\end{defn}

Notice that the empty function~$\emptyset$ is always a partial
isomorphism between any two !!{structure}s.

\begin{defn}\ollabel{defn:partialisom}
  Two !!{structure}s $\Struct{M}$ and $\Struct{N}$, are
  \emph{partially isomorphic}, written $\Struct{M} \iso[p]
  \Struct{N}$, if and only if there is a non-empty set $I$
  of partial isomorphisms between $\Struct{M}$ and $\Struct{N}$
  satisfying the \emph{back-and-forth} property:
  \begin{enumerate}
  \item (\emph{Forth}) For every $p \in I$ and $a \in \Domain M$
    there is $q \in I$ such that $p \subseteq q$ and $a$ is
    in the domain of $q$;
  \item (\emph{Back}) For every $p \in I$ and $b \in \Domain N$
    there is $q \in I$ such that $p \subseteq q$ and $b$ is
    in the range of $q$.
  \end{enumerate}
\end{defn}

\begin{thm}\ollabel{thm:p-isom1}
  If $\Struct{M} \iso[p] \Struct{N}$ and $\Struct{M}$ and
  $\Struct{N}$ are !!{enumerable}, then $\Struct{M} \iso
  \Struct{N}$.
\end{thm}

\begin{proof}
  Since $\Struct{M}$ and $\Struct{N}$ are !!{enumerable}, let $\Domain{M} =
  \{a_0, a_1, \ldots \}$ and $\Domain{N} = \{b_0, b_1, \ldots \}$. Starting
  with an arbitrary $p_0 \in I$, we define an increasing
  sequence of partial isomorphisms $p_0 \subseteq p_1 \subseteq p_2
  \subseteq \cdots$ as follows:
  \begin{enumerate}
  \item if $n+1$ is odd, say $n = 2r$, then using the Forth property
    find a $p_{n+1} \in I$ such that $p_n \subseteq p_{n+1}$
    and $a_r$ is in the domain of $p_{n+1}$;
  \item if $n+1$ is even, say $n+1 =2r$, then using the Back property
    find a $p_{n+1} \in I$ such that $p_n \subseteq p_{n+1}$
    and $b_r$ is in the range of $p_{n+1}$.
  \end{enumerate}
If we now put:
\[
p = \bigcup_{n\ge 0} p_n,
\]
we have that $p$ is a an isomorphism between $\Struct{M}$ and
$\Struct{N}$.
\end{proof}

\begin{prob}
  Show in detail that $p$ as defined in
  \olref[mod][bas][pis]{thm:p-isom1} is in fact an isomorphism.
\end{prob}

\begin{thm}\ollabel{thm:p-isom2}
  Suppose $\Struct{M}$ and $\Struct{N}$ are !!{structure}s for a
  purely relational !!{language} (!!a{language} containing only
  !!{predicate}s, and no !!{function}s or constants). Then if
  $\Struct{M} \iso[p] \Struct{N}$, also $\Struct{M} \elemequiv
  \Struct{N}$.
\end{thm}

\begin{proof}
  By induction on !!{formula}s, one shows that if $a_1$, \dots, $a_n$ and
  $b_1$, \dots, $b_n$ are such that there is a partial isomorphism $p$
  mapping each $a_i$ to $b_i$ and $s_1(x_i) =a_i$ and $s_2(x_i) =b_i$
  (for $i =1$, \dots,~$n$), then $\Sat{M}{!A}[s_1]$ if
  and only if $\Sat{N}{!A}[s_2]$. The case for $n=0$
  gives $\Struct{M} \elemequiv \Struct{N}$.
\end{proof}

\begin{rem}
If !!{function}s are present, the previous result is still true, but
one needs to consider the isomorphism induced by $p$ between the
sub!!{structure} of $\Struct{M}$ generated by $a_1$, \dots, $a_n$ and the
sub!!{structure} of $\Struct{N}$ generated by $b_1$, \dots, $b_n$.
\end{rem}

The previous result can be ``broken down'' into stages by establishing a
connection between the number of nested quantifiers in !!a{formula} and
how many times the relevant partial isomorphisms can be extended.

\begin{defn}
  For any !!{formula}~$!A$, the \emph{quantifier rank} of $!A$, denoted
  by $\QuantRank{!A} \in \Nat$, is recursively defined as
  the highest number of nested quantifiers in $!A$.  Two
  !!{structure}s $\Struct{M}$ and $\Struct{N}$ are \emph{$n$-equivalent},
  written $\Struct{M} \elemequiv[n] \Struct{N}$, if they agree on all
  sentences of quantifier rank less than or equal to~$n$.
\end{defn}

\begin{prop}\ollabel{prop:qr-finite}
  Let $\Lang{L}$ be a finite purely relational !!{language}, i.e., a
  !!{language} containing finitely many !!{predicate}s and !!{constant}s,
  and no !!{function}s. Then for each $n \in \Nat$ there are
  only finitely many first-order !!{sentence}s in the !!{language}
  $\Lang{L}$ that have quantifier rank no greater than $n$, up to
  logical equivalence.
\end{prop}

\begin{proof}
  By induction on $n$.
\end{proof}

\begin{defn}
  Given !!a{structure}~$\Struct{M}$, let $\Domain M^{<\omega}$ be the set of
  all finite sequences over $\Domain{M}$. We use $\mathbf{a},
  \mathbf{b}, \mathbf{c}, \ldots$ to range over finite sequences of
  elements. If $\mathbf{a} \in \Domain{M}^{<\omega}$ and $a \in \Domain{M}$, then
  $\mathbf{a}a$ represents the \emph{concatenation} of $\mathbf{a}$ with $a$.
\end{defn}

\begin{defn}
  Given !!{structure}s $\Struct{M}$ and $\Struct{N}$, we define
  relations $I_n \subseteq \Domain M^{<\omega} \times \Domain N^{<\omega}$ between
  sequences of equal length, by recursion on $n$ as follows:
   \begin{enumerate}
   \item $I_0(\mathbf{a},\mathbf{b})$ if and only if $\mathbf{a}$ and
     $\mathbf{b}$ satisfy the same atomic !!{formula}s in  $\Struct{M}$
     and  $\Struct{N}$; i.e., if $s_1(x_i) = a_i$ and $s_2(x_i) =
     b_i$ and $!A$ is atomic with all !!{variable}s among
     $x_1$, \dots,~$x_n$, then $\Sat{M}{!A}[s_1]$ if and
     only if~$\Sat{N}{!A}[s_2]$.
   \item $I_{n+1} (\mathbf{a},\mathbf{b})$ if and only if for every
     $a\in \Domain M$ there is a $b\in \Domain N$ such that $I_n
     (\mathbf{a}a,\mathbf{b}b)$, and vice-versa.
   \end{enumerate}
\end{defn}


\begin{defn}
  Write $\Struct{M} \approx_n \Struct{N}$ if
  $I_n(\emptyseq,\emptyseq)$ holds of $\Struct{M}$ and
  $\Struct{N}$ (where $\emptyseq$ is the empty sequence).
\end{defn}

\begin{thm}\ollabel{thm:b-n-f}
  Let $\Lang{L}$ be a purely relational !!{language}. Then $I_n
  (\mathbf{a},\mathbf{b})$ implies that for every $!A$ such that
  $\QuantRank{!A} \le n$, we have $\Sat{M}{!A}[\mathbf{a}]$ if and
  only if $\Sat{N}{!A}[\mathbf{b}]$ (where again $\mathbf{a}$
  satisfies $!A$ if any $s$ such that $s(x_i) = a_i$ satisfies
  $!A$). Moreover, if $\Lang{L}$ is finite, the converse also holds.
\end{thm}

\begin{proof}
  The proof that $I_n(\mathbf{a},\mathbf{b})$ implies that
  $\mathbf{a}$ and $\mathbf{b}$ satisfy the same !!{formula}s of
  quantifier rank no greater than $n$ is by an easy induction on
  $!A$. For the converse we proceed by induction on $n$, using
  \olref{prop:qr-finite}, which ensures that for each $n$
  there are at most finitely many non-equivalent !!{formula}s of that
  quantifier rank.

  For $n=0$ the hypothesis that $\mathbf{a}$ and $\mathbf{b}$ satisfy
  the same quantifier-free !!{formula}s gives that they satisfy the same
  atomic ones, so that $I_0(\mathbf{a},\mathbf{b})$.

  For the $n+1$ case, suppose that $\mathbf{a}$ and $\mathbf{b}$
  satisfy the same !!{formula}s of quantifier rank no greater than
  $n+1$; in order to show that $I_{n+1}(\mathbf{a},\mathbf{b})$
  suffices to show that for each $a \in \Domain M$ there is a $b \in
  \Domain N$ such that $I_n(\mathbf{a}a,\mathbf{b}b)$, and by the
  inductive hypothesis again suffices to show that for each $a \in
  \Domain M$ there is a $b \in \Domain N$ such that $\mathbf{a}a$ and
  $\mathbf{b}b$ satisfy the same !!{formula}s of quantifier rank no
  greater than $n$.

  Given $a \in \Domain M$, let $!T^a_n$ be set of !!{formula}s
  $!B(x,\mathbf{y})$ of rank no greater than $n$ satisfied by
  $\mathbf{a}a$ in $\Struct{M}$; $!T^a_n$ is finite, so we can
  assume it is a single first-order !!{formula}. It follows that
  $\mathbf{a}$ satisfies $\lexists[x][!T^a_n(x,\mathbf{y})]$, which
  has quantifier rank no greater than $n+1$. By hypothesis
  $\mathbf{b}$ satisfies the same !!{formula} in $\Struct{N}$, so that
  there is a $b \in \Domain N$ such that $\mathbf{b}b$ satisfies
  $!T^a_n$; in particular, $\mathbf{b}b$ satisfies the same
  !!{formula}s of quantifier rank no greater than $n$ as
  $\mathbf{a}a$. Similarly one shows that for every $b \in \Domain N$
  there is $a\in \Domain M$ such that $\mathbf{a}a$ and $\mathbf{b}b$
  satisfy the same !!{formula}s of quantifier rank no greater than $n$,
  which completes the proof.
\end{proof}

\begin{cor}\ollabel{cor:b-n-f}
  If $\Struct{M}$ and $\Struct{N}$ are purely relational !!{structure}s
  in a finite !!{language}, then $\Struct{M} \approx_n\Struct{N}$ if and
  only if $\Struct{M} \elemequiv[n] \Struct{N}$. In particular
  $\Struct{M} \elemequiv \Struct{N}$ if and only if for each $n$,
  $\Struct{M} \approx_n \Struct{N}$ .
\end{cor}

\end{document}