Model theory

Basics of Model Theory

content/model-theory/basics/basics.tex

% Part: model-theory% Chapter: basics\documentclass[../../../include/open-logic-chapter]{subfiles}\begin{document}\olchapter{mod}{bas}{Basics of Model Theory}\olimport{reducts-and-expansions}\olimport{substructures}\olimport{overspill}\olimport{isomorphism}\olimport{theory-of-m}\olimport{partial-iso}\olimport{dlo}%\olimport{nonstandard-arithmetic}\OLEndChapterHook\end{document}

content/model-theory/basics/reducts-and-expansions.tex

% Part: first-order-logic% Chapter: model-theory% Section: reducts-and-expansions\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{mod}{bas}{red}\section{Reducts and Expansions}Often it is useful or necessary to compare languages which havesymbols in common, as well as !!{structure}s for these languages.  Themost common case is when all the symbols in !!a{language}~$\Lang{L}$are also part of !!a{language}~$\Lang{L'}$, i.e., $\Lang{L} \subseteq\Lang{L'}$. An $\Lang{L}$-!!{structure}~$\Struct{M}$ can then alwaysbe expanded to an $\Lang{L'}$-!!{structure} by adding interpretationsof the additional symbols while leaving the interpretations of thecommon symbols the same.  On the other hand, from an$\Lang{L'}$-structure~$\Struct{M'}$ we can obtain an$\Lang{L}$-structure simply by ``forgetting'' the interpretations ofthe symbols that do not occur in~$\Lang{L}$.\begin{defn}\ollabel{defn:reduct}Suppose $\Lang L \subseteq \Lang L'$, $\Struct M$ is an$\Lang L$-!!{structure} and $\Struct M'$ is an $\Lang L'$-!!{structure}.$\Struct M$ is the \emph{reduct} of $\Struct M'$ to $\Lang L$, and$\Struct M'$ is an \emph{expansion} of $\Struct M$ to $\Lang L'$ iff\begin{enumerate}\item $\Domain{M} = \Domain{M'}$\item For every !!{constant}~$c \in \Lang L$, $\Assign{c}{M} =  \Assign{c}{M'}$.\item For every !!{function}~$f \in \Lang L$, $\Assign{f}{M} =  \Assign{f}{M'}$.\item For every !!{predicate}~$P \in \Lang L$, $\Assign{P}{M} =  \Assign{P}{M'}$.\end{enumerate}\end{defn}\begin{prop}\ollabel{prop:reduct}If an $\Lang{L}$-!!{structure}~$\Struct{M}$ is a reduct of an$\Lang{L'}$-!!{structure}~$\Struct{M'}$, then for all$\Lang{L}$-!!{sentence}s~$!A$,\[\Sat{M}{!A} \text{ iff } \Sat{M'}{!A}.\]\end{prop}\begin{proof}  Exercise.\end{proof}\begin{prob}Prove \olref[mod][bas][red]{prop:reduct}.\end{prob}\begin{defn}When we have an $\Lang{L}$-structure $\Struct{M}$, and $\Lang{L'} =\Lang{L} \cup \{P\}$ is the expansion of $\Lang{L}$ obtained by addinga single $n$-place !!{predicate}~$P$, and $R \subseteq \Domain{M}^n$is an $n$-place relation, then we write $\Expan{M}{R}$ for theexpansion~$\Struct{M'}$ of~$\Struct{M}$ with $\Assign{P}{M'} = R$.\end{defn}\end{document}

content/model-theory/basics/substructures.tex

% Part: first-order-logic% Chapter: model-theory% Section: substructures\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{mod}{bas}{sub}\olsection{Sub\printtoken{p}{structure}}The !!{domain} of !!a{structure}~$\Struct{M}$ may be a subset ofanother~$\Struct{M'}$.  But we should obviously only consider$\Struct{M}$ a ``part'' of $\Struct{M'}$ if not only $\Domain{M}\subseteq \Domain{M'}$, but $\Struct{M}$ and $\Struct{M'}$ ``agree''in how they interpret the symbols of the language at least on theshared part~$\Domain{M}$.\begin{defn}\ollabel{defn:substructure}Given !!{structure}s $\Struct M$ and $\Struct M'$ for the samelanguage~$\Lang L$, we say that $\Struct M$ is a \emph{sub!!{structure}}of $\Struct M'$, and $\Struct M'$ an \emph{extension} of $\Struct M$,written $\Struct M \substruct \Struct M'$, iff\begin{enumerate}\item $\Domain{M} \subseteq \Domain{M'}$,\item For each constant $c \in \Lang L$, $\Assign{c}{M} =    \Assign{c}{M'}$;\item For each $n$-place !!{function} $f \in \Lang L$  $\Assign{f}{M}(a_1, \dots, a_n) = \Assign{f}{M'}(a_1, \dots, a_n)$  for all $a_1$, \dots, $a_n \in \Domain{M}$.\item For each $n$-place !!{predicate} $R \in \Lang L$, $\langle  a_1, \dots, a_n\rangle \in \Assign{R}{M}$ iff $\langle a_1, \dots,  a_n\rangle \in \Assign{R}{M'}$ for all $a_1$, \dots, $a_n \in  \Domain{M}$.\end{enumerate}\end{defn}\begin{rem}\ollabel{rem:substructure}If the language contains no constant or !!{function}s, then any $N\subseteq \Domain{M}$ determines a sub!!{structure}~$\Struct{N}$ of$\Struct M$ with !!{domain}~$\Domain{N} = N$ by putting $\Assign{R}{N} =\Assign{R}{M} \cap N^n$.\end{rem}% prove something about this? Examples?\end{document}

content/model-theory/basics/overspill.tex

% Part: first-order-logic% Chapter: model-theory% Section: overspill\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{mod}{bas}{ove}\olsection{Overspill}\begin{thm}\ollabel{overspill} If a set $\Gamma$ of sentences has arbitrarilylarge finite models, then it has an infinite model.\end{thm}\begin{proof}Expand the language of $\Gamma$ by adding countably many new constants$c_0$, $c_1$, \dots and consider the set $\Gamma \cup \{c_i \neq c_j :i \neq j\}$. To say that $\Gamma$ has arbitrarily large finite modelsmeans that for every $m >0$ there is $n\ge m$ such that $\Gamma$ has amodel of cardinality~$n$. This implies that $\Gamma \cup \{c_i \neqc_j : i \neq j\}$ is finitely satisfiable. By compactness, $\Gamma\cup \{c_i \neq c_j : i \neq j\}$ has a model $\Struct M$ whose domainmust be infinite, since it satisfies all inequalities $c_i \neq c_j$.\end{proof}\begin{prop}\ollabel{inf-not-fo} There is no sentence $!A$ of any first-order language that is true in!!a{structure}~$\Struct M$ if and only if the domain $\Domain{M}$ ofthe !!{structure} is infinite.\end{prop}\begin{proof}If there were such a $!A$, its negation $\lnot !A$ would be true inall and only the finite !!{structure}s, and it would therefore havearbitrarily large finite models but it would lack an infinite model,contradicting \olref{overspill}.\end{proof}\end{document}

content/model-theory/basics/isomorphism.tex

% Part: first-order-logic% Chapter: model-theory% Section: isomorphism\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{mod}{bas}{iso}\olsection{Isomorphic Structures}First-order !!{structure}s can be alike in one of two ways. One way inwhich they can be alike is that they make the same !!{sentence}strue. We call such !!{structure}s \emph{elementarily equivalent}. Butstructures can be very different and still make the same !!{sentence}strue---for instance, one can be !!{enumerable} and the other not.This is because there are lots of features of !!a{structure} thatcannot be expressed in first-order languages, either because thelanguage is not rich enough, or because of fundamental limitations offirst-order logic such as the L\"owenheim--Skolem theorem. So another,stricter, aspect in which !!{structure}s can be alike is if they arefundamentally the same, in the sense that they only differ in theobjects that make them up, but not in their structural features. A wayof making this precise is by the notion of an \emph{isomorphism}.\begin{defn}\ollabel{defn:elem-equiv} Given two !!{structure}s $\Struct{M}$ and $\Struct M'$ for the same!!{language}~$\Lang{L}$, we say that $\Struct{M}$ is \emph{elementarily  equivalent to} $\Struct M'$, written $\Struct{M} \equiv \Struct M'$,if and only if for every !!{sentence}~$!A$ of~$\Lang{L}$,$\Sat{M}{!A}$ iff $\Sat{M'}{!A}$.\end{defn}\begin{defn}\ollabel{defn:isomorphism} Given two !!{structure}s $\Struct{M}$ and$\Struct M'$ for the same !!{language}~$\Lang L$, we say that$\Struct{M}$ is \emph{isomorphic to}~$\Struct M'$, written $\Struct{M}\simeq \Struct M'$, if and only if there is a function $h \colon\Domain{M} \to \Domain{M'}$ such that:\begin{enumerate}\item $h$ is !!{injective}: if $h(x) =  h(y)$ then $x = y$; \item $h$ is !!{surjective}: for every $y \in \Domain{M'}$ there  is $x \in \Domain{M}$ such that $h(x) = y$;\item \ollabel{defn:iso-const}for every !!{constant} $c$:  $h(\Assign{c}{M}) = \Assign{c}{M'}$;\item \ollabel{defn:iso-pred}for every $n$-place !!{predicate}~$P$:  \[  \tuple{a_1, \dots, a_n}\in \Assign{P}{M} \quad\text{iff}\quad  \tuple{h(a_1), \dots, h(a_n)} \in \Assign{P}{M'};  \]\item \ollabel{defn:iso-func}for every $n$-place !!{function} $f$:  \[  h(\Assign{f}{M}(a_1, \dots, a_n)) =  \Assign{f}{M'}(h(a_1), \dots, h(a_n)).  \]\end{enumerate}\end{defn}\begin{thm}\ollabel{thm:isom}If $\Struct{M} \iso \Struct M'$ then $\Struct{M} \elemequiv\Struct{M'}$.\end{thm}\begin{proof}Let $h$ be an isomorphism of $\Struct{M}$ onto $\Struct M'$. For anyassignment~$s$, $h \circ s$ is the composition of $h$ and $s$, i.e.,the assignment in $\Struct{M'}$ such that $(h \circ s)(x) = h(s(x))$.By induction on $t$ and $!A$ one can prove the stronger claims:\begin{enumerate}  \item[a.] $h(\Value{t}{M}[s]) = \Value{t}{M'}[h\circ s]$.  \item[b.] $\Sat{M}{!A}[s]$ iff $\Sat{M'}{!A}[h \circ s]$.\end{enumerate}The first is proved by induction on the complexity of~$t$.\begin{enumerate}\item If $t \ident c$, then $\Value{c}{M}[s] = \Assign{c}{M}$ and  $\Value{c}{M'}[h \circ s] = \Assign{c}{M'}$. Thus,  $h(\Value{t}{M}[s]) = h(\Assign{c}{M}) = \Assign{c}{M'}$ (by  \olref{defn:iso-const} of \olref{defn:isomorphism}) $=  \Value{t}{M'}[h \circ s]$.\item If $t \ident x$, then $\Value{x}{M}[s] = s(x)$ and  $\Value{x}{M'}[h \circ s] = h(s(x))$. Thus, $h(\Value{x}{M}[s]) =  h(s(x)) = \Value{x}{M'}[h \circ s]$.\item If $t \ident f(t_1, \dots, t_n)$, then  \begin{align*}    \Value{t}{M}[s] & = \Assign{f}{M}(\Value{t_1}{M}[s], \dots, \Value{t_n}{M}[s]) \quad\text{and}\\  \Value{t}{M'}[h \circ s] & = \Assign{f}{M}(\Value{t_1}{M'}[h \circ    s], \dots, \Value{t_n}{M'}[h \circ s]).  \end{align*}  The induction hypothesis is that for each $i$, $h(\Value{t_i}{M}[s])  = \Value{t_i}{M'}[h\circ s]$. So,  \begin{align}    h(\Value{t}{M}[s])     & = h(\Assign{f}{M}(\Value{t_1}{M}[s], \dots, \Value{t_n}{M}[s]) \notag\\    & = \Assign{f}{M'}(h(\Value{t_1}{M}[s]), \dots,    h(\Value{t_n}{M}[s])) \ollabel{iso-1}\\    & = \Assign{f}{M'}(\Value{t_1}{M'}[h \circ s], \dots,    \Value{t_n}{M'}[h \circ s]) \ollabel{iso-2}\\    & = \Value{t}{M'}[h\circ s] \notag  \end{align}  Here, \olref{iso-1} follows by \olref{defn:iso-func} of  \olref{defn:isomorphism} and \olref{iso-2} by induction hypothesis.\end{enumerate}Part (b) is left as an exercise.If $!A$ is a sentence, the assignments~$s$ and $h \circ s$ areirrelevant, and we have $\Sat{M}{!A}$ iff $\Sat{M'}{!A}$.\end{proof}\begin{prob}Carry out the proof of (b) of \olref[mod][bas][iso]{thm:isom} indetail. Make sure to note where each of the five propertiescharacterizing isomorphisms of \olref[mod][bas][iso]{defn:isomorphism}is used.\end{prob}\begin{defn}An \emph{automorphism} of a structure $\Struct{M}$ is an isomorphismof $\Struct{M}$ onto itself.\end{defn}\begin{prob}Show that for any structure $\Struct{M}$, if $X$ is a definable subsetof $\Struct{M}$, and $h$ is an automorphism of $\Struct{M}$, then $X= \Setabs{h(x)}{x \in X}$ (i.e., $X$ is fixed under $h$).\end{prob}\end{document}

content/model-theory/basics/theory-of-m.tex

% Part: first-order-logic% Chapter: model-theory% Section: theory-of-m\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{mod}{bas}{thm}\section{The Theory of a \printtoken{S}{structure}}Every !!{structure}~$\Struct{M}$ makes some !!{sentence}s true, andsome false. The set of all the !!{sentence}s it makes true is calledits \emph{theory}. That set is in fact a theory, since anything itentails must be true in all its models, including~$\Struct{M}$.\begin{defn}  Given !!a{structure}~$\Struct M$, the \emph{theory} of  $\Struct{M}$ is the set $\Theory{M}$ of !!{sentence}s  that are true in $\Struct{M}$, i.e., $\Theory{M} =  \Setabs{!A}{\Sat{M}{!A}}$.\end{defn}We also use the term ``theory'' informally to refer to setsof !!{sentence}s having an intended interpretation, whether deductivelyclosed or not.\begin{prop}For any $\Struct{M}$, $\Theory{M}$ is complete.\end{prop}\begin{proof}For any !!{sentence}~$!A$ either $\Sat{M}{!A}$ or $\Sat{M}{\lnot !A}$,so either $!A \in \Theory{M}$ or $\lnot !A \in \Theory{M}$.\end{proof}\begin{prop}\ollabel{prop:equiv}  If $\Struct{N} \models !A$ for every $!A \in \Theory{M}$, then  $\Struct{M} \elemequiv \Struct{N}$.\end{prop}\begin{proof}Since $\Sat{N}{!A}$ for all $!A \in \Theory{M}$, $\Theory{M} \subseteq\Theory{N}$. If $\Sat{N}{!A}$, then $\Sat/{N}{\lnot !A}$, so $\lnot !A\notin \Theory{M}$. Since $\Theory{M}$ is complete, $!A \in\Theory{M}$. So, $\Theory{N} \subseteq \Theory{M}$, and we have$\Struct{M} \elemequiv \Struct{N}$.\end{proof}\begin{rem}\ollabel{remark:R}  Consider $\Struct{R} = \langle\Real, <\rangle$, the !!{structure}  whose domain is the set $\Real$ of the real numbers, in the !!{language}  comprising only a 2-place !!{predicate} interpreted as the $<$  relation over the reals. Clearly $\Struct{R}$ is !!{nonenumerable};  however, since $\Theory{R}$ is obviously consistent, by the  L\"owenheim--Skolem theorem it has !!a{enumerable} model, say  $\Struct{S}$, and by \olref{prop:equiv}, $\Struct{R}  \equiv \Struct{S}$. Moreover, since $\Struct{R}$ and $\Struct{S}$  are not isomorphic, this shows that the converse of  \olref[iso]{thm:isom} fails in general.\end{rem}\end{document}

content/model-theory/basics/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 partialisomorphism 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, butone needs to consider the isomorphism induced by $p$ between thesub!!{structure} of $\Struct{M}$ generated by $a_1$, \dots, $a_n$ and thesub!!{structure} of $\Struct{N}$ generated by $b_1$, \dots, $b_n$.\end{rem}The previous result can be ``broken down'' into stages by establishing aconnection between the number of nested quantifiers in !!a{formula} andhow 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}

content/model-theory/basics/dlo.tex

% Part: first-order-logic% Chapter: model-theory% Section: partial-iso\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{mod}{bas}{dlo}\section{Dense Linear Orders}\begin{defn}  A \emph{dense linear ordering without endpoints} is !!a{structure}  $\Struct{M}$ for the !!{language} containing a single 2-place  !!{predicate}~$<$ satisfying the following sentences:  \begin{enumerate}  \item $\lforall[x][\lnot x < x]$;  \item $\lforall[x][\lforall[y][\lforall[z][(x < y \lif (y < z \lif x    <z ))]]]$;  \item $\lforall[x][\lforall[y][(x< y \lor \eq[x][y] \lor y < x)]]$;  \item $\lforall[x][\lexists[y][x < y]]$;  \item $\lforall[x][\lexists[y][y < x]]$;  \item $\lforall[x][\lforall[y][(x < y \lif \lexists[z][(x < z \land        z < y))]]]$. \end{enumerate}\end{defn}\begin{thm}\ollabel{thm:cantorQ}  Any two !!{enumerable} dense linear orderings without  endpoints are isomorphic.\end{thm}\begin{proof}  Let $\Struct{M_1}$ and $\Struct{M_2}$ be !!{enumerable} dense linear  orderings without endpoints, with ${<_1} = \Assign{<}{M_1}$ and ${<_2} =  \Assign{<}{M_2}$, and let $\PIso{I}$ be the set of all partial  isomorphisms between them. $\PIso{I}$ is not empty since at least  $\emptyset \in \PIso{I}$. We show that $\PIso{I}$ satisfies the  Back-and-Forth property.  Then $\Struct{M_1} \iso[p] \Struct{M_2}$,  and the theorem follows by \olref[pis]{thm:p-isom1}.  To show $\PIso{I}$ satisfies the Forth property, let $p \in  \PIso{I}$ and let $p(a_i) = b_i$ for $i = 1$, \dots,~$n$, and  without loss of generality suppose $a_1 <_1 a_2 <_1 \cdots <_1  a_n$. Given $a \in \Domain{M_1}$, find $b \in \Domain{M_2}$ as  follows:  \begin{enumerate}  \item if $a <_1 a_1$ let $b \in \Domain{M_2}$ be such that $b <_2    b_1$;  \item if $a_n <_1 a$ let $b \in \Domain{M_2}$ be such that $b_n <_2 b$; \item if $a_i <_1 a <_1 a_{i+1}$ for some $i$, then let $b \in   \Domain{M_2}$ be such that $b_i <_2 b <_2 b_{i+1}$.  \end{enumerate}  It is always possible to find a $b$ with the desired property since  $\Struct{M_2}$ is a dense linear ordering without endpoints. Define  $q = p \cup \{ \langle a, b \rangle \}$ so that $q \in \PIso{I}$ is  the desired extension of $p$. This establishes the Forth  property. The Back property is similar. So $\Struct{M_1} \iso[p]  \Struct{M_2}$; by \olref[pis]{thm:p-isom1}, $\Struct{M_1} \iso  \Struct{M_2}$.\end{proof}\begin{prob}  Complete the proof of \olref[mod][bas][dlo]{thm:cantorQ} by  verifying that $\PIso{I}$ satisfies the Back property.\end{prob}\begin{rem}  Let $\Struct{S}$ be any !!{enumerable} dense linear ordering without  endpoints. Then (by \olref{thm:cantorQ}) $\Struct{S} \iso  \Struct{Q}$, where $\Struct{Q} = (\Rat, <)$ is the !!{enumerable}  dense linear ordering having the set $\Rat$ of the rational numbers  as its domain. Now consider again the !!{structure}~$\Struct{R} =  (\Real, <)$ from \olref[thm]{remark:R}. We saw that there is  !!a{enumerable} !!{structure}~$\Struct{S}$ such that $\Struct{R}  \elemequiv \Struct{S}$. But $\Struct{S}$ is !!a{enumerable} dense  linear ordering without endpoints, and so it is isomorphic (and  hence elementarily equivalent) to the !!{structure}~$\Struct{Q}$. By  transitivity of elementary equivalence, $\Struct{R} \elemequiv  \Struct{Q}$. (We could have shown this directly by establishing  $\Struct{R} \iso[p] \Struct{Q}$ by the same back-and-forth  argument.)\end{rem}\end{document}