\documentclass[%
version=last,%
a5paper,
10pt,%
headings=small,%
bibliography=totoc,%
index=totoc,%
twoside,%
reqno,%
cleardoublepage=empty,%
%open=any,%
%parskip=half,%
%draft=false,%
draft=true,%
%DIV=classic,%
DIV=11,%
headinclude=true,%
pagesize]%{scrreprt}
{scrartcl}

%\usepackage[notref,notcite]{showkeys}
\renewcommand{\theequation}{\fnsymbol{equation}}

\usepackage[headsepline]{scrpage2}
\pagestyle{scrheadings}
\clearscrheadings
\ohead{\pagemark}
\ihead{Lindstr\"om's Theorem}

\usepackage{hfoldsty}
\usepackage[neverdecrease]{paralist}
\usepackage{url}

\usepackage{amsmath,amsthm,amssymb,bm,upgreek,mathrsfs}
\usepackage[all]{xy}
\newcommand{\Forall}[1]{\forall#1\;}
\newcommand{\Exists}[1]{\exists#1\;}
\newcommand{\conc}{\mathbin{\hat{\ }}}
\newcommand{\sig}{\mathscr S}
\newcommand{\str}[1]{\mathfrak{#1}}
\newcommand{\size}[1]{\lvert#1\rvert}
\newcommand{\Mod}[1]{\textbf{Mod}(#1)}
\newcommand{\Moda}[1]{\textbf{Mod}^*(#1)}
\newcommand{\Str}[1][\sig]{\textbf{Str}_{#1}}
\DeclareMathOperator{\sentences}{Sn}
\newcommand{\Sn}[1][\sig]{\sentences_{\sig}}
\newcommand{\Sna}[1][\sig]{\sentences^*_{\sig}}
\DeclareMathOperator{\formulas}{Fm}
\newcommand{\Fm}[1][\sig]{\formulas_{#1}}
\DeclareMathOperator{\freevariables}{fv}
\newcommand{\fv}[1]{\freevariables(#1)}
\DeclareMathOperator{\variables}{v}
\newcommand{\vr}[1]{\variables(#1)}
\DeclareMathOperator{\theory}{Th}
\newcommand{\Th}[1]{\theory(#1)}
\newcommand{\Tha}[1]{\theory^*(#1)}
\renewcommand{\emptyset}{\varnothing}
\renewcommand{\setminus}{\smallsetminus}
\renewcommand{\leq}{\leqslant}
\renewcommand{\geq}{\geqslant}
\renewcommand{\phi}{\varphi}
%\newcommand{\Or}{\;\lor\;}
\newcommand{\Or}{\;\mathrel{\text{\textsc{or}}}\;}
\renewcommand{\models}{\vDash}
\newcommand{\nmodels}{\nvDash}
\newcommand{\included}{\subseteq}
\newcommand{\includes}{\supseteq}
\newcommand{\pincluded}{\subset}
\newcommand{\liff}{\Leftrightarrow}
\newcommand{\lto}{\Rightarrow}

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

\begin{document}

\title{Lindstr\"om's Theorem}
\author{David Pierce}
\date{June 15, 2015}
\publishers{Mimar Sinan Fine Arts University\\
Istanbul\\
\url{http://mat.msgsu.edu.tr/~dpierce/}}
\maketitle

We work out a proof of Lindstr\"om's Theorem,
that in any proper expansion of first-order logic
(meeting certain natural conditions),
either the Compactness Theorem
or the (downward) L\"owenheim--Skolem Theorem is lost.
Our main reference is Chang \&\ Keisler \cite[\S2.5, pp.~127--135]{MR91c:03026};
but Hodges \cite[\S3.3, pp.~102--111]{MR94e:03002} is also useful.
The sections of these notes are as follows.
\begin{compactenum}[\S1]
  \item
establishes some notation.
\item
reviews the basic definitions of model theory,
so that we can be precise about what an \emph{abstract logic} is.
\item
reviews notions that Chang \&\ Keisler introduce \emph{ad hoc,}
but Hodges develops generally,
in terms of \emph{games}
(namely Ehren\-feucht--Fra\"{\i}ss\'e games).
\item
proves Lindstr\"om's Theorem,
in a way that seems simpler than Chang \&\ Keisler's.
\end{compactenum}
The last major editing of these notes was on or before August 11, 2014.
Some mild adjustments were made in June, 2015.

\tableofcontents

\section{Tuples}

If $A$ and $\Omega$ are sets,
then a \textbf{relation from $\Omega$ to $A$}
is a subset of the Cartesian product $\Omega\times A$.
If $R$ is such a relation, and it contains $(b,a)$, we write
\begin{equation*}
  b\mathrel Ra.
\end{equation*}
If for every $b$ in $\Omega$ 
there is exactly one $a$ in $A$ for which this holds, 
then $R$ is a \textbf{function} from $\Omega$ to $A$,
and we use the notation
\begin{equation}\label{eqn:Rb}
  R(b)=a,
\end{equation}
so that $R(b)$ can be used as another name for $a$.
We denote by
\begin{equation*}
  A^{\Omega}
\end{equation*}
the class of all functions from $\Omega$ to $A$.
(We could also let $A$, but not $\Omega$, be a proper class.)
A typical element of $A^{\Omega}$ can be written as
\begin{equation*}
  (a_i\colon i\in\Omega).
\end{equation*}
We let $\upomega$ be the set of von Neumann natural numbers.
If $n\in\upomega$,
then a typical element of $A^n$ can be written in any of three forms:
\begin{align*}
  &(a_k\colon k<n),&&(a_0,\dots,a_{n-1}),&&\bm a.
\end{align*}
Such functions are \textbf{$n$-tuples} of $A$.
There is a unique $0$-tuple, namely $0$, so that
\begin{equation*}
  A^0=1.
\end{equation*}
There is a function, actually a bijection,
\begin{equation}\label{eqn:AnA}
  (\bm a,b)\mapsto(a_0,\dots,a_{n-1},b)
\;\text{ from }\;A^n\times A\;\text{ to }\;A^{n+1}.
\end{equation}
Likewise, if also $m\in\upomega$, then there is a bijection
\begin{equation}\label{eqn:AnAm}
  (\bm a,\bm b)\mapsto(a_0,\dots,a_{n-1},b_0,\dots,b_{m-1})
\;\text{ from }\;A^n\times A^m\;\text{ to }\;A^{n+m}.
\end{equation}
We let
\begin{equation*}
  A^{<\upomega}=\bigcup_{n\in\upomega}A^n.
\end{equation*}
Then, by taking the corresponding unions of the functions 
in \eqref{eqn:AnA} and \eqref{eqn:AnAm}, we have embeddings
\begin{equation}\label{eqn:map}
\left.
  \begin{gathered}
  (\bm a,b)\mapsto(a_0,\dots,b)
\;\text{ from }\;A^{<\upomega}\times A\;\text{ to }\;A^{<\upomega},\\
  (\bm a,\bm b)\mapsto(a_0,\dots,b_0,\dots)
\;\text{ from }\;A^{<\upomega}\times A^{<\upomega}\;\text{ to }\;A^{<\upomega}
\end{gathered}
\right\}
\end{equation}
(which we shall need on page \pageref{map}).
We may also write these embeddings as if they were inclusions.
That is, 
we may consider $(\bm a,b)$ and $(\bm a,\bm b)$ as elements of $A^{<\upomega}$.

\section{Model theory}

\subsection{Structures}

If $n\in\upomega$,
then an \textbf{$n$-ary relation} on a set $A$
is a subset of $A^n$;
an \textbf{$n$-ary operation} on $A$
is a function from $A^n$ to $A$.
Here $n$ is the number of \textbf{arguments} of the relation or operation.
By means of the bijection in \eqref{eqn:AnA},
we may consider $n$-ary operations as $(n+1)$-ary relations,
though we retain the special notation for functions given in \eqref{eqn:Rb}.
Normally we have no use for nullary ($0$-ary) relations,
but an nullary operation on $A$ is identified with an element of $A$.

A \textbf{structure} is a set,
possibly given together with some operations and relations on it.
If the set is $A$, the structure can be denoted by
\begin{equation*}
  \str A,
\end{equation*}
and then $A$ is the \textbf{universe} of $\str A$.
Each of the operations and relations of $\str A$ is assigned a symbol,
and these symbols compose the \textbf{signature} of $\str A$.
Each symbol carries the information 
of whether it denotes an operation or relation, 
along with its number of arguments.
We shall use
\begin{equation*}
\sig
\end{equation*}
to denote an arbitrary signature,
and we shall denote the class of structures having this signature by
\begin{equation*}
  \Str.
\end{equation*}

\subsection{Sentences}

We shall define a set of \emph{first order sentences} in the signature $\sig$.
In any such sentence may occur 
\textbf{individual variables} from the list $(v_0,v_1,v_2,\dots)$.
We use expressions from the list $(x_0,x_1,x_2,\dots)$,
as well as $x$, $y$, $z$, and $w$,
to stand for individual variables.
An \textbf{unnested atomic formula} of $\sig$
is an expression of one of the forms
\begin{align*}
              x_0&=x_1,          &  
                 &Rx_0\cdots x_n,&
Fx_0\cdots x_{n-1}&=x_n,
\end{align*}
where $R$ is an $(n+1)$-ary relation symbol of $\sig$
and $F$ is an $n$-ary operation symbol of $\sig$.
We obtain arbitrary \textbf{atomic formulas}
by closing under the operation
of replacing a variable by an expression 
like $Fx_0\cdots x_{n-1}$.
Alternatively,
we first define a \textbf{term} to be either a variable
or an expression
\begin{equation*}
  Ft_0\cdots t_{n-1},
\end{equation*}
where the $t_k$ are now terms;
then an atomic formula is an expression
\begin{align*}
              t_0&=t_1,          &  
                 &Rt_0\cdots t_n,
\end{align*}
where the $t_k$ are terms.
Then we obtain the set
\begin{equation*}
  \Fm
\end{equation*}
of all \textbf{first order formulas} of $\sig$
by closing the set of atomic formulas 
under the operations denoted by $\lnot$, $\lor$, and $\exists x$:
thus, if $\phi$ and $\psi$ are formulas,
then so are the expressions denoted by
\begin{align*}
  &\lnot\phi,&&(\phi\lor\psi),&&\Exists x\phi;
\end{align*}
these are, respectively,
\begin{compactenum}[1)]
\item 
the \textbf{negation} of $\phi$,
\item
the \textbf{disjunction} of $\phi$ and $\psi$, and 
\item
the \textbf{instantiation} at $x$ of $\phi$.
\end{compactenum}
The set of \textbf{unnested formulas} is obtained
by closing likewise the set of unnested atomic formulas.

Thus the set of formulas of $\sig$ 
(as well as of unnested formulas)
is defined recursively,
and so it is possible to prove by induction
that particular subsets of $\Fm$ are actually the whole set.
An important theorem, often overlooked,
is that functions \emph{on} $\Fm$ can be defined by recursion,
because of the \emph{unique readability} of formulas.
Each formula is the root of a tree whose nodes are all of the subformulas
that occur in the construction of the formula;
\textbf{unique readability} is that this tree is unique.

For example, by unique readability, 
there is a function
\begin{equation*}
 \phi\mapsto\fv{\phi}
\end{equation*}
 assigning to each formula in $\Fm$
its set of \textbf{free variables,}
and this function can be defined recursively:
\begin{compactenum}\setcounter{enumi}{-1}
\item 
The free variables of an atomic formula are the variables that occur in it.
\item
$\fv{\lnot\phi}=\fv{\phi}$.
\item
$\fv{(\phi\lor\psi)}=\fv{\phi}\cup\fv{\psi}$.
\item
$\fv{\Exists x\phi}=\fv{\phi}\setminus\{x\}$.
\end{compactenum}
A \textbf{first order sentence} 
is a first order formula having no free variables.
We shall denote the set of first order sentences of $\sig$ by
\begin{equation*}
\Sn.
\end{equation*}
Thus
$\Sn=\{\phi\in\Fm\colon\fv{\phi}=\emptyset\}$.


\subsection{Truth}

There is a relation of \emph{truth,} denoted by
\begin{equation*}
  \models
\end{equation*}
or more precisely $\models_{\sig}$,
between $\Str$ and $\Sn$.
There are two equivalent ways to define it,
and each one has its inconveniences.

\subsubsection{Definable sets}

One approach to truth is to define more generally a certain function
\begin{equation*}
  (\str A,\phi)\mapsto\phi^{\str A}
\end{equation*}
on $\Str\times\Fm$, where $\phi^{\str A}\included A^{\fv{\phi}}$;
here $\phi^{\str A}$ is the relation on $A$
that is \textbf{defined} by $\phi$ in $\str A$.
Once we have defined this for arbitrary $\phi$,
we can make the definition
\begin{equation*}
  \str A\models\sigma\iff\sigma^{\str A}=1,
\end{equation*}
where $\sigma\in\Sn$.

First we have to note that the same symbol $S$ in $\sig$
denotes different things in different structures;
what it denotes in $\str A$ can be denoted more precisely by
\begin{equation*}
  S^{\str A}.
\end{equation*}
Then $S^{\str A}$ is the \textbf{interpretation} in $\str A$ of $S$.
We proceed.

The interpretation of an operation symbol is an operation.
A term $t$ also has an interpretion $t^{\str A}$, which is an operation.
More precisely, if $\vr t$ is the set of variables occurring in $t$,
then $t^{\str A}$ is a function from $A^{\vr t}$ to $A$.
In particular, if $t$ is just $v_k$,
then an element of $A^{\vr t}$ is just a set $\{(v_k,a)\}$,
whose image under $v_k{}^{\str A}$ is $a$.
Also,
\begin{multline*}
Ft_0\cdots t_{n-1}{}^{\str A}(a_x\colon x\in\vr{Ft_0\cdots t_{n-1}})\\
=F^{\str A}(t_0{}^{\str A}(a_x\colon x\in\vr{t_0}),\dots,
t_{n-1}{}^{\str A}(a_x\colon x\in\vr{t_{n-1}})).
\end{multline*}
Now we can define interpretations of formulas.
\begin{compactenum}\setcounter{enumi}{-1}
\item 
For unnested atomic formulas, we define
\begin{gather*}
  (x_0=x_1)^{\str A}=\{f\in A^{\{x_0,x_1\}}\colon f(x_0)=f(x_1)\},\\
(Rx_0\cdots x_n)^{\str A}
=\{f\in A^{\{x_0,\dots,x_n\}}\colon(f(x_0),\dots,f(x_n))\in R^{\str A}\},
\end{gather*}
and
\begin{multline*}
(Fx_0\cdots x_{n-1}=x_n)^{\str A}\\
=\{f\in A^{\{x_0,\dots,x_n\}}\colon F^{\str A}(f(x_0),\dots,f(x_{n-1}))=f(x_n)\}.
\end{multline*}
For arbitrary formulas,
\begin{multline*}
  (t_0=t_1)^{\str A}=
\{f\in A^{\vr{t_0}\cup\vr{t_1}}\colon\\
t_0{}^{\str A}(f\restriction\vr{t_0})=t_1{}^{\str A}(f\restriction\vr{t_1})\},
\end{multline*}
\begin{multline*}
  (Rt_0\cdots t_n)^{\str A}=
\{f\in A^{\vr{t_0}\cup\dots\cup\vr{t_n}}\colon\\
(t_0{}^{\str A}(f\restriction\vr{t_0}),\dots,
t_n{}^{\str A}(f\restriction\vr{t_n}))\in R^{\str A}\}.
\end{multline*}
\item
For negations:
\begin{equation*}
  (\lnot\phi)^{\str A}=A^{\fv{\phi}}\setminus\phi^{\str A}.
\end{equation*}
\item
For disjunctions,
if $\fv{\phi}=\fv{\psi}$, then
\begin{equation*}
  (\phi\lor\psi)^{\str A}=\phi^{\str A}\cup\psi^{\str A};
\end{equation*}
but in general we have to say
\begin{multline*}
  (\phi\lor\psi)^{\str A}
=\{f\in A^{\fv{\phi}\cup\fv{\psi}}\colon f\restriction\fv{\phi}\in\phi^{\str A}\}\\
\cup
\{f\in A^{\fv{\phi}\cup\fv{\psi}}\colon f\restriction\fv{\psi}\in\psi^{\str A}\}.
\end{multline*}
\item
Finally, for instantiations,
\begin{equation*}
  (\Exists x\phi)^{\str A}=\{f\restriction(\fv{\phi}\setminus\{x\})\colon
f\in\phi^{\str A}\}.
\end{equation*}
\end{compactenum}

\subsubsection{Constants}

Alternatively, if $\str A\in\Str$,
we can create the \emph{expanded} signature $\sig(A)$,
which is $\sig$ together with a new \textbf{constant} (nullary operation symbol)
for each element of $A$.
Then we expand $\str A$ to an element $\str A_A$ of $\Str[\sig(A)]$,
where the constant associated with an element of $A$
is interpreted as that element.
Normally we denote the constant and the element by the same symbol.

A \textbf{closed term} is a term with no variables.
Every closed term of $\sig(A)$ has an obvious interpretation in $\str A$:
\begin{equation*}
  (Ft_0\cdots t_{n-1})^{\str A}=F^{\str A}(t_0{}^{\str A},\dots,t_{n-1}{}^{\str A}).
\end{equation*}
Now we can define truth as follows.
\begin{compactenum}\setcounter{enumi}{-1}
\item 
For atomic sentences we have
\begin{gather*}
  \str A\models t_0=t_1\iff t_0{}^{\str A}=t_1{}^{\str A},\\
\str A\models Rt_0\cdots t_n\iff(t_0{}^{\str A},\dots,t_n{}^{\str A})\in R^{\str A}.
\end{gather*}
\item
For negations,
\begin{equation*}
  \str A\models\lnot\sigma\iff\str A\nmodels\sigma.
\end{equation*}
\item
For disjunctions,
\begin{equation*}
  \str A\models(\sigma\lor\tau)\iff\str A\models\sigma\Or\str A\models\tau.
\end{equation*}
\item
For instantiations, we introduce yet another notation: by
\begin{equation*}
  \phi^x_a
\end{equation*}
we mean the result of replacing each \emph{free occurrence} 
of $x$ in $\phi$ with $a$.
The formal definition is recursive:
\begin{enumerate}
  \item
If $\phi$ is atomic, then $\phi^x_a$ is just $\phi$;
\item
$\lnot\phi^x_a$ is $\lnot\psi$, where $\psi$ is $\phi^x_a$;
\item
$(\phi\lor\psi)^x_a$ is $\phi^x_a\lor\theta$, where $\theta$ is $\psi^x_a$;
\item
$\Exists y\phi^x_a$ is just $\Exists y\phi$, if $x$ is the same variable as $y$;
otherwise it is $\Exists y\psi$, where $\psi$ is $\phi^x_a$.
\end{enumerate}
Now we can define
\begin{equation*}
  \str A\models\Exists x\phi
\iff\text{ for some $a$ in $A$, }\;
\str A\models\phi^x_a.
\end{equation*}
\end{compactenum}
The recursive definition of truth 
relies on a recursive definition of $\Sn[\sig(A)]$
(and then on their unique readability, as before):
starting with atomic \emph{sentences,}
we close under
\begin{compactenum}[1)]
\item 
negation,
\item
disjunction, and
\item
the ``multivalued operations'' $\phi^x_a\mapsto\Exists x\phi$,
that is, for each $a$ in $A$,
the operation that, given a sentence,
finds all of the (finitely numerous) formulas $\phi$ 
such that the sentence is $\phi^x_a$,
and then forms the sentences $\Exists x\phi$.
\end{compactenum}

\subsection{Abstract logic}

The class $\Str$, the set $\Sn$, and the relation $\models$ between them
make up the \textbf{first order logic} of $\sig$.
For an instance of an \textbf{abstract logic} of $\sig$,
we replace $\Sn$ with $\Sna$,
which has the same closure properties as $\Sn$ just mentioned:
$\Sna$ must contain all atomic sentences
and be closed under
\begin{inparaenum}[(1)]
\item 
negation,
\item
disjunction, and
\item
the operations $\phi^x_a\mapsto\Exists x\phi$.
\end{inparaenum}
But $\Sna$ may have some other closure properties as well.
Then the definition of truth must be enlarged
to deal with the new closure properties;
but the existing parts of the definition stand.
We make the following additional requirements:
\begin{compactdesc}
\item[Occurrence:]
In every element $\sigma$ of $\Sna$,
only finitely many symbols of $\sig$ may occur.
\item[Reduction:]
Of the symbols in $\sig$,
the definition of truth of $\sigma$ in $\str A$
involves only those that actually occur in $\sigma$.
\item[Renaming:]
All that matters about these symbols 
is whether they denote relations or operations, 
and how many arguments they take.
\item[Isomorphism:]
Truth must be preserved under isomorphism of structures.
\item[Relativization:]
Sentences can be \emph{relativized}
in the way to be described on page \pageref{relative}.
\end{compactdesc}
As we shall use it,
Relativization will subsume Renaming and Isomorphism.

\subsection{The Galois correspondence}

If $\sigma\in\Sn$, we let
\begin{equation}\label{eqn:Mod}
  \Mod{\sigma}=\{\str A\in\Str\colon\str A\models\sigma\};
\end{equation}
this is the class of \textbf{models} of $\sigma$.
Then
\begin{equation}\label{eqn:cup}
\left.  \begin{gathered}
  \Mod{\sigma\lor\tau}=\Mod{\sigma}\cup\Mod{\tau},\\
\Mod{\Exists xx\neq x}=\emptyset,
  \end{gathered}\quad\right\}
\end{equation}
and so the sets $\Mod{\sigma}$ 
are a basis of closed \emph{classes} of a topology on $\Str$.
We may call this topology the \textbf{first order topology.}
\begin{itemize}
\item 
The \textbf{Compactness Theorem} is that this topology is compact.
\item
The most basic form of the \textbf{L\"owenheim--Skolem Theorem}
is that every sentence with model has a \textbf{countable model}
(that is, a model with a countable universe);
in other words,
every nonempty basic closed set has a countable element.
\end{itemize}
If one is bothered by a topological space that is a proper class,
one can pass to a \emph{Kolmogorov quotient} of $\Str$,
namely
\begin{equation*}
  \{\Th{\str A}\colon\str A\in\Str\}, 
\end{equation*}
where
\begin{equation*}
  \Th{\str A}=\{\sigma\in\Sn\colon\str A\models\sigma\}.
\end{equation*}
However, we do not want to do this,
since we shall be interested in refinements of the first order topology,
as induced by abstract logics.
In any case, let us note that two structures $\str A$ and $\str B$ in $\Str$
are \textbf{elementarily equivalent,}
and we write
\begin{equation*}
  \str A\equiv\str B,
\end{equation*}
if they are indistinguishable in the first order topology, that is,
\begin{equation*}
  \Th{\str A}=\Th{\str B}.
\end{equation*}
Now, if we replace $\Sn$ above with $\Sna$ from an abstract logic of $\sig$,
we can still make the definition \eqref{eqn:Mod} when $\sigma\in\Sna$,
and then \eqref{eqn:cup} still holds
for arbitrary $\sigma$ and $\tau$ in $\Sna$.
Thus passing to $\Sna$ gives us a finer topology on $\Str$
than the first order topology.
However, because of our requirements on abstract logics,
this topology still does not distinguish isomorphic structures.

It is going to be convenient to allow \emph{multi-sorted} structures,
that is, structures (like vector spaces) with more than one universe,
each of these universes being called a \textbf{sort.}
Then variables fall into different sorts,
and there may be functions (like scalar multiplication)
from a product of some of the sorts (possibly with repeated sorts)
to one of them.
We shall need only structures with finitely many sorts,
and in this case,
we can consider the structures as one-sorted,
by means of a dodge:
we replace the sorts with their disjoint union,
and we introduce new relation symbols to distinguish the sorts.
(We shall also have to deal with the fact that,
in the formal definition, 
operations are total functions on a power of the universe.)

Two sentences $\sigma$ and $\tau$ are \textbf{logically equivalent,}
and we may write
\begin{equation*}
  \sigma\sim\tau,
\end{equation*}
if $\Mod{\sigma}=\Mod{\tau}$.

\begin{theorem}
  Every first order sentence is logically equivalent to an unnested sentence.
\end{theorem}

\begin{proof}
First note that
  \begin{gather*}
    t_0=t_1\sim\Exists x(t_0=x\land t_1=x),\\
Rt_0\cdots t_n\sim\exists x_0\cdots\Exists{x_n}
(t_0=x_0\land\dots\land t_n=x_n\land Rx_0\cdots x_n)
  \end{gather*}
(where $(\phi\land\psi)$ is an abbrevation for $\lnot(\lnot\phi\land\lnot\psi)$,
and $(\phi\land\psi\land\theta)$ means $(\phi\land(\psi\land\theta))$,
and so on).
The formulas $t_k=x$ and $t_k=x_k$ may not be unnested.
If they are not, we apply the equivalence
\begin{multline*}
Ft_0\cdots t_{n-1}=y\sim
\exists x_0\cdots\Exists{x_{n-1}}\\
(t_0=x_0\land\dots\land t_n=x_n\land Fx_0\cdots x_{n-1}=y),
\end{multline*}
repeatedly as necessary,
in order to conclude that
every atomic sentence is equivalent to an unnested sentence.
\end{proof}


\section{Local isomorphisms}


An \textbf{$n$-ary} formula
is a formula whose free variables belong to the set $\{v_k\colon k<n\}$.
Thus if $m<n$, then $m$-ary formulas are also $n$-ary.
If $\str A$ is a structure of $\sig$,
and $\phi$ is an $n$-ary formula of $\sig(A)$,
and $\bm a\in A^n$, then the expression denoted by
\begin{equation*}
  \phi(\bm a)
\end{equation*}
is the result of replacing each free occurrence of $v_k$ in $\phi$ with $a_k$,
for each $k$ in $n$.
Suppose also $\str B\in\Str$. 
We denote by
\begin{equation*}
  I_0
\end{equation*}
the relation from $A^{<\upomega}$ to $B^{<\upomega}$
consisting of those pairs $(\bm a,\bm b)$
such that, for some $n$ in $\upomega$,
both $\bm a$ and $\bm b$ are $n$-tuples,
and for all $n$-ary \emph{unnested} formulas $\phi$ of $\sig$,
\begin{equation*}
  \str A\models\phi(\bm a)\iff\str B\models\phi(\bm b).
\end{equation*}
Since there are no unnested sentences, we have
\begin{equation*}
  0\mathrel{I_0}0.
\end{equation*}
For any $k$ in $\upomega$, if $I_k$ has been defined as a subset of $I_0$,
we define $I_{k+1}$ to comprise those $(\bm a,\bm b)$ in $I_0$ such that,
for all $c$ in $A$, for some $d$ in $B$,
and also, for all $d$ in $B$, for some $c$ in $A$,
\begin{equation*}
  (\bm a,c)\mathrel{I_k}(\bm b,d).
\end{equation*}
Finally, let
\begin{equation*}
  I=\bigcap_{k\in\upomega}I_k.
\end{equation*}
If $\bm a\mathrel I\bm b$, then,
for all $c$ in $A$, for some $d$ in $B$,
and also, for all $d$ in $B$, for some $c$ in $A$,
\begin{equation*}
  (\bm a,c)\mathrel I(\bm b,d).
\end{equation*}
If $I\neq0$, then $\str A$ and $\str B$ are said to be
\textbf{locally isomorphic.}

\begin{theorem}\label{thm:iso}
  Countable locally isomorphic structures are isomorphic.
\end{theorem}

\begin{proof}
  If $A=\{a_k\colon k\in\upomega\}$ and $B=\{b_k\colon k\in\upomega\}$,
then by recursion there are $k\mapsto b_k'$ and $k\mapsto a_k'$ from $\upomega$
to $B$ and $A$ respectively such that,
for each $n$ in $\upomega$,
\begin{equation*}
  (a_0,a_0',\dots,a_n,a_n')\mathrel I(b_0',b_0,\dots,b_n',b_n).
\end{equation*}
Then $a_k\mapsto b_k'$ is a well-defined isomorphism from $\str A$ to $\str B$,
whose inverse is $b_k\mapsto a_k'$.
\end{proof}

\begin{theorem}
  Locally isomorphic structures are elementarily equivalent.
\end{theorem}

\begin{proof}
  Suppose $\str A$ and $\str B$ are locally isomorphic.
We shall show that,
for all \emph{unnested} formulas $\phi$ of $\sig$,
\begin{equation}\label{eqn:ih}
  \bm a\mathrel I\bm b\implies
\bigl(\str A\models\phi(\bm a)\iff\str B\models\phi(\bm b)\bigr).
\end{equation}
We use induction on the complexity of formulas.
\begin{asparaenum}
  \item
The claim is true by definition if $\phi$ is unnested atomic.
\item
If \eqref{eqn:ih} holds when $\phi$ is $\psi$,
then it holds when $\phi$ is $\lnot\psi$.
\item
If \eqref{eqn:ih} holds when $\phi$ is $\psi$ or $\theta$,
then it holds when $\phi$ is $\psi\lor\theta$.
\item
Suppose \eqref{eqn:ih} holds when $\phi$ is $\psi$.
Say $\bm a\mathrel I\bm b$.
If $\str A\models(\Exists x\psi)(\bm a)$,
then for some $c$ in $A$, we have $\str A\models\psi^x_c(\bm a)$.
By hypothesis, for some $d$ in $B$, we have $(\bm a,c)\mathrel I(\bm b,d)$,
and then $\str B\models\psi^x_d(\bm b)$, 
so $\str B\models(\Exists x\psi)(\bm b)$.
By symmetry, we are done.\qedhere
\end{asparaenum}
\end{proof}

\section{Refinements of the first order topology}

There is an alternative proof of the last theorem
that does not rely directly on the recursive definition of formulas.
This proof turns out to establish a more general result,
namely the next theorem,
where, given the set $\Sna$ of sentences of an abstract logic of $\sig$,
we define
\begin{equation*}
  \Tha{\str A}=\{\sigma\in\Sna\colon\str A\models\sigma\}.
\end{equation*}


\begin{theorem}\label{thm:LS}
  If $\str A$ and $\str B$ are locally isomorphic,
and a given abstract logic of $\sig$
satisfies the L\"owenheim--Skolem Theorem,
then
\begin{equation*}
  \Tha{\str A}=\Tha{\str B}.
\end{equation*}
\end{theorem}

\begin{proof}
Suppose there is $\sigma$ in $\Sna$
that is true in $\str A$, but not in $\str B$.
We shall obtain a contradiction
to the assumption that $\str A$ and $\str B$ are locally isomorphic.
Let $\sig_0$ consist of the symbols of $\sig$
that actually occur in $\sigma$;
by the Occurrence property, $\sig_0$ is finite.
We can \textbf{reduce} $\str A$ 
to a structure $\str A\restriction\sig_0$ having signature $\sig_0$;
but still, by the Reduction property,
\begin{equation*}
  \str A\models\sigma\iff\str A\restriction\sig_0\models\sigma.
\end{equation*}
So we may assume that $\sig$ is the finite signature $\sig_0$.
We shall form a multi-sorted structure, 
to be denoted by $(\str A,\str B)$,
with a signature $\sig^*$.
There will be a sentence $\tau$ of $\sig^*$ such that
$(\str A,\str B)\models\tau$,
and if $(\str C,\str D)\models\tau$,
then $\str C$ and $\str D$ are locally isomorphic,
and $\sigma$ is true in $\str C$, but not in $\str D$.
By the L\"owenheim--Skolem Theorem,
countable such $\str C$ and $\str D$ exist,
and then they are isomorphic by Theorem \ref{thm:iso},
which is absurd.

The structure $(\str A,\str B)$ will have four sorts,
namely $A$, $A^{<\upomega}$, $B$, and $B^{<\upomega}$.
The relation $I$ from $A^{<\upomega}$ to $B^{<\upomega}$
will be a relation of the structure.
There will also be operations as in \eqref{eqn:map}\label{map} 
on page \pageref{eqn:map},
and likewise for $B$ in place of $A$.
There will be constants for $0$ in $A^{<\upomega}$ and $B^{<\upomega}$ respectively.
Then $\tau$ will have, as conjuncts,
\begin{gather*}
0\mathrel I0,\\
  \Forall{\bm x}\Forall{\bm y}\Forall z\Exists w
(\bm x\mathrel I\bm y\lto(\bm x,z)\mathrel I(\bm y,w)\bigr),\\
  \Forall{\bm x}\Forall{\bm y}\Forall w\Exists z
(\bm x\mathrel I\bm y\lto(\bm x,z)\mathrel I(\bm y,w)\bigr),\\
  \Forall{\bm x}\Forall{\bm y}\Forall{\bm z}\Forall{\bm w}
(\bm x\mathrel I\bm y
\land\bm z\mathrel I\bm w
\liff(\bm x,\bm z)\mathrel I(\bm y,\bm w)\bigr).
\end{gather*}
Also,
let $\Gamma$ consist of the unnested atomic formulas of $\sig$
of one of the precise forms
\begin{align*}
v_0&=v_1,&
  &Rv_0\cdots v_n,&Fv_0\cdots v_{n-1}&=v_n.
\end{align*}
Since $\sig$ is assumed to be finite,
$\Gamma$ is also finite,
and there is some $n$ such that
each formula in $\Gamma$ is $(n+1)$-ary.
Then $\tau$ can have, as a conjunct,
\begin{multline*}
\forall{x_0}\cdots\Forall{x_n}
\forall{y_0}\cdots\Forall{y_n}\\
\left(\bm x\mathrel I\bm y\lto
\bigwedge_{\phi\in\Gamma}\bigl(\phi(x_0,\dots,x_n)
\liff\psi(y_0,\dots,y_n)\bigr)\right).
\end{multline*}
Here the $x_k$ are understood to range over $A$,
while $\bm x$ is the image of $(x_0,\dots,x_n)$ in $A^{<\upomega}$;
likewise with $y$ for $x$ and $B$ for $A$;
and the two instances of $\phi$ are also appropriately \textbf{relativized,}%
\label{relative}
that is, their variables are assigned to the sorts $A$ and $B$ respectively.
Now, in any model of $\tau$, 
the symbol $I$ will be interpreted as a nonempty subset of $I$
(though not necessarily as $I$ itself).
Finally,
by the Relativization property,
we let $\tau$ have, as conjuncts,
$\sigma$ relativized to $A$
and $\lnot\sigma$ relativized to $B$.
Then we have $\tau$ as desired.
\end{proof}

If $I_k\neq0$, we write
\begin{equation*}
  \str A\equiv_k\str B.
\end{equation*}

\begin{theorem}
  If $\sig$ is finite,
then for all $n$ in $\upomega$ 
there is a finite set $\Gamma_n$ of sentences of $\sig$ such that
\begin{equation*}
  \str A\equiv_n\str B\iff
\{\sigma\in\Gamma_n\colon\str A\models\sigma\}
=\{\sigma\in\Gamma_n\colon\str B\models\sigma\}.\qedhere
\end{equation*}
\end{theorem}

\begin{proof}
Assuming $\sig$ is finite,
for each $n$ in $\upomega$, for each $k$ in $n+1$,
we shall define a finite set $\Gamma^k_{n-k}$ 
of $k$-ary formulas such that,
\begin{multline}\label{eqn:G}
  \text{for all $\bm a$ in $A^k$ and $\bm b$ in $B^k$, }\;
  \bm a\mathrel{I_{n-k}}\bm b\iff\\
\{\phi\in\Gamma^k_{n-k}\colon\str A\models\phi(\bm a)\}
=\{\phi\in\Gamma^k_{n-k}\colon\str B\models\phi(\bm b)\}.
\end{multline}
We can let $\Gamma^n_0$ 
be the set of all $n$-ary unnested atomic formulas of $\sig$.
If $\ell<n$, and we have a finite set $\Gamma^{\ell+1}_{n-\ell-1}$ 
of $(\ell+1)$-ary formulas such that \eqref{eqn:G} holds when $k=\ell+1$,
then we can let
\begin{equation*}
\Gamma^{\ell}_{n-\ell}=
\left\{
\Forall{v_{\ell}}\bigvee_{\phi\in X}\phi\land
\bigwedge_{\phi\in X}\Exists{v_{\ell}}\phi
\colon X\included\Gamma^{\ell}_{n-\ell}\right\}.
\end{equation*}
So we have $\Gamma^k_{n-k}$ as desired
for all $k$ in $n+1$.
Now let $\Gamma_n=\Gamma^0_n$.
\end{proof}

Thus each equivalence relation $\equiv_n$
partitions $\Str$ into finitely many subclasses.
Moreover, each of those subclasses is a basic closed set
in the first order topology:

\begin{corollary}
  If $\sig$ is finite, then for all $n$ in $\upomega$,
there is a finite set $\Sigma_n$ of sentences of $\sig$
such that, for all structures $\str A$ of $\sig$,
there is $\sigma_n(\str A)$ in $\Sigma_n$ 
such that 
%$\str A\models\sigma_n(\str A)$, and 
for all structures $\str B$ of $\sig$,
\begin{equation*}
  \str A\equiv_n\str B\iff\str B\models\sigma_n(\str A).
\end{equation*}
\end{corollary}

\begin{proof}
  Let $\sigma_n(\str A)$ be
  \begin{equation*}
    \bigwedge\{\sigma\in\Gamma_n\colon\str A\models\sigma\}
\land\bigwedge\{\lnot\sigma\colon\sigma\in\Gamma_n\And\str A\nmodels\sigma\}.
\qedhere
  \end{equation*}
\end{proof}

\begin{theorem}[Lindstr\"om]
In every abstract logic of $\sig$
that admits the L\"owenheim--Skolem and Compactness Theorems,
every sentence is logically equivalent to a first order sentence.
\end{theorem}

\begin{proof}
Suppose $\sigma$ is a sentence of such a logic,
and $\sig$ consists of the symbols in $\sigma$, so $\sig$ is finite.
We shall show that, for some $n$ in $\upomega$,
for all $\str A$ and $\str B$ in $\Str$,
\begin{equation}\label{eqn:iff}
  \str A\equiv_n\str B\implies(\str A\models\sigma\iff\str B\models\sigma).
\end{equation}
If this does hold, 
then $\Mod{\sigma}$ is $\bigcup_{\tau\in X}\Mod{\tau}$ 
for some subset $X$ of $\Sigma_n$, namely 
\begin{equation*}
\{\sigma_n(\str A)\colon\str A\in\Mod{\sigma}\};
\end{equation*}
this means
 $\sigma\sim\bigvee X$.
Suppose however \eqref{eqn:iff} fails for all $n$.
Then for all $n$ there are $\str A_n$ and $\str B_n$ such that
\begin{align*}
  \str A_n&\equiv_n\str B_n,&
\str A_n&\models\sigma,&
\str B_n&\models\lnot\sigma.
\end{align*}
We define a sequence $(\sigma_n\colon n\in\upomega)$
recursively so that
\begin{itemize}
\item 
each $\sigma_n$ is in $\Sigma_n$;
\item
$\{k\in\upomega\colon\str A_k\models\sigma_n\}$ is infinite;
\item
$\Mod{\sigma_{n+1}}\included\Mod{\sigma_n}$.
\end{itemize}
By Compactness
(and the Relativization property of $\Sna$),
there is a structure $(\str A,\str B)$
such that
$\str A\models\sigma$ and $\str B\models\lnot\sigma$,
but both $\str A$ and $\str B$ are models of the $\sigma_n$.
By Theorem \ref{thm:LS},
the abstract logic cannot admit the L\"owenheim--Skolem Theorem.
\end{proof}

%\bibliographystyle{amsplain}
%\bibliography{../references}

\providecommand{\MR}{\relax\ifhmode\unskip\space\fi MR }
% \MRhref is called by the amsart/book/proc definition of \MR.
\providecommand{\MRhref}[2]{%
  \href{http://www.ams.org/mathscinet-getitem?mr=#1}{#2}
}
\providecommand{\href}[2]{#2}
\begin{thebibliography}{1}

\bibitem{MR91c:03026}
C.~C. Chang and H.~J. Keisler, \emph{Model theory}, third ed., Studies in Logic
  and the Foundations of Mathematics, vol.~73, North-Holland Publishing Co.,
  Amsterdam, 1990. \MR{91c:03026}

\bibitem{MR94e:03002}
Wilfrid Hodges, \emph{Model theory}, Encyclopedia of Mathematics and its
  Applications, vol.~42, Cambridge University Press, Cambridge, 1993.
  \MR{94e:03002}

\end{thebibliography}


\end{document}
