\subsection*{\underline{#1}\nopunct}}
    \newcommand\repart[1]{\mathrm{Re}\left[ #1 \right]}
    \newcommand\impart[1]{\mathrm{Im}\left[ #1 \right]}
    \newcommand\syl[1]{\| #1 \|_{\mathrm{syl}}}
    \newcommand\stl[1]{\| #1 \|_{\mathrm{*}}}
    \newcommand\ba{\begin{align*}}
    \newcommand\ea{\end{align*}}
    \newcommand\be{\begin{enumerate}}
    \newcommand\ee{\end{enumerate}}
    \newcommand\bp{\bp }
    \newcommand\ep{\ep }
    \newcommand\bpp{\begin{prop}}
    \newcommand\epp{\end{prop}}
    \newcommand\bpb{\begin{prob}}
    \newcommand\epb{\end{prob}}
    \newcommand\bd{\begin{defn}}
    \newcommand\ed{\end{defn}}
    \newcommand\bh{\begin{hint}}
    \newcommand\eh{\end{hint}}

    \newcommand{\ja}[1]{{\color{magenta}#1}}
    \newcommand{\sam}[1]{{\color{blue}#1}}

    \newcommand\sgn{\mathrm{sgn}}
    \newcommand\stab{\mathrm{Stab}}
\newcommand\eu{\mathrm{eu}}
    \newcommand\fform[1]{\langle\!\langle #1\rangle\!\rangle}
    \newcommand\vform[1]{\vert #1\vert}
    \newcommand\vstar[1]{\| #1\|_{\mathrm{*}}}
    \newcommand\vh[1]{\| #1\|_{\mathcal{H}}}

    \newcommand\bC{\mathbb{C}}
    \newcommand\bE{\mathbb{E}}
    \newcommand\bN{\mathbb{N}}
    \newcommand\N{\mathbb{N}}
    \newcommand\bR{\mathbb{R}}
    \newcommand\bQ{\mathbb{Q}}
    \newcommand\bZ{\mathbb{Z}}
    \newcommand\Z{\mathbb{Z}}
    \newcommand\bH{\mathbb{H}}
    \newcommand\BB{\mathcal{B}}
    \newcommand\CC{\mathcal{C}}
    \newcommand\EE{\mathcal{E}}
    \newcommand\FF{\mathcal{F}}
    \newcommand\GG{\mathcal{G}}
    \newcommand\DD{\mathcal{D}}
    \newcommand\LL{\mathcal{L}}
    \newcommand\PP{\mathcal{P}}
\newcommand\UU{\mathcal{U}}
\newcommand\VV{\mathcal{V}}
\newcommand\XX{\mathcal{X}}
\newcommand\YY{\mathcal{Y}}
    \newcommand\sech{\operatorname{sech}}
    \newcommand\Sym{\operatorname{Sym}}
    \newcommand{\R}[0]{\mathbb{R}}

    \newcommand\ev{\operatorname{ev}}
    \newcommand\cay{\operatorname{Cayley}}
    \newcommand\aut{\operatorname{Aut}}
    \newcommand\Inn{\operatorname{Inn}}
    \newcommand\Mono{\operatorname{Mono}}
    \newcommand\PMod{\operatorname{PMod}}
    \newcommand\Hom{\operatorname{Hom}}
\DeclareMathOperator\Push{\mathcal{Push}}
\newcommand\vol{\operatorname{vol}}
\DeclareMathOperator\Forget{\mathcal{Forget}}
\newcommand\Isom{\operatorname{Isom}}
    \newcommand\UT{\operatorname{UT}}
    \newcommand\Comm{\operatorname{Comm}}
    \newcommand\Symp{\operatorname{Symp}}
    \newcommand\rot{\operatorname{rot}}
    \newcommand\Rot{\operatorname{Rot}}
    \newcommand\Fill{\operatorname{Fill}}
    \newcommand\supp{\operatorname{supp}}
    \newcommand\Id{\operatorname{Id}}
    \newcommand\lk{\operatorname{Lk}}
    \newcommand\Diffb{\operatorname{Diff}_+^{1+\mathrm{bv}}}
    \newcommand\Diffi{\operatorname{Diff}_+^{\infty}}
    \newcommand\Diffo{\operatorname{Diff}_{+,0}^{\infty}}
    \newcommand\diam{\operatorname{diam}}
    \newcommand\Gam{\Gamma}
    \newcommand\gam{\Gamma}
    \newcommand\Mod{\operatorname{Mod}}
    \newcommand\cc{\mathrm{cc}}
    \newcommand\rigid{\mathrm{rigid}}
    \newcommand\union{\mathrm{union}}

    \newcommand\near{\mathrm{near}}
    \newcommand\rk{\operatorname{rk}}
    \newcommand\symp{\operatorname{Symp}}
    \DeclareMathOperator\Homeo{Homeo}

    \newcommand\mC{\mathcal{C}}
    \newcommand\mL{\mathcal{L}}
    \newcommand\cM{\mathcal{M}}
    \newcommand\xek{(X^e)_k}
    \newcommand\yt{\widetilde}
    \newcommand\sse{\subseteq}
    \newcommand\co{\colon}
    \newcommand\cH{ G}
    \DeclareMathOperator\im{im}
    \DeclareMathOperator\tr{tr}
    \DeclareMathOperator\fix{fix}
    \DeclareMathOperator\Out{Out}
    \DeclareMathOperator\Aut{Aut}
    \DeclareMathOperator\CAT{CAT}
    \DeclareMathOperator\PSL{PSL}
    \DeclareMathOperator\SL{SL}
    \DeclareMathOperator\SO{SO}
    \DeclareMathOperator\Diff{Diff}
    \DeclareMathOperator\Exp{Exp}
    \newcommand\catz{\mathrm{CAT}(0)}
    \DeclareMathOperator\Stab{Stab}
    \DeclareMathOperator\Orbit{Orbit}
    \DeclareMathOperator\ro{RO}
    \DeclareMathOperator\Ro{RO}
    \DeclareMathOperator\inte{int}
    \DeclareMathOperator\cl{cl}
    \DeclareMathOperator\fr{fr}
    \DeclareMathOperator\ext{ext}
    \DeclareMathOperator\agape{AGAPE}
    \DeclareMathOperator\cont{Cont}
    \DeclareMathOperator\appl{appl}
    \DeclareMathOperator\Th{{Th}}
    \DeclareMathOperator\act{{Act}}
    \DeclareMathOperator\bdy{{bdy}}
    \DeclareMathOperator\bdle{{bdle}}
    \DeclareMathOperator\adbdle{{adbdle}}
    \DeclareMathOperator\cov{{Cov}}
    \DeclareMathOperator\embed{{Embed}}
    \DeclareMathOperator\param{{Param}}
     \DeclareMathOperator\collar{{collar}}
    \DeclareMathOperator\orb{{orb}}
     \DeclareMathOperator\comp{{comp}}
    \DeclareMathOperator\cfibr{{cfibr}}
    \DeclareMathOperator\paramball{{ParamBall}}
    \DeclareMathOperator\paramfnc{{ParamFnc}}
    \DeclareMathOperator\flow{Flow}
    \newcommand{\p}[0]{\mathsf{p}}
    \newcommand{\q}[0]{\mathsf{q}}

    \newcommand\suppo{\operatorname{supp}^\circ}
    \newcommand\supt{\operatorname{supt}}
    \newcommand\suppc{\operatorname{\overline{supp}}}
\newcommand\suppe{\operatorname{{supp}^{\mathrm{e}}}}
\newcommand\bG{\mathbf G}

    \renewcommand{\thefootnote}{\alpha{footnote}}
    \newcommand{\arxiv}[1]
    {\texttt{\href{http://arxiv.org/abs/#1}{arXiv:#1}}}
    \newcommand{\doi}[1]
    {\texttt{\href{http://dx.doi.org/#1}{doi:#1}}}
    \renewcommand{\MR}[1]
    {\href{http://www.ams.org/mathscinet-getitem?mr=#1}{MR#1}}

    \def{First order rigidity of homeomorphism groups of manifolds}{{First order rigidity of homeomorphism groups of manifolds}}
    \def{J. de la Nuez Gonz\'alez, Sang-hyun Kim, Thomas Koberda}{{J. de la Nuez Gonz\'alez, Sang-hyun Kim, Thomas Koberda}}
    \usepackage{hyperref}
    \hypersetup{

    	colorlinks=false,
    	plainpages,
    	urlcolor=black,
    	linkcolor=black
    	pdftitle=   {First order rigidity of homeomorphism groups of manifolds},
    	pdfauthor=  {{J. de la Nuez Gonz\'alez, Sang-hyun Kim, Thomas Koberda}}
    }

    \theoremstyle{plain}
    \newtheorem{thm}{Theorem}[section]
    \newtheorem{lem}[thm]{Lemma}
    \newtheorem{lemma}[thm]{Lemma}
    \newtheorem{cor}[thm]{Corollary}
    \newtheorem{prop}[thm]{Proposition}
    \newtheorem{con}[thm]{Conjecture}
    \newtheorem{que}[thm]{Question}
    \newtheorem{obs}[thm]{Observation}
    \newtheorem*{claim*}{Claim}
    \newtheorem*{fact}{Fact}
    \newtheorem{claim}{Claim}
    \newtheorem{thmA}{Theorem}
    \renewcommand*{\thethmA}{\Alph{thmA}}
    \newtheorem{corA}[thmA]{Corollary}
    \renewcommand*{\thecorA}{\Alph{corA}}

    \theoremstyle{remark}
    \newtheorem{exmp}[thm]{Example}
    \newtheorem{rem}[thm]{Remark}

    \theoremstyle{definition}
    \newtheorem{defn}[thm]{Definition}
    \newtheorem{prob}{Problem}[section]
    \newtheorem{setting}[thm]{Setting}

    \begin{document}
    \title{First order rigidity of homeomorphism groups of manifolds}
    \date{\today}
    \keywords{homeomorphism group, manifold, first order theory, elementary equivalence}
    \subjclass[2020]{Primary: 20A15, 57S05, ; Secondary: 03C07, 57S25, 57M60}

    \author[S. Kim]{Sang-hyun Kim}
    \address{School of Mathematics, Korea Institute for Advanced Study (KIAS), Seoul, 02455, Korea}
    \email{skim.math@gmail.com}
    \urladdr{https://www.cayley.kr}

    \author[T. Koberda]{Thomas Koberda}
    \address{Department of Mathematics, University of Virginia, Charlottesville, VA 22904-4137, USA}
    \email{thomas.koberda@gmail.com}
    \urladdr{https://sites.google.com/view/koberdat}

    \author[J. de la Nuez Gonz\'alez]{J. de la Nuez Gonz\'alez}
    \address{School of Mathematics, Korea Institute for Advanced Study (KIAS), Seoul, 02455, Korea}
    \email{jnuezgonzalez@gmail.com}

    \begin{abstract}
    	For every compact, connected manifold $M$, we prove the existence of a sentence $\phi_M$ in the language of groups such that
the homeomorphism group of another compact manifold $N$ satisfies
 $\phi_M$ if and only if $N$ is homeomorphic to $M$.
	We prove the analogous statement for groups
    	of homeomorphisms preserving an Oxtoby--Ulam probability measure.
    \end{abstract}

    \maketitle

\setcounter{tocdepth}{1}
\tableofcontents

\section{Introduction}\label{sec:intro}
In this paper, a \emph{manifold} will be a Hausdorff, second countable, locally Euclidean topological space.
For a manifold $M$ (possibly equipped with a measure $\mu$), we let $\Homeo(M)$ and $\Homeo_\mu(M)$
denote the homeomorphism group of $M$ and its $\mu$--preserving subgroup, respectively.
We denote by $\Homeo_0(M)$ and $\Homeo_{0,\mu}(M)$ the identity components of $\Homeo(M)$ and $\Homeo_\mu(M)$, respectively. We will use the terminology \emph{bounded manifold} and \emph{manifold with boundary} interchangeably.

Let us denote by $\cM$
 the class of all pairs $(M,\cH)$,
where $M$ is a compact, connected manifold
and $\cH$ is a group satisfying
\[
\Homeo_0(M)\le \cH\le\Homeo(M).
\]
We also let $\cM_{\vol}$ denote
the class of all $(M,\cH)$
where $M$ is further assumed to be
equipped with an \emph{Oxtoby--Ulam measure} $\mu$ (that is, a nonatomic Borel probability measure having full support and assigning measure zero to the boundary),
and $\cH$ is a group satisfying
\[
\Homeo_{0,\mu}(M)\le \cH\le\Homeo_\mu(M).
\]
Note~\cite{Fathi1980} in this case that
\[
\Homeo_{0,\mu}(M)=\Homeo_0(M)\cap\Homeo_\mu(M).
\]

In statements that apply to both of the classes $\cM$ and $\cM_{\vol}$, we will often use the notation $\cM_{(\vol)}$;
in such a statement, the choices of formulae may differ, even when the formulae share the same names.
We will later modify the definitions of these classes slightly so that only manifolds of dimension at least two are considered; see the remark at the end of Section~\ref{ss:top}.

The goal of this paper is to investigate,
under the assumption that $(M,\cH)\in\cM_{(\vol)}$,
the extent to which the elementary theory of $\cH$ determines the homeomorphism type of $M$.

\subsection{Elementary equivalence implies homeomorphism}

    It is a classical result of Whittaker that the homeomorphism group of a compact manifold determines the homeomorphism type of the
    underlying manifold in the following sense.

\begin{thm}[See~\cite{whittaker}]\label{thm:Whittaker}
Let $M$ and $N$ be compact manifolds, and suppose \[\phi\colon \Homeo(M)\longrightarrow\Homeo(N)\] is an isomorphism of groups.
Then there exists a homeomorphism \[\psi\colon M\longrightarrow N\] such that for all $f\in\Homeo(M)$, we have $\phi(f)=\psi\circ f\circ\psi^{-1}$.
    \end{thm}

Whittaker's result has been generalized by a number of authors; see Chapter 3 of~\cite{KK2021book} for a survey. For instance, combining the work of Bochner--Mongomery~\cite{BM1945} on Hilbert's eighth problem and of Takens on smooth conjugation between diffeomorphisms~\cite{takens} (cf.~\cite{filipkiewicz}), one obtains that if $M$ and $N$ are smooth and closed, and if the diffeomorphism groups $\Diff^k(M)$ and $\Diff^{\ell}(N)$
are isomorphic as groups, then $k=\ell$ and
each isomorphism
between the groups is induced by
some $C^k$--diffeomorphism between $M$ and $N$.

In the continuous category, a different generalization was given by Rubin.
We say a topological action of a group $G$ on a topological space $X$ is \emph{locally dense} if for each pair $(x,U)$ of a point $x\in X$
and a neighborhood $U\sse X$ of $x$,
the orbit $Z$ of $x$ by the action of the group
\[
G[U]:=\{g\in G\mid g(y)=y\text{ for all }y\not\in U\}
\]
is somewhere dense; that is, the closure of $Z$ has nonempty interior.
Rubin's Theorem can be stated as follows.

\begin{thm}[\cite{Rubin1989}]\label{thm:rubin-intro}
Let $X_1$ and $X_2$ be perfect, locally compact, Hausdorff topological spaces, and let $G_i\leq \Homeo(X_i)$ be locally dense subgroups, for $i\in\{1,2\}$. Suppose that there exists an isomorphism \[\phi\colon G_1\longrightarrow G_2.\] Then there exists a homeomorphism \[\psi\colon X_1\longrightarrow X_2\] such that for all $g\in G_1$, we have $\phi(g)=\psi\circ g\circ\psi^{-1}$. \end{thm}

An isomorphism between two groups of homeomorphisms is a rather unwieldy piece of data. Homeomorphism groups of manifolds are generally much to large to write down, and directly accessing homomorphisms between them is difficult. Therefore in this paper, we are interested in more finitary ways of investigating homeomorphism groups of manifolds, namely through their elementary theories.

We consider the language of groups, which consists of a binary operation (interpreted as the group operation) and a constant (interpreted as the identity element). Models of the theory of groups are just sets with interpretations of the group operation and identity element which satisfy the axioms of groups. We say that two groups $G_1$ and $G_2$ are \emph{elementarily equivalent}, written $G_1\equiv G_2$, if every first order sentence in the language of groups holds in $G_1$ if and only if it holds in $G_2$; this is sometimes expressed as saying that the theories of $G_1$ and $G_2$ agree, i.e.~$\Th(G_1)=\Th(G_2)$. Here, \emph{first order} refers to the scope of quantification, which is allowed to range over elements (as opposed to subsets, relations, or functions).

Our main result is to establish that
two compact, connected manifolds have elementarily equivalent homeomorphism groups
if and only if the two manifolds are homeomorphic to each other.

More strongly, for each compact connected manifold $M$
 we prove the existence of a group theoretic sentence that asserts ``I am homeomorphic to $M$'':

\begin{thm}\label{thm:main}
For each compact, connected manifold $M$,
there exists a sentence $\phi_M^{(\vol)}$ in the language of groups such that
when $(N,\cH)\in\cM_{(\vol)}$,
we have that
\[
\phi_M^{(\vol)}\in\Th(\cH)\qquad\text{iff}\qquad N\cong M.\]
\end{thm}

In other words, the theories of homeomorphism groups of manifolds
are \emph{quasi-finitely axiomatizable} within the class
$\cM_{(\vol)}$, a property that is stronger than first order rigidity.

In Theorem~\ref{thm:main}, we emphasize that $M$ and $N$ are not assumed to have any further structure, such as a smooth or piecewise-linear structure. We thus generalize Whittaker's result and produce for each manifold a finite, group--theoretic sentence that certifies homeomorphism or non--homeomorphism with the manifold.
The sentences $\phi_M$ and $\phi_M^{\vol}$ are produced explicitly insofar as is possible,
{though in practice it would be quite a complex task to write those down.
We note that the connectedness hypothesis for $N$ can also be dropped from the theorem;
see
part
(\ref{p:cnt1-2})
of
Lemma~\ref{lem:top-prop}, for instance.
}

We remark that Theorem~\ref{thm:main} fits within a tradition of results proving first order rigidity of various structures, such as lattices in higher rank~\cite{avni-etal}, function fields~\cite{duret1,duret2,vidaux,Pop02}, rings~\cite{leloup,greenfeld}, finite--by--abelian groups~\cite{oger}, and linear groups~\cite{plotkin}, and into the philosophy of distinguishing between objects that are difficult to access directly via finite syntactic objects.

Another perspective on Theorem~\ref{thm:main} centers around the following question; a number of other motivating questions are enumerated in Section~\ref{sec:questions}.

    \begin{que}\label{que:homeo-action}
    	Let $M$ be a compact, connected manifold. Under what conditions is there a finitely generated (or countable) group $G_M\leq \Homeo(M)$ such that if $N$ is a
    	compact manifold with $\dim M=\dim N$ on which $G_M$ acts faithfully, then $M\cong N$?
    \end{que}

    Related results for actions of the full homeomorphism group of $M$ are given by Chen--Mann~\cite{chen-mann}. They show that
    if the identity component of $\Homeo(M)$ acts transitively on a connected manifold or CW--complex $N$, then $N$ is homeomorphic
    to a cover of a configuration space of points of $M$. In our context, we have the following immediate consequence of the downward
    L\"owenheim--Skolem Theorem:

    \begin{cor}\label{cor:L-S}
To each compact connected manifold $M$
one can associate a countable group $G_M\leq \Homeo(M)$ that is elementarily equivalent to $\Homeo(M)$, and such that
for two compact, connected manifolds $M$ and $N$ we have
\[G_M\equiv G_N\quad\textrm{if and only if}\quad M\cong N.\]
In particular
    	$G_M\cong G_N$ if and only if $M\cong N$.
    \end{cor}

    \begin{rem}
    	In~\cite{Rubin1989}, there is a cryptic announcement of a version of Theorem~\ref{thm:main}. In particular, Rubin claims that under
    	the assumption $V=L$ (i.e.~G\"odel constructibility) that two arbitrary connected manifolds are homeomorphic if and only if their
    	homeomorphism groups are elementarily equivalent;
     it is likely that
     he implicitly made a few other assumptions to avoid trivial counterexamples such as $\Homeo(0,1)\cong\Homeo[0,1]$. To the knowledge of the authors, the paper
    	bearing the title announced in~\cite{Rubin1989} never appeared, and neither did any result
    	(of any authors whatsoever) proving first order rigidity of homeomorphism
    	groups of manifolds; cf.~a related MathOverflow post~\cite{MO-Rubin}.
	We note that we only establish the main result for compact manifolds, in contrast to Rubin's original announcement,
    	and Rubin's remark about the constructible universe
    	remains puzzling to us.
    \end{rem}

{
Our proof of Theorem~\ref{thm:main} largely consists of two parts.
The first part is an expansion of the group theory language to a seemingly more powerful language, called $\agape$. The universe of an $\agape$ structure corresponding to $(M,\cH)\in\cM_{(\vol)}$ then contains the group $\cH$, the real numbers $\bR$, the maps $C^0([0,1]^n,\bR^\ell)$ for $n,\ell\in\omega$
and the finite subsets of $M$.
Since the expansion is specified by first order definitions, we deduce the following, which roughly means that each sentence in the theory of $\agape(M,\cH)$ can be translated, in a way that is independent of $(M,\cH)$, to a sentence in the theory of the group $\cH$; see Section~\ref{sec:prelim} for the precise definition of \emph{uniform interpretation}.
\begin{thm}\label{thm:interpret}
Uniformly for $(M,\cH)\in \cM_{(\vol)}$,
the structure $\agape(M,\cH)$ is interpretable in the group structure $\cH$.
\end{thm}

The second part is to show that the $\agape$ language can express the sentence that ``I am homeomorphic to $M$'':
\begin{thm}\label{thm:iamM}
For each compact, connected manifold $M$,
there exists an $\agape$ sentence $\psi^{(\vol)}_M$
such that for all $(N,\cH)\in\cM_{(\vol)}$,
we have
\[\psi^{(\vol)}_M\in\Th\agape(N,\cH)\quad
\text{iff}\quad N\cong M.\]
\end{thm}
By Theorem~\ref{thm:interpret},
we can interprete $\psi_M^{(\vol)}$ to a group theoretic sentence $\phi_M^{(\vol)}$ that distinguishes $M$ from any other non-homeomorphic manifolds $N$;
see Lemma~\ref{lem:inter-models} for a more formal explanation.
We thus obtain a proof of Theorem~\ref{thm:main}.}

We briefly announce a related result, which will appear in~\cite{kkdln-pre}.
If $G\leq \Homeo(M)$, we say that $G$ is
    \emph{rigidly dense} if for every regular open $U\sse M$, we have $G[U]$ is dense in $\Homeo(M)[U]$    in the $C^0$ topology.

A natural example of a proper rigidly dense subgroup of $\Homeo(M)$ is the group of piecewise linear homeomorphisms. The authors will show under mild hypotheses for a compact manifold $M$ of fixed dimension $n\in\{1,2,3\}$,
there is a sentence $\phi_M$ in the language of groups such that whenever $G\leq\Homeo(N)$ are rigidly dense for some compact manifold $N$, then $G\models \phi_N$ if and only if $M\cong N$.

Thus, within manifolds of fixed low--dimension, there are sentences which identify the homeomorphism type of a compact, connected manifold via the elementary theories of rigidly dense groups of homeomorphisms. The principle reason that the conclusions in the case of rigidly dense subgroups are somewhat weaker is that one does not have access to the full richness of the regular open sets of $M$, and the regular open sets to which one has access may even fail to be closed under the Boolean operations. Several steps in the proof of Theorem~\ref{thm:main} do not carry over to the rigidly dense case.

  \subsection{Outline of the paper}

    The paper proves Theorem~\ref{thm:main} in several steps, each of which builds on the previous.
    Section~\ref{sec:prelim} gathers basic results, fixes notation,
    interprets the regular open sets in $\cH$, and constructs several general formulae that encode
    various topological properties of regular open sets.
    Section~\ref{sec:arith} interprets second order arithmetic using regular open sets
    and actions of homeomorphisms on them. Section~\ref{sec:points} uses arithmetic to encode individual points of a manifold, and uses
    this encoding to interpret finite collections of points and the exponentiation map. Section~\ref{sec:balls} interprets the dimension
    of a manifold, as well as embedded Euclidean balls in a manifold.
    Section~\ref{sec:boundary} interprets collar neighborhoods of boundary components of a compact manifold. Section~\ref{sec:homeo} proves Theorem~\ref{thm:main}
    for closed manifolds by
    interpreting a result of Cheeger--Kister~\cite{CK1970} in order to encode embeddings of manifolds of Euclidean spaces that are
    ``close enough". Section~\ref{sec:homeo} also addresses the case of manifolds with boundary.
    We conclude with some questions in Section~\ref{sec:questions}.

\section{Preliminaries}\label{sec:prelim}
In this section, we gather some notation, background, and generalities.

\subsection{Transitivity of balls in manifolds}
The high degree of transitivity of the action of homeomorphism groups
on balls in manifolds is crucial for this paper. We begin with the
following fundamental fact regarding Oxtoby--Ulam measures.

\begin{thm}[von Neumann~\cite{vonNeumann1961},
Oxtoby--Ulam~\cite{oxtoby-ulam}]\label{thm:ou}
If $\mu$ and $\nu$ are Oxtoby--Ulam measures on a compact connected manifold $M$ then there exists a homeomorphism $h$ of $M$ isotopic to the identity and
fixing the boundary such that $h_*\mu=\nu$.
\end{thm}

Thus, for Oxtoby--Ulam measures, the groups of measure-preserving homeomorphisms of $M$ are all conjugate to each other.
We will therefore refer to groups of \emph{measure-preserving homeomorphisms} without specifying a particular Oxtoby--Ulam measure.  We refer the reader to~\cite{Fathi1980,Banyaga1997} for generalities about measure-preserving homeomorphisms.

A group theoretic interpretation of (certain) balls in a manifold will be a crucial step in this paper.
By $B^n(r,p)$, we mean the compact ball of radius $r>0$ about the center $p$ in the Euclidean space $\bR^n$.
If $p$ is the origin then we simply write $B^n(r)$.
If there is no risk of ambiguity, we often suppress the dimension from the notation.

We call a topologically embedded image of $B^n(r)$ in a manifold $M$ a \emph{Euclidean $n$--ball}, or more traditionally, an \emph{$n$--cell}. The same goes for an \emph{open Euclidean ball} and an \emph{open $n$--cell} in $M$.
If there exists an embedding $h\co B^n(2)\to M$, then the image $h(B^n(1))$ is called a \emph{collared ball}~\cite[Chapter 17]{CV1977}. The same goes for a \emph{collared open ball}.
In the case when $M$ is equipped with an Oxtoby--Ulam measure, we say a collared ball $B$ is $\mu$--\emph{good} (or, simply \emph{good}) if $\partial B$ has measure zero.
There exists an arbitrarily small covering of $M$ by $\mu$--good balls~\cite{Fathi1980}.
\emph{For the brevity of the exposition,
we mean by a \emph{good ball} both a collared ball in the context of $(M,G)\in\cM$ and a $\mu$--good ball in the context of $(M,G)\in\cM_{\vol}$. The same goes for a good open ball.}

We let $\Homeo(M,\partial M)$ denote the subgroup of $\Homeo(M)$
consisting of homeomorphisms $g$ satisfying $g\restriction_{\partial M}=\Id$.
We define the subgroups
$\Homeo_0(M,\partial M)$
and $\Homeo_{0,\mu}(M,\partial M)$
 similarly.

The following fundamental fact in the case $k=1$ can be found in~\cite[Corollaries 2.1 and 2.2]{LeRoux2014}.
The general case is an easy consequence, by a similar argument for the proof of $k$--fold transitivity of diffeomorphism groups~\cite[Lemma 2.1.10]{Banyaga1997}.

\begin{lem}\cite[Corollaries 2.1 and 2.2]{LeRoux2014}\label{lem:transitive}
For a compact connected $n$--manifold $M$ with $n\ge2$,
and for a connected regular open set $U$ in $M$,
the following hold.
\be
\item
The group $\Homeo_0(M,\partial M )[U]$ acts transitively on the set of disjoint $k$--tuples of collared balls in $U$.
\item
If $M$ is equipped with an Oxtoby--Ulam measure $\mu$, and if  $(B_1,\ldots,B_k)$ and $(B_1',\ldots,B_k')$ are disjoint $k$--tuples of collared balls in $U$, then there exists an element $g\in \Homeo_{0,\mu}(M,\partial M)[U]$ such that for some good balls $C_i\sse B_i$ and $C_i'\sse B_i'$, we have $g(C_i)=C_i'$. We can further require that each $C_i$ has an arbitrarily small positive measures.
\ee
\end{lem}

The following lemma is originally due to Brown~\cite{Brown1962b}. We use a version modified by Fathi~\cite{Fathi1980}.
One may consider this as a natural generalization of the fact that every compact connected 2-manifold can be obtained by gluing up the boundary of a polygon in a suitable way.
See also~\cite{CV1977,LeRoux2014} for more details.

\begin{lem}[\cite{Brown1962b,Fathi1980}]\label{lem:brown-measure}
If a compact connected $n$--manifold $M$ is equipped with an Oxtoby--Ulam measure $\mu$, then there exists a continuous surjection \[f\colon B^n
\longrightarrow M\] such that the following hold:
\begin{enumerate}[(i)]
\item
the restriction of $f$ on  $\inte B^n$ is an embedding;
\item
we have $f(\inte B^n)\cap f(\partial B^n)=\varnothing$,
and in particular, $\partial M\sse  f(\partial B^n)$;
\item
we have $\mu(f(\partial B^n))=0$;
\item\label{p:brown-leb}
The measure $\mu$ is the pushforward of Lebesgue measure by $f$.
\end{enumerate}
\end{lem}
In fact, the requirement (\ref{p:brown-leb}) is to be satisfied by Theorem~\ref{thm:ou}; see also~\cite{GP1975}. For a possbily non-compact manifold, we have the following variation also due to Fathi, which loosens the condition on the surjectivity of the map.
\begin{lem}[\cite{Fathi1980}]\label{lem:brown-measure2}
If a connected $n$--manifold $M$ has nonempty boundary
and if $M$ is equipped with a nonatomic, fully supported Radon measure $\mu$ that assigns zero measure to $\partial M$, then there exists an open embedding
\[
f\co \bH^n_+:=\{(x_1,\ldots,x_n)\in\bR^n\mid x_n\ge0\}\to M
\]
such that the following hold:
\be[(i)]
\item $f(\inte \bH^n_+)\sse\inte M$ and $f(\partial\bH^n_+)\sse\partial M$;
\item $M\setminus f(\bH^n_+)$ is closed and of measure zero.
\ee
\end{lem}

\begin{lem}\label{lem:measure-ball}
Let $M$ be a compact, connected $n$--manifold with $n\ge2$,
equipped with an Oxtoby--Ulam measure $\mu$.
If $U\sse M$ is an open connected subset, then for each positive real number $r<\mu(U)$, there exists a good ball of measure precisely $r$ inside $U\cap\inte M$. Moreover, we may require that $U\setminus B$ is connected.
\end{lem}
\begin{proof}
Note the general fact that for a connected open subset $U$ of $M$ and for a locally flat ball $B$ in $U\cap\inte M$, the set $U\setminus B$ is connected; this can be seen from that a locally flat ball is cellular, and that each celluar set is pointlike~\cite[Chapter 17]{CV1977}.

Pick sufficiently small good balls $Q\sse U\cap\inte M$
such that
the connected, bounded $n$--manifold $M':=U\setminus \inte Q$ has measure larger than $r$. Applying Lemma~\ref{lem:brown-measure2} to the bounded manifold $M'$, we have an open embedding
\[
f\co \bH^n_+\longrightarrow M'
\]
such that \[f(\partial \bH^n_+)\sse \partial M'=\partial Q.\]
Since $\inte \bH^n_+$ is a countable increasing union of locally flat balls,
we can find a locally flat ball $\hat B$ in $M'\cap\inte M$ having measure larger than $r$;
moreover, we can further require that $\hat B$ is good since in general,  all but countably many disjoint spheres in $\inte\bH^n_+$ will map to measure zero sets.
Applying Theorem~\ref{thm:ou} to $\hat B$, we see that the restriction of $\hat B$ is conjugate to a Lebesgue measure on a cube.
It is then trivial to find a good ball $B\sse \hat B$
with measure precisely $r$.
\end{proof}

For a later use, let us record the following form of ``almost--transitivity'' between open connected subsets in the measure--preserving setting.

\begin{lem}\label{lem:measure-sum}
Let $M$ be a compact connected $n$--manifold with $n\ge2$,
equipped with an Oxtoby--Ulam measure $\mu$.
Suppose we have a finite disjoint collection of open connected sets $\{U_1,\ldots,U_k\}$, and an open connected set $V$ in $M$.
If positive real numbers $r_1,\ldots, r_k$ satisfying
$r_i<\mu(U_i)$ for each $i$ and \[\sum_i r_i<\mu(V),\]
then we have an element $g\in\Homeo_{0,\mu}(M,\partial M)$
and a good ball $B_i\sse U_i$ of measure $r_i$ for each $i$
such that $U_i\setminus B_i$ is connected,
and such that \[g\left(\bigcup_{i=1}^k B_i\right)\subseteq V.\]
\end{lem}
\begin{proof}
By Lemma~\ref{lem:measure-ball}, we have good balls $B_1\sse U_1\cap \inte M$
and $C_1\sse V\cap \inte M$ having measures precisely $r_1$.
From Lemma~\ref{lem:transitive}, we see that some $g_1\in\Homeo_{0,\mu}(M,\partial M)$ maps $B_1$ homeomorphically onto $C_1$. We now repeat this argument to the manifold $M\setminus (\inte B_1\cup \inte C_1)$ and the pair of open sets $(U_2,V\setminus\inte C_1)$, and find $g_2\in\Homeo_{0,\mu}(M,\partial M)$ fixing $B_1\cup C_1$ and mapping some good ball $B_2\sse U_2$ of measure $r_2$ onto another good ball $C_2\sse (V\cap\inte M)\setminus C_1$. Itereating this process, we obtain homeomorphisms $g_1,\ldots,g_k$ such that $g:=g_k\cdots g_1$ is the desired map.
\end{proof}

\subsection{Regular open sets and homeomorphism groups}
Let $S$ be a topological space.
If $A\subseteq S$ is a subset then we write $\cl A$ and $\inte A$ for its closure and interior, respectively, and
    \[
    \fr(A):=\cl A\setminus\inte A\] for the \emph{frontier} of $A$.

A set $U\sse X$ is \emph{regular open} if $U=\inte\cl U$.
For instance, a good ball is always regular open.
The set of regular open subsets of $X$ forms a Boolean algebra, denoted as $\ro(M)$.
In this Boolean structure,
the minimal and maximal elements are the empty set and $X$ respectively.
The meet is the intersection,
and the join of two regular open sets $U$ and $V$ is given by \[U\oplus V:=\inte\cl(U\cup V).\] The complement coincides with the exterior: \[U^{\perp}:=X\setminus \cl U.\]
Consequently, the Boolean partial order $U\le V$ coincides with the inclusion $U\sse V$ for $U,V\in \ro(X)$. For each subcollection $\FF\sse \ro(X)$ of regular open sets we can define its supremum as
\[ \sup \FF :=\inte\cl\left( \bigcup \FF\right)\in\ro(X).\]
In particular, $\ro(X)$ is a complete Boolean algebra.
We remark briefly that the collection of open sets of a manifold (or indeed of an arbitrary topological space) is not a Boolean algebra in a natural way, but rather a Heyting algebra, since it is possible that $U\subsetneq U^{\perp\perp}$.

We will repeatedly use the following straightforward fact, which in particular implies that every nonempty open subset of a manifold contains a nonempty relatively compact regular open set.

\begin{lem}\label{lem:shrink}
If an open set $U$ in a manifold $M$
contains a closed set $C$,
then there exists a regular open set $V$ such that
\[C\subseteq V\subseteq \cl V\sse U.\]
If, furthermore, $C$ is compact then we can require $V$
to be relatively compact.
\end{lem}
\begin{proof}
From the normality of $M$, we obtain an open set $W$ such that
\[
C\sse W\sse \cl W\sse U.\]
Then $V:=\inte \cl W$ satisfies the first conclusion.
If $C$ is compact, then we even use only the local compactness of the ambient space
to find a relatively compact $W$ and obtain the second conclusion.
\end{proof}

Let $g\in\Homeo(X)$.
We denote its fixed point set by $\fix g$, and define its \emph{(open) support} as $\supp g:=X\setminus \fix g$.
We then define its \emph{extended support} as
\[
\suppe g:= \inte\cl \supp g = \inte \cl (X\setminus\fix g).
\]
Let $G\le\Homeo(X)$.
We define
a \emph{rigid stabilizer (group)} as
\[
G[A]:=\{g\in G\mid  \supp g\sse A\}.\]
If $U$ is regular open in $X$, we note that
\[G[U]=\{g\in G\mid \suppe g\sse U\}.
\]

Recall from the introduction that the group $G\le\Homeo(S)$ is \emph{locally dense}
if for each nonempty open set $U$ and for each $p\in U$ we have hat
\[
\inte\cl G[U].p\ne\varnothing.
\]
More weakly, we say $G$ is \emph{locally moving} if the rigid stabilizer of each nonempty open set is nontrivial.

If $G$ is a locally moving group of homeomorphisms of $S$ then $\ro(M)$ has no atoms, and the set of extended supports \[ \{\suppe g\mid g\in G\}\] is \emph{dense} in the complete Boolean algebra $\ro(M)$, i.e.~ for all $U\in\ro(M)$ there exists $g\in G$ such that $\suppe g\subseteq U$; see \cite{Rubin1996} and \cite[Theorem 3.6.11]{KK2021book}.
When the ambient space is a manifold,
we note a fundamental observation that every regular open set can actually be represented as the extended support of some homeomorphism.

\begin{prop}\label{prop:full-support}
Suppose either that $(M,G)\in\cM$  with $\dim M\ge1$,
or that $(M,G)\in\cM_{\vol}$ with $\dim M>1$.
Then each regular open set $U$ of $M$ is the extended support of some $g\in G$.
\end{prop}

  \begin{proof}
Pick a countable dense subset $\{x_i\}_{i\in\omega}$ of a given regular open set $U$. We let $y_1:=x_1$ and pick $V_1\sse U$ which is a good open ball containing $y_1$ with diameter less than $1$. Suppose that for $1\leq i\leq k-1$ we have constructed $(y_i,V_i)$, with the property that $\{V_i\}_{i=1}^{k-1}$ is a collection of good open    balls inside $U$ with disjoint closures, with $y_i\in V_i$ for each $i$,     and such that $\diam V_i<1/i$.

If $U=\bigcup_{i=1}^k V_i$, then we terminate the procedure; otherwise, let $x_j$ be the point in the countable dense subset with minimal index such that \[x_j\in W=U\cap \left(\bigoplus_{i=1}^{k-1} V_i\right)^\perp.\] Pick a good open ball $V_k$ whose closure is contained in $W$ with $\diam V_k<1/k$, and such that $x_j\in V_k$. Thus, we build a (finite or infinite) collection of open balls  $\{V_i\}_{i\in\omega}$ that is dense in $U$.

We claim that there exists $h_i\in G$ for each $i$ such that $\suppe h_i=V_i$.
When a measure is not considred, this is clear from the definition of a good ball. So, let us consider the given measure $\mu$.
We endow $B^n(1)\cong V_i$ with the pull-back measure of a probability measure $\mu$ on $M$; that is, choosing a homeomorphism
$\phi_i\colon\inte B^n(1)\longrightarrow V_i$ and letting $A\sse B^n(1)$ be Borel measurable, we let $\mu^*(A)=\mu(\phi_i(A))$. Observe
that $\mu^*$ is the pushforward of (a rescaling of) Lebesgue measure by a homeomorphism. It is well-known that a compact Euclidean $n$--ball with $n\ge2$ admits a Lebesgue--measure preserving homeomorphism fixing only the
boundary and at most one interior point; see~\cite[Corollary 3]{Alpern1988} for instance.
By conjugation and extension by the identity, we have a measure--preserving homeomorphism of
$h_i$ of $M$ that fixes only the points outside $V_i$ and possibly a single interior point of $V_i$. This proves the claim.

Since we have \[\sup_{x}d(x,h_i(x))\le \diam V_i<1/i\] for all $i$,
the infinite product $g:=\prod_i h_i$ converges in $\Homeo(M)$,
and is isotopic to the identity.
We have that
\[
\suppe g = \oplus_i V_i = U.
\]
Hence, this map $g$ satisfies the conclusion.

    \end{proof}

 \subsection{First order logic}\label{ss:model theory}
Let us first note the measure-preserving homeomorphism groups of compact one--manifolds are highly restrictive.
\begin{prop}\label{prop:dim1}
For each compact connected one--manifold $M$,
there exist a group theoretic formula $\phi_M^{\vol}$ such that
when $(N,G)\in\cM_{\vol}$,
we have that \[ G\models \phi_M^{\vol} \] iff $N$ and $M$ are homeomorphic.
\end{prop}
\begin{proof}
Since $\Homeo_{\mu}(I)\cong\bZ/2\bZ$, the group theoretic sentence $\phi_I^{\vol}$ stating that there are at most two elements in the group is satisfied by a pair $(N,G)\in\cM_{\vol}$ iff $N\cong I$.
Since $\Homeo_{\mu}(S^1)$ contains the abelian group $\Homeo_{0,\mu}(S^1) \cong \on{SO}(2,\bR)$ as the index--two subgroup, a pair of the form $(S^1,G)\in\cM_{\vol}$ satisfies the sentence \[\phi_{S^1}^{\vol}:=(\forall\gamma_1,\gamma_2)\gamma_1\gamma_2^2\gamma_1^{-1}\gamma_2^{-2}=1]\wedge\neg\phi_I^{\vol}.\] Moreover, if $(N,G)\in\cM_{\vol}$ with $\dim N>1$, then $G$ is not virtually abelian and hence $G$ does not satisfy the above formulae.
\end{proof}

This proposition establishes the measure-preserving case with $\dim M=1$.
Our key strategy for all the other cases is to build a new language, which is powerful enough that it can distinguish a given manifold from all the other ones,
but which can still be ``interpreted'' to the language of groups. In order to do this, let us begin with  a brief review of the basic terminology from multi-sorted first order logic. Details can be found in~\cite{marker-book,tent-ziegler}
and also succinctly in~\cite{BH2017}.

On the syntactic side, a (multi-sorted, first order) \emph{language} $\LL$ is specified by \emph{logical symbols} and a \emph{signature}.
Logical symbols include quantifiers ($\forall$, $\exists$), logical connectives ($\wedge$, $\vee$, $\neg$, $\to$), the equality ($=$) and a  countable set of variables.
We often write auxiliary symbols such as parentheses or commas for the convenience of the reader.

A \emph{signature} consists of  \emph{sort symbols},
\emph{relation symbols} (also called as \emph{predicate symbols}),
\emph{function symbols} and
 \emph{constant symbols}.
For the brevity of exposition we often regard a function or constant symbol as a special case of a relation symbol.
An \emph{arity function} is also in the signature,
which assigns a finite tuple of sort symbols to each relation symbol. The arity function for each constant symbol is further required to assign only a single (i.e. 1--tuple of) sort symbol.

A \emph{(well-formed) $\LL$--formula} is a juxtaposition of the above symbols which is ``valid''; the meaning of this validity requires a recursive definition~\cite{marker-book}, although is intuitively clear.
For instance, if $P$ is a relation symbol with the arity value $(s,t)$ for some sort symbols $s$ and $t$
and if $x$ and $y$ are variables with sort values $s$ and $t$, respectively,
then $Pxy$ is a formula. We write $P(x,y)$ instead of $Pxy$ for the ease of reading.
By slight abuse of the terminology,
we often call the formula $P(x,y)$
as a \emph{relation} as well.
The \emph{language} $\LL$ specified by the above information is the collection of all formulae.
Unquantified variables in a formula are called $\emph{free}$, and a \emph{sentence} is a formula with no free variables.

On the semantic side, we have an $\LL$--\emph{structure} (or, an $\LL$--\emph{model}) $\mathcal{X}$, which is specified by a set $|\XX|$ called the \emph{universe}, a sort function $\sigma$ from $|\XX|$ to the set of sort symbols,
and an \emph{assignment}
that is a correspondence from each relation symbol $P$ to an actual relation $P^\XX$ among tuples of the elements in the universe.
For each sort symbol $s$, we call $s^\XX:=\sigma^{-1}(s)$  the \emph{domain} of $s$ in $\XX$.
It is required that the relation $P^\XX$ respects the arity value of $P$.
For instance, if $P$ is as in the previous paragraph, then $P^\XX$ will be a subset of $s^{\XX}\times t^{\XX}$.
A function symbol is assigned the graph of some function, and often written as a function notation such as $f(x)=y$.
A constant symbol is fixed as an element in the universe by an assignment.
An assignment (for relations) naturally extends to an assignment $\phi^\XX$ for each formula $\phi$.
We sometimes omit $\XX$ from $\phi^\XX$ when the meaning is clear.

For an $\LL$--formula $\phi$ with a tuple of free variables $\underbar x$,
and
for a tuple $\underbar a$ of elements in $|\XX|$,
we write $\XX\models \phi(\underbar a)$
if  $\phi^\XX$ holds after $\underbar a$
has substituted
$\underbar x$.
We define $\Th(\XX)$ as the set of all $\LL$--sentences $\phi$ such that $\XX\models \phi$.
Let $p,q\ge0$, and let $\underbar b$ be a $q$--tuple of elements of $|\XX|$.

A subset $A$ of $X^p$ is \emph{definable (by $\phi$) with parameters $\underbar b=(b_1,\ldots,b_q)$}
if for some formula $\phi$ with $p+q$ free variables, the set $A$ coincides with the set
\[
\XX(\phi;\underbar b)
:=\{\underbar a\in |\XX|^p\co \phi(\underbar a,\underbar b)\}.
\]
If $q=0$ we simply say $A$ is $0$--\emph{definable}, or \emph{definable};
in this case we denote the above set as $\XX(\phi)$.
We can now formalize the previously mentioned concept of ``interpreting''
a new language to an old one.

\bd\label{d:interpret}
Let $\LL_1$ and $\LL_2$ be languages.
Suppose we have a class $\XX$
of ordered pairs in the form  $(X_1,X_2)$ with $X_i$
 being an  $\LL_i$--structure.
We say $X_2$  is \emph{interpretable in $X_1$ uniformly for $(X_1,X_2)$ in $\XX$}
if the following hold.
\be[(i)]
\item\label{p:interpret1}
there exists a map from the set of $\LL_2$--formulae to the set of $\LL_1$--formulae denoted as $\psi\mapsto\hat\psi$; we call $\hat\psi$ as the \emph{interpretation} of $\psi$.
\item\label{p:interpret2} there exist $\LL_1$--formulae $\phi_{\mathrm{dom}}$ and $\phi_{\mathrm{eq}}$,
such that
for each $(X_1,X_2)\in\XX$
the set
 $X_1(\phi_{\mathrm{dom}})$
 admits an equivalence relation
 $X_1(\phi_{\mathrm{eq}})$.
\item\label{p:interpret}
for each $(X_1,X_2)\in\XX$,
we have a bijection
\[
\rho\co  |X_2|\to X_1(\phi_{\mathrm{dom}})/X_1(\phi_{\mathrm{eq}}),\]
naturally extending to a map between tuples,
such that  each $\LL_2$--formula $\psi$
and its interpretation $\hat\psi$ satisfy
\[
\rho(X_2(\psi))=
X_1(\hat\psi).
\]
\ee
\ed

\begin{rem}\label{rem:interpret}
\be
\item
We employ a multi-sorted language for convenience of exposition,
although a theory with finitely many sorts is  Morita equivalent to some single-sorted theory~\cite{BH2017}.
\item\label{p:interpret-rem}
In practice, in order to verify the interpretability we only need to consider a relation symbol $\psi$ in part (\ref{p:interpret}) rather than an arbitrary $\LL_2$--formula.
\item In various instances of this paper, it will be the case that $\LL_1\sse \LL_2$
and that the interpretation restricts to the identity on $\LL$.
As a consequence of such an interpretability, we will have that $\Th(\XX^*)$ is a {conservative extension} of $\Th(\XX)$ for each $(\XX,\XX^*)\in\CC$.
\ee
\end{rem}

The following lemma explains how the combination of Theorems~\ref{thm:interpret}
and~\ref{thm:iamM} implies Theorem~\ref{thm:main}.
\begin{lem}\label{lem:inter-models}
Suppose $\LL_1,\LL_2$ and $\XX$ are as in Definition~\ref{d:interpret} so that $X_2$ is  interpretable in $X_1$ uniformly for $(X_1,X_2)\in\XX$.
Let $(X_1,X_2)$ and $(Y_1,Y_2)$ be in $\XX$.
Then for each sentence $\psi$ belonging to $\Th(X_2)\setminus \Th(Y_2)$, the interpretation $\hat\psi$ belongs to $\Th(X_1)\setminus \Th(Y_1)$.
In particular,  if $X_1\equiv Y_1$, then $X_2\equiv Y_2$.
\end{lem}

\subsection{The AGAPE structure}\label{ss:sorts}
The fundamental universe that we work in will be the group of homeomorphisms of a manifold. Objects such as regular open sets, real numbers, points in the manifold, continuous functions, etc.~will all be constructed as definable equivalence classes of definable subsets of finite tuples of homeomorphisms.

The ultimate language we will work in will be called $\agape$, which stands for ``Action of a Group, Analysis, Points and Exponentiation''.
This language contains the following set of eight different sort symbols,
\[\{\bG,\ro,\bN,\PP(\bN),\bR,\PP^{1},\PP^{<\omega},\cont\},\]
in which $\PP^1$ is a subsort of $\PP^{<\omega}$.
The above sorts come with some symbols that are intrinsic to the sort (such as a group operation),
and others which relate the sorts to each other,
 as we spell out below.
There will be a countable set of variables for each sort, as is typically required.
We also describe an $\agape$ structure assigned to each pair $(M,G)$ in the class $\cM$ or $\cM_{\vol}$.
In this structure,
we give the ``intended'' choice of the {domain of each sort symbol.}

{\bf The group sort.}
The domain of the sort symbol $\bG$ will be the group $\cH$, under our standing assumption that $(M,G)\in\cM_{(\vol)}$. The non-logical symbols only relevant for this sort are
\[
1,\circ,\]
where we interpret $1$ as the group identity and $\circ$ as the group composition.
These symbols, along with variables, form the \emph{language of groups} $L^0_{\act}=L_\bG$. The group $\cH$ is regarded an $L_{\bG}$-structure $\act^0(M,G)=\act_{\bG}(M,G)$. We will usually not write
the $\circ$ symbol.

{\bf The sort of regular open sets.}
The domain of the sort symbol $\ro$ is the set $\ro(M)$ of the regular open sets in $M$.
The newly introduced symbols for this sort are
\[
\sse,\cap,\,^{\perp},\oplus,\varnothing,\top,\suppe,\appl.
\]
The symbol $\top$ means the manifold $M$ in the structure, and we will sometimes use $M$ to mean the symbol $\top$, although the symbol $M$ does not belong to the $\agape$ language.
By the natural interpretation as before, we have Boolean symbols \[\sse,\cap,\oplus,\,^\perp,\top, \varnothing\]
for the Boolean algebra $\ro(M)$.
We let the function symbol $\suppe$ mean the map $G\to \ro(M)$ defined as
\[g\mapsto \suppe g.\]
We then interpret $\appl$ so that for
$U\in\ro(M)$ we have
\[\appl(g,U)=g(U).\]
The symbols introduce so far (along with countably many variables for each sort) form the
\emph{language of action (of a group on a Boolean algebra)} $L^1_{\act}=L_{\mathbf{G},\ro}$.
The $L^1_{\act}$--structure described above on the universe $\cH\sqcup\ro(M)$ is denoted as $\act^1(M,G)=\act_{\bf G,\ro}(M,G)$.
We often abbreviate $\appl(g,u)$ for $g(u)$ if $g$ and $u$ are variables for the sort $\bG$ and $\ro$, respectively.

{\bf The sorts from the analysis}
The sort symbols
$\bN$ and $\PP(\N)$ are interpreted in the second order arithmetic:
    	\[\mathrm{Arith}_2=(\N,\mathcal{P}(\N),0,1,<,+,\times,\in,\subseteq).\]
We note the ambiguity of our notation that the sort symbols $\bN$ and $\PP(\bN)$ will be interpreted as the set of the natural numbers $\bN$ and its power set, respectively.
We also introduce a symbol $\#\pi_0$, interpreted so that
\[\#\pi_0(U)=k\]
means $U\in\ro(M)$ has $k$ connected components.
For the sort $\PP(\bN)$,
we introduce relation symbols $\{\in,\subseteq\}$ that are interpreted as membership and subset, respectively.

As is usual, we interpret the ordered ring of the real numbers:
\[\{0,1,+,\times,<,=_{\bR}\}\]
to the second order arithmetic.
These symbols will be interpreted naturally;
in particular, $=_{\bR}$ is interpreted as the equality between $k\in\bN$ and $r\in \bR$.
For the set $\bR$, we use the same sort symbol $\bR$.

Combining these symbols with $L^1_{\act}$, we obtain the language
$L^2_{\act}=L_{\bG,\ro,\bR}$.
An $L^2_{\act}$--structure
$\act^2(M,G)=\act_{\bG,\ro,\bR}$ is assigned to  each $(M,G)\in\cM_{(\vol)}$ having the universe
\[
\cH \sqcup\ro(M)\sqcup\bN\sqcup\PP(\bN)\sqcup\bR.
\]

{\bf The sorts $\PP^{<\omega}$ and $\PP^1$.}
The sort symbol $\PP^{<\omega}(M)$ means the set of all the finite subsets in $M$.
This sort contains a special subsort $\PP^1(M)$, the set of singletons; we naturally identify each element in the domain of $\PP^1(M)$ as a point in $M$.
By abuse of notation, the membership relation symbol $\in$ introduced above will have multiple meanings (depending on the context),
so that it also has the arity value $(\PP^1,\ro)$
and also the arity value $(\PP^1,\PP^{<\omega})$.
The subset relation symbol $\sse$ also has an additional meaning
with the arity $(\PP^{<\omega},\ro)$. The intended interpretations are clear.
The interpretation of points of the manifold will allow us to include symbols such as $\cl$ and $\fr$, the closure and frontier of a regular open set, together with membership relations into these sets. These symbols will simply be abbreviations for formulae which impose the intended meaning.
The function symbol $\appl$ has an additional meaning as well, so that its interpretation in some context is the naturally defined map
 \[\appl\colon G\times \PP^{<\omega}(M)\longrightarrow \PP^{<\omega}(M).\]
    abbreviate $\appl(g,p)$ by $g(p)$.
Combining these symbols with $L^2_{\act}$, we obtain the \emph{language of actions and points} denoted as $L^3_{\act}=L_{\bG,\ro,\bR,\PP^{\on{fin}}}$
and also the structure $\act^3(M,G)=\act_{\bG,\ro,\bR,\PP^{\on{fin}}}(M,G)$.

{\bf The sort $\cont$.} The domain of this sort symbol contains the set of continuous functions
\[C^0(B^n(1), \bR^{\ell}),\] for all $n,\ell\in\omega$.
If $n$ and $\ell$ are fixed, we will write $\cont_{n,\ell}$ for the corresponding subsort.
We can also interpret the formula
$\appl(f,x)=y$ when the sort value of $f$ is $\cont$,
and when $x$ and $y$ are tuples of variables assigned with the sort symbol $\bR$.
The omnibus language, combining all of the previous sorts and relevant symbols, is denoted by $L^4_{\act}=L_{\bG,\ro,\bR,\PP^{\on{fin}},\cont}$,
or simply as \emph{AGAPE}.
We have so far described the $\agape$--structure $\act^4(M,G)=\agape(M,G)$ corresponding to $(M,G)\in\cM_{(\vol)}$.

\subsection{Remarks on sorts, variables, and notation}
In dealing with the sorts in Subsection~\ref{ss:model theory}, we will distinguish notationally between variables referring to a particular sort and elements of that sort. For the convenience of the reader, we will record a table summarizing the notation. In general, we will write an underline to denote an arbitrary finite tuple of variables or objects.

    \begin{center}
    	\begin{tabular}{ | l | l | l | l | p{3cm} |}
    		\hline
    		Sort & variable & object  \\ \hline
    		Group elements & $\gamma$, $\delta$, $\underline\gamma$, $\underline\delta$ & $g$, $h$  \\ \hline
    		Regular open sets & $u$, $v$, $w$, $\underline u$, $\underline v$, $\underline w$ & $U$, $V$, $W$ \\ \hline
    		Natural numbers & $\alpha$, $\beta$, $\underline\alpha$, $\underline\beta$ & $k,m,n$\\ \hline
    		Sets of natural numbers & $\Lambda$, $\underline\Lambda$ & $A$  \\ \hline
    		Real numbers & $\rho$, $\sigma$, $\underline\rho$, $\underline\sigma$ & $r$, $s$ \\
    		\hline
    		Finite sets of points & $\pi$, $\underline\pi$, $\tau$, $\underline\tau$ & $p$, $q$, $T$ \\
    		\hline
    		Functions & $\chi$, $\theta$, $\underline\chi$, $\underline\theta$ & $f$ \\
    		\hline
    	\end{tabular}
    \end{center}

We will reserve the letters in this table for exclusive use as variables or objects of a particular sort.
In the ambient metalanguage from now on,
we will use $i,j\in\omega$ to denote indices. The symbols $M$ and $N$ will be reserved for manifolds, and $\{X,Y,Z\}$ will generally be reserved for definable sets.

\subsection{Interpreting action structures in homeomorphism groups}
Since the uniform interpretability (Definition~\ref{d:interpret}) is transitive,
the following proposition would trivially imply Theorem~\ref{thm:interpret}.
The proof of this proposition will span the next few sections.

\begin{prop}\label{prop:induct}
For each $i=0,1,2,3$,
and uniformly for $(M,G)\in\cM_{(\vol)}$,
the $L^{i+1}_{\act}$--structure $\act^{i+1}(M,G)$ is interpretable in
the $L^{i}_{\act}$--structure $\act^{i}(M,G)$.
\end{prop}

 A powerful theorem of Rubin~\cite{Rubin1989,Rubin1996} states that
    if two isomorphic groups $G_1$ and $G_2$ act locally densely on perfect, locally compact Hausdorff spaces $S_1$ and $S_2$ respectively,
    then there exists a homeomorphism $S_1\longrightarrow S_2$ that is equivariant with respect to the given actions.
    This theorem can be used to prove various \emph{reconstruction theorems}, by which we mean the
    group isomorphism types greatly restrict the homeomorphism types of spaces on which the groups
    can act nicely. See~\cite{KK2021book} for comprehensive references on this, especially regarding diffeomorphism groups.

    The key step in the proof of Rubin's theorem can be rephrased as follows. We emphasize that the formulae below are independent of the choice of the group $G$ or the space $S$.

\begin{thm}[Rubin's Expressibility Theorem, {cf.~\cite{Rubin1996}}]\label{t:express}
There exist first order formulae \[ \subseteq(\gamma_1,\gamma_2),\quad \appl(\gamma_1,\gamma_2,\gamma_3),\quad\cap(\gamma_1,\gamma_2,\gamma_3), \quad\oplus(\gamma_1,\gamma_2,\gamma_3),\quad\perp(\gamma_1,\gamma_2)\] in the language of groups such that if $G$ be a locally moving group of homeomorphisms of a Hausdorff topological space $S$, then the following hold for all $g_1,g_2,g_3\in G$.
\be
\item
  	$\displaystyle
	G\models\sse(g_1,g_2)\Longleftrightarrow \suppe g_1 \sse \suppe g_2
    	\Longleftrightarrow g_1\in G[\suppe g_2]$.
    	\item
    	$\displaystyle
    	G\models\mathrm{appl} (g_1,g_2,g_3)\Longleftrightarrow \appl(g_1, \suppe g_2) =\suppe g_3$.
    	\item
    	$\displaystyle
    	G\models \cap(g_1,g_2,g_3)\Longleftrightarrow \suppe g_1 \cap \suppe g_2 =\suppe g_3$.
    	\item
    	$\displaystyle
    	G\models \oplus (g_1,g_2,g_3)\Longleftrightarrow \suppe g_1 \oplus \suppe g_2 =\suppe g_3$.
    	\item
    	$\displaystyle
    	G\models \ext(g_1,g_2)\Longleftrightarrow \suppe g_1 =(\suppe g_2)^{\perp}$.
    	\ee
    \end{thm}
\begin{proof}
Parts (1) and (2) are given as Theorem 2.5 in~\cite{Rubin1989}; see also~\cite[Corollary 3.6.9]{KK2021book} for a concrete formula. The rests are clear from that the supremum in $\ro(M)$ is first order expressible in terms of the inclusion relations.
\end{proof}
Let $(M,G)\in\cM$ or $\cM_{\vol}$.
By Proposition~\ref{prop:full-support}, we have a surjection $G\to\ro(M)$ defined as $g\mapsto \suppe g$.
Since $G$ is locally moving on $M$,
Rubin's expressibility theorem implies that
the fiber $\{(g,h)\mid \suppe g = \suppe h\}$ of the surjection is definable,
and that the Boolean symbols and the function symbols $\appl$ and $\suppe$ have group theoretic interpretations; see also part (\ref{p:interpret-rem}) of Remark~\ref{rem:interpret}.
As a conclusion, we have the following, which means that Proposition~\ref{prop:induct} holds for the case $i=0$.
\begin{cor}\label{cor:interp-action}
Uniformly for $(M,G)\in\cM$ or $\cM_{\vol}$,
the $L_{\bf G,\ro}$--structure $\act_{\bf G,\ro}(M,G)$ is interpretable in
the group structure $G$.
\end{cor}

Corollary~\ref{cor:interp-action} can be summarized as saying that $\cH$ interprets the action structure of $\cH$ on the algebra of regular open sets, in a way that preserves the meaning of $\cH$.    This interpretation is uniform in the underlying pair $(M,G)$, and any formula in the language of $G$ and $\ro$ can be expressed entirely in $G$, since the formulae in Theorem~\ref{t:express} are independent of $M$. Henceforth, we will assume that we will work with the expanded language $L_{\act}^1=L_{\bG,\ro}$.

\subsection{First order descriptions of basic topological properties}\label{ss:top}
We write \[U_1\sqcup U_2=V\] when $V$ is the disjoint union of two sets $U_1$ and $U_2$.
\begin{lem}\label{lem:top-prop}
The following hold for $(M,G)\in\cM_{(\vol)}$.
\be
\item\label{p:full1}
For two regular open sets $U$ and $V$, we have that $\cH[U]=\cH[V]$ iff $U=V$.
\item\label{p:contained}
For each $U\in\ro(M)$, we have that
\[
G[U]=\{g\in G\mid g(V)=V\text{ for all regular open set }V\sse U^\perp\}.
\]
\item\label{p:pcnt}
An open subset is path-connected iff it is connected.
\item\label{p:cnt1}
Every connected component of a regular open set is regular open. More specifically, if a regular open set $W$ can be written as $W=U\sqcup V$ for some disjoint pair of open sets $U$ and $V$, then $U$ and $V$ are regular open and $W=U\oplus V$.
Moreover, we have $V=W\cap U^{\perp}$.
\item\label{p:group}
For disjoint pair $U,V$ of regular open sets, we have (i)$\Rightarrow$(ii)$\Rightarrow$(iii).
\be[(i)]
\item $U$ is connected, and $U\oplus V=U\sqcup V$;
\item Every $g\in \cH[U\oplus V]$ satisfies either $g(U)=U$ or $g(U)\cap U=\varnothing$;
\item $U\oplus V=U\sqcup V$
\ee
\item\label{p:cnt2}
    	Let $W$ and $U$ are regular open sets such that $U$ is connected and such that $U\sse W$.
    	Then $U$ is a connected component of $W$
    	iff $W=U\oplus V$ for some regular open $V$ that is disjoint from $U$
    	and every $g\in \cH[W]$ satisfies either $g(U)=U$ or $g(U)\cap U=\varnothing$.
    	\item\label{p:cnt1-2} The following are all equivalent for a regular open set $W$.
    	\be[(i)]
    	\item  $W$ is disconnected;
    	\item $W=U\sqcup V$ for some disjoint pair of nonempty regular open sets $U$ and $V$ such that $U$ is connected;
    	\item $W=U\oplus V$ for some disjoint pair of nonempty regular open sets $U$ and $V$, and every $g\in \cH[W]$ satisfies either $g(U)=U$ or $g(U)\cap U=\varnothing$;
    	\item $W=U\oplus V=U\sqcup V$ for some disjoint pair of nonempty regular open sets $U$ and $V$.\ee

    \item\label{p:full2}
    For two regular open subsets $U$ and $V$
    satisfying $U\cap V=\varnothing$,
    we have that
    $U\sqcup V= U\oplus V$
    if and only if
    each connected component of $U\oplus V$ is contained either in $U$ or in $V$.
    \ee
    \end{lem}
    \begin{proof}
    (\ref{p:full1})
    If
    $x\in U\setminus V$, then
    there exists some $h\in \cH[U]$
    satisfies $h(x)\ne x$; see \cite[Lemma 3.2.3]{KK2021book} for instance.
    In particular, we have that $h\in \cH[U]\setminus \cH[V]\ne\varnothing$. This proves the nontrivial part of the given implication.
We remark that the same statement holds without the assumption that $U$ and $V$ are regular open, under the extra hypothesis that $M\not\cong I$.

    (\ref{p:pcnt}) This part is clear from the fact that every manifold is locally path-connected.

    (\ref{p:cnt1})
    Whenever two open sets $U$ and $V$ are disjoint
    we have that $U^{\perp\perp}$ and $V^{\perp\perp}$ are also disjoint; see~\cite[Lemma 3.6.4 (4)]{KK2021book}, for instance.
    From
    \[
    W=U\sqcup V\sse U^{\perp\perp}\sqcup V^{\perp\perp}\sse U^{\perp\perp}\oplus  V^{\perp\perp} \sse W^{\perp\perp}=W,\]
    we see that $U$ and $V$ are actually regular open and $W=U\oplus V=U\sqcup V$. It is clear that  $V\cap \fr U=\varnothing$,
    which implies $V= W\cap U^{\perp}$.

    (\ref{p:group}) The implication (i)$\Rightarrow$(ii) is clear from that every setwise stabilizer of $g\in \cH[U\oplus V]$ permutes connected components of $U\oplus V$.

    For the implication (ii)$\Rightarrow$(iii), assume we have a point
    \[
    p_1\in
    (U\oplus  V)\setminus (U\cup V).\]
    Take a sufficiently small open ball $B$ around $p_1$ so that
    \[
    B\sse U\oplus V
    =
    \inte\cl (U\cup V)\sse\cl U\cup \cl V.\]
    Note also from \[p_1\not\in U=\inte \cl U\] that $B\not\sse\cl U$. Similarly, $B\not\sse\cl V$.
    This implies that we can choose distinct points
    \[p_2,p_3\in B\cap U\cap\inte M\]
    and $p_4\in B\cap V\cap\inte M$.

Since $G$ is $k$--transitive on $B\cap \inte M$ for all $k$,
we can find a $g\in G$ supported in $B$ satisfying
    $g(p_2)=p_3$ and $g(p_3)=p_4$;
    see also  Lemma~\ref{lem:transitive}.
    Then $g(U)$ is neither $U$ nor disjoint from $U$.

    Parts (\ref{p:cnt2}) and (\ref{p:cnt1-2}) are clear from the previous parts.

    (\ref{p:full2}) The forward direction comes from the observation that $(U,V)$ is a disconnection of $U\oplus V$. In order to see the backward direction we simply note from the hypothesis that each connected component of $U\oplus V$ is contained $U\sqcup V$,
    and that each connected component of $U\sqcup V$ is contained either in $U$ or in $V$.
    \end{proof}

    From Rubin's Expressibility Theorem (Theorem~\ref{t:express}) and Lemma~\ref{lem:top-prop}, we have the following straightforward
    consequences.

\begin{cor}\label{cor:basic-form}
There exist first order formulae in the language $L_{\bf{G},\ro}$ as follows:
\begin{enumerate}
\item A formula $\on{contained}(\gamma,u)$
such that
\[
\models\on{contained}(g,U)
\quad\textrm{if and only if }\suppe g\sse U.\]
\item
A formula $\on{conn}(u)$ such that \[\models \on{conn}(U)\quad\textrm{if and only if $U$ is connected.}\]
\item
    	A formula $\on{cc}(u,v)$ such that \[\models \on{cc}(U,V)\quad\textrm{if and only if $U$ is a connected component of $V$.}\]
\item
    	A formula $\on{ucc}(u,v)$ such that \[\models \on{ucc}(U,V)\quad\textrm{if and only if $U$ is a union of connected component of $V$.}\]
    	\item
    	For all $k\in\omega$, a formula $\#\on{cc}_k(u)$ such that \[\models \#\on{cc}_k(U)\quad\textrm{if and only if $U$ has exactly $k$ connected components.}\]
    	\item
    	A formula $\on{disj}(u,v)$ such that
	\[\models \on{disj}(U,V)\quad\textrm{if and only if $U\cap V=\varnothing$ and $U\oplus V=U\sqcup V$.}\]
    \end{enumerate}
    \end{cor}
We also denote $\gamma\in \bG[v]$ for the $L_{\bf G,\ro}$--formula
$\on{contained}{\gamma,v}$.
    Observe that we can choose
    	$$
    	\on{ucc}(u',u)\equiv\forall w\,\on{cc}(w,u')\rightarrow \on{cc}(w,u).
    	$$
    In light of Corollary~\ref{cor:basic-form}, we will be justified in using the abbreviation \[\forall u\in \pi_0(v)\,\phi(u)\] for the formula
    \[\forall u\, \on{cc}(u,v)\longrightarrow\phi(u).\] Occasionally we will drop parentheses for compactness of notation.

Using the above formula, we can distinguish the case that $\dim M=1$ among all compact connected manifolds.
\begin{cor}\label{cor:dim1}
For each compact connected one--manifold $M$,
there exist $L_{\bf G,\ro}$--formulae $\phi_M$ such that when $(N,G)\in\cM$,
 we have that \[ \act_{\bf G,\ro}(N,G)\models \phi_M \] iff $N$ and $M$ are homeomorphic.
\end{cor}
\begin{proof}
We let $\phi_I$ be the $L_{\bf G,\ro}$--formula expressing that for all pairwise disjoint, proper, nonempty regular open sets $U_1,U_2$ and $U_3$ the exterior of $U_i$ is disconnected for some $i$. This formula holds for $M\cong I$ since at least one of $\cl U_i$ does not intersect $\partial M$, and hence $U_i^\perp$ separates the two endpoints of $M$. It is clear that $\phi_I$ is never satisfied by any other compact connected manifolds.

We now suppose that $M$ is a compact connected manifold not homeomorphic to $I$. Then for all disjoint, proper, non-empty regular open sets $U$ and $V$ satisfying $U\oplus V=U\sqcup V$,
the set $M\setminus (U\oplus V)$ is disconnected. From Corollary~\ref{cor:basic-form}, we obtain the formula $\phi_{S^1}$ expressing that $M$ and $S^1$ are homeomorphic.
\end{proof}

By Proposition~\ref{prop:dim1} and Corollary~\ref{cor:dim1}, we establish Theorem~\ref{thm:main} for the case when $M$ is one--dimensional.
\emph{So from now on, we modify the definitions of $\cM$ and $\cM_{\vol}$, replacing these classes by subclasses where all the manifolds in consideration are of dimension at least two.}

\subsection{Further topological properties}
We will need several more general first order formulae to express basic topological properties of regular open sets. One of primary importance will be a formula which implies that a particular regular open set $U$ is contained in a collared ball inside of another regular open set $V$. This is not particularly difficult to state and prove in the class $\cM$, but is substantially harder in $\cM_{\vol}$. For the rest of this section, we will make a standing assumption that $(M,G)\in\cM_{(\vol)}$, and that the underlying structure is $\act_{\bG,\ro}(M,G)$.

\subsubsection{Transitivity and relative-compactness regarding good balls}\label{ss:more-topol}
We now use preceding results to find first order formulae that compare measures of regular open sets.
For the remainder of this subsection, we assume that $M$ is a connected, compact $n$--manifold with $n>1$, equipped with a Oxtoby--Ulam measure $\mu$.

    \begin{lem}\label{lem:leq-fo}
    There exists a formula $\vol_{\leq}(u_1,u_2,v)$ in the language $L_{\bf{G},\ro}$ such that for any triple $(U_1,U_2,V)$ with $U_1$
    and $U_2$
    connected and $U_1,U_2\subseteq V$, we have:
    \begin{enumerate}
    	\item
    	If $\mu(U_1)\leq \mu(U_2)$ then $\vol_{\leq}(U_1,U_2,V)$ holds.
    	\item
    	If $\vol_{\leq}(U_1,U_2,V)$ holds then $\mu(U_1)\leq\mu((\cl U_2)\cap V)$.
    \end{enumerate}
    \end{lem}
    \begin{proof}
Let us set \begin{align*}
    \vol_{\leq}(u_1,u_2,v)\equiv&
    (\forall w_0\ne\varnothing,\exists w_1)[w_1\sse u_1\wedge
    \on{conn}(u_1\cap w_1^{\perp})\wedge \\ &
    	(\forall \gamma\in  \bG)[
    	\gamma(w_0)\not\subseteq u_1\cap w_1^{\perp}]\wedge
      (\exists \delta\in  \bG[v])[\delta(w_1)\subseteq u_2]].
    \end{align*}

Suppose first that $\mu(U_1)\le \mu(U_2)$, and let $\varnothing\ne W_0\in\ro(M)$ be arbitrary.
By Lemma~\ref{lem:measure-ball}, we can find a good  ball $B\sse U_1\cap\inte M$ such that
\[
\mu(U_1)-\mu(W_0)<\mu(B)<\mu(U_1)\le\mu(U_2),
\]
and such that $U_1\setminus B$ connected.
Lemma~\ref{lem:measure-sum} furnishes  $g\in\Homeo_{0,\mu}(M,\partial M)[V]$ such that $g(B)\sse U_2$, but clearly there is no measure-preserving $h$ such that \[h(W_0)\subseteq U_1\setminus B=U_1\cap (\inte B)^\perp,\] and so $\vol_{\leq}(U_1,U_2,V)$ holds after setting $W_1:=\inte B$.

Now, suppose for a contradiction that $\vol_{\leq}(U_1,U_2,V)$ holds but that \[\mu(U_1)>\mu(V\cap \cl U_2).\] Let $W_0$ be the interior of a good ball in $M$ with measure $r_0<\mu(U_1)-\mu(V\cap \cl U_2)$.
It suffices to show that there is no witness $W_1$ as required by $\vol_{\leq}$.

If such a $W_1$ exists then by the condition on $\gamma$, we see again from Lemma~\ref{lem:measure-sum} that $\mu(U_1\cap W_1^\perp)\le r_0$.
Moreover, there is a group element $g\in \cH[V]$ such that $g(W_1)\subseteq U_2$, so that in fact \[g((\cl W_1)\cap V)\subseteq (\cl U_2)\cap V.\]
We then obtain
\[
r_0= \mu(W_0) \ge \mu(U_1\cap W_1^\perp) \ge \mu(U_1)-\mu(V\cap \cl W_1)
\ge \mu(U_1)-\mu(V\cap \cl U_2).
\]
This violates the choice of $r_0$.
    \end{proof}

    The foregoing discussion allows us to characterize when a regular open set $U$ is contained in a collared ball $B$ inside
    a regular open set $V$. There are separate formulae which apply in the measure-preserving case, and in the general case.

\begin{lem}\label{lem:rcb}
There exist first order formulae $\on{RCB}(u,v)$
and $\on{RCB}_{\vol}(u,v)$ satisfying the following.
\be\item\label{p:rcb1}
For $(M,G)\in\cM$,
and for nonempty connected regular open subsets $U,V$ of $M$,
\[\models \on{RCB}(U,V)\] holds if and only if $U$ is relatively compact in a good
ball $B$ in $V$.
\item\label{p:rcb2}
For $(M,G)\in\cM_{\vol}$,
and for nonempty connected regular open subsets $U,V$ of $M$,
\[\models \on{RCB}_{\vol}(U,V)\] holds if $U$ is relatively compact in a good ball $B$ in $V$,
and holds only if $U$ is relatively compact in $V$.
\ee
\end{lem}
    \begin{proof}
(\ref{p:rcb1})
We claim the following formula satisfies the conclusion.
\[\on{RCB}(u,v)\equiv(\forall w)[(w\subseteq v)\longrightarrow
(\exists\gamma\in  \bG[v])[\gamma(u)\subseteq w]].\]
Indeed, if $U$ is relatively compact in a good ball $B\subseteq V$ then for all $W\subseteq V$, there exists is a homeomorphism $g\in \cH[V]$ mapping $B$ onto an arbitrarily chosen collared ball in $W$; see Lemma~\ref{lem:transitive}. Since  $g(U)\subseteq g(B)\subseteq W$, we have that $\models\on{RCB}(U,V)$.
Conversely, assume $\models\on{RCB}(U,V)$.
We pick a collared ball $B_0$ in $V$
and set $W:=\inte B_0$. From the assumption we can find $g\in G[V]$ such that $g(U)\sse W$.
Then we have that
\[
U\sse g^{-1}(W)\sse g^{-1}(B_0)\sse V.
\]
In particular, $U$ is relatively compact in the collared ball $g^{-1}(B_0)$ in $V$.

(\ref{p:rcb2})
Let us set
\begin{align*}
\on{RCB}_{\vol}(u,v)\equiv & (\exists u')(u\subseteq u'\subsetneq v)\wedge(\forall w)[(\on{conn}(w)\wedge w\subseteq v
\wedge\\ &\neg\vol_{\leq}(w,u',v))\longrightarrow (\exists\gamma\in  \bG[v])[\gamma(u')\subseteq w]].
\end{align*}

In order to prove the forward direction, let us assume that $\on{RCB}_{\vol}(U,V)$ holds for some nonempty connected $U,V\in\ro(M)$. Let $U'$ be a witness for the existentially quantified $u'$ variable.
Since $U'\subsetneq V$, the Boolean subtraction $V\cap (U')^\perp$ is nonempty.
We now see that \[ \mu(V)-\mu(U')=\mu(V\cap (\fr U'\sqcup\ (U')^\perp))>\mu(V\cap\fr U').\] So, Lemma~\ref{lem:measure-sum} furnishes a good ball $B\sse V$ such that \[\mu(B)>\mu(U')+\mu(V\cap\fr U')=\mu(V\cap \cl U').\] By Lemma~\ref{lem:leq-fo}, we have that $\neg\vol_\leq(\inte B,U',V)$, and that some $g\in G[V]$ satisfies that $g(U')\sse \inte B$. It follows that \[\cl U\sse\cl U'\sse g^{-1}(B)\sse V,\] as desired.

For the backward direction, we pick a good ball $B$ satisfying $U\sse B\sse V$ and set $U':=\inte B$.
Let us consider an arbitrary connected regular open set $W\sse V$ satisfying $\neg\vol_\leq(W,U',V)$. From Lemma~\ref{lem:leq-fo} again, we see that $\mu(W)>\mu(U')=\mu(B)$. We may therefore find some $g\in G[V]$ such that $g(B)\sse W$. This shows that $\on{RCB}_{\vol}(U,V)$ holds.
\end{proof}

When using Lemma~\ref{lem:rcb}, we will write $\on{RCB}$ both in the case of the full homeomorphism group and the measure-preserving homeomorphism group, and suppress the $\vol$ from the notation.

\subsubsection{Detecting finiteness}\label{ss:fin}
Let us construct a first order formula describing the infinitude of connected components and apply this to describe certain topological properties regarding the boundary of a manifold.

\begin{prop}\label{prop:number-compact-infinite}
There exist first order $L_{\bG,\ro}$--formulae $\#_=(u,v)$ and $\inf(u)$ such that when $(M,G)\in\cM_{(\vol)}$, the following hold.
\be
\item
For all regular open sets $U$ and $V$ with finitely many connected components,
    	\[\models \#_=(U,V)\] if and only if $U$ and $V$ have the same number
    	of connected components;
\item
For all regular open set $U$, we have
\[\models \on{inf}(U)\] if and only if $U$ has infinitely many connected components.
\ee
    \end{prop}

\begin{proof}
We prove the items in order.
Let us avoid writing explicit formulae when the informal description is obviously first order.

{\bf Connected components.}
From the transitivity on good balls (of the same measures, in the measure preserving case) as in Lemma~\ref{lem:transitive}, we see that the following formula is the desired one.
\begin{align*}
    \#_=(u,v)\equiv (\exists u'\sse u,\exists v'\sse v)(\forall \hat u,\hat v)[(\on{cc}(\hat u, u)\rightarrow \on{conn}(u'\cap\hat u)
    \wedge u'\cap\hat u\neq\varnothing)
    \wedge\\
    (\on{cc}(\hat v, v)\rightarrow
    \on{conn}(v'\cap\hat v)
    \wedge v'\cap\hat v\neq\varnothing)\wedge (\exists\gamma)[\gamma(u')=v']].
    \end{align*}

    {\bf Infinitude of components.}
    We claim that a regular open set $U\in\ro(M)$ has infinitely many connected components if and only if the following hold for
    some $V\in\ro(M)$ and $g\in\cH$.
    \be[(i)]
    \item
    For each $\hat V\in\pi_0(V)$, we have that $\on{RCB}(\hat V,U)$, and that $\on{RCB}(g(\hat V),U)$;
    \item
    There exists $\hat U_0\in\pi_0(U)$ such that $\hat U_0\cap V$ is connected and nonempty and $\hat U_0\cap g(V)=\varnothing$;
    \item
    If $\hat U\in\pi_0(U)$ is distinct from $\hat U_0$, then either \[\hat U\cap (V\cup g(V))=\varnothing,\] or else
    $\hat U$ contains exactly one component of $V$ and exactly one component of $g(V)$.
    \ee

    It is straightforward to write down a formula defining sets $U\in\ro(M)$ satisfying these conditions, and we record this formula as $\inf(u)$.
    Observe that if $\models \inf(U)$ then $U$ has infinitely many components. Suppose the contrary, so that $U$ has components
    $\{U_0,\ldots,U_k\}$, with $U_0=\hat U_0$. We also then have that $V$ has $\ell+1\leq k+1$ components $\{V_0,\ldots,V_{\ell}\}$,
    with $V_0\sse U_0$. We then see that the components $\{V_1,\ldots,V_{\ell}\}$ must be permuted cyclically, or $U_i$ contains
    at least two components of $g(V)$ for some $i$. The first possibility is ruled out by the invertibility of $g$, and the second is ruled out
    by the conditions defining the formula. Thus, $U$ must have infinitely many components.

    Conversely, suppose that $U$ has infinitely many components $\{U_i\}_{i\in\omega}$. By passing to a subsequence and shrinking
    components if necessary, we may assume that \[U=\bigoplus U_i=\bigsqcup_i U_i,\] that each $U_i$ is an open ball in a single chart of
    $\R^n$ or the positive halfspace $\R^n_+$, that these open balls converge to the origin, and that the distance from
    the ball $U_i$ to the origin is a strictly decreasing function of $i$. By the Oxtoby--Ulam Theorem, we may
    assume that $\mu$ is just Lebesgue measure in this chart.

Recall our standing assumption that $\dim M\geq 2$.
We choose a point $p_0\in U_0$, and choose distinct points $p_i,q_i\in U_i$ for $i\geq 1$. Build a disjoint collection
    $\{\delta_i\}_{i\in\omega}$ of arcs such that $\delta_i(0)=p_i$ and $\delta_i(1)=q_{i+1}$, and such that the lengths of these
    arcs tend to zero as $i\to\infty$.
This is possible since each $U_i$ is an open ball
    and since the complement of a finite collection of disjoint arcs in $\bR^n$ is connected if $n\geq 2$. We choose a disjoint collection
    of compact topological balls $\{B_i\}_{i\in\omega}$ so that $B_i$ contains $\delta_i$ in its interior and so that $\diam(B_i)\to 0$ as
    $i\to\infty$.

By the topological transitivity of $\Homeo_{0}[\inte B_i]_\mu$ on the set of balls of the same volume (Corollary 2.2 in~\cite{LeRoux2014}),
    there exists a $h_i\in\cH[\inte B_i]$ sending a small ball $W_i$ about $p_i$ to a small ball about $q_{i+1}$.
    We choose these balls to be small enough so that they are relatively compact in $U_i$ for each $i$.
    Let \[g_k=\prod_{i\leq k} h_i,\]
    a definition which makes sense since $B_i\cap B_j=\varnothing$ for $i\neq j$.
    By construction, the set of homeomorphisms $\{g_k\}_{k\in\omega}$ is uniformly bounded. Moreover, this family is uniformly equicontinuous
    since $g_k$ is the identity outside $\cup_{i\in\omega} B_i$, and since on each $B_i$ the restriction of $g_k$ is either the identity or $h_i$.
    By Arzel\`a--Ascoli's Theorem, we may extract a limit $g$ which has the desired properties, and we may set \[W=\bigcup_{i\in\omega} W_i,\]
    and this completes the proof.
    \end{proof}

We remark that we may also test if a regular open set has finitely many components, and write \[\on{fin}(u)\equiv\neg\inf(u).\]

\subsubsection{Touching and containing the boundary}
Let us define the formula
    \begin{align*}
	    	\on{finint}(w,u)\equiv&(\exists w')[\on{fin}(w')\wedge(\forall w'_{0}\in\pi_{0}(w'))[\on{cc}(w'_{0},w)]\\
	    	&\wedge(\forall w_{0}\in\pi_{0}(w))[\on{cc}(w_{0},w')\leftrightarrow w_{0}\cap u\neq\emptyset]].
    	\end{align*}

It is clear from the formulation that \[\models\on{finint}(W,U)\] if and only if $U$ meets $W$ in finitely many components on $W$.
We can now state several formulae regarding the boundary of a given manifold. Recall again our context that $(M,G)$ belongs to either $\cM$ or $\cM_{\vol}$.

\begin{lem}\label{lem:touch}
There exist $L_{\bG,\ro}$--formulae as follows.
\be
\item\label{p:touch-partial}
A formula $\on{touch}_\partial(u)$ such that
\[\models \on{touch}_\partial(U)
\quad\textrm{iff }
\cl U\cap\partial M\neq\varnothing.\]
\item\label{p:contain-partial}
A formula $\on{contain}_\partial(u)$ such that
\[\models \on{contain}_\partial(U)
\quad\textrm{iff } \partial M\sse U.\]
\item\label{p:stab-partial}
A formula $\on{stab}_\partial(\gamma)$ such that
\[\models \on{stab}_\partial(g)
\quad\textrm{iff }
g(C)=C\text{ for each }C\in\pi_0(\partial M).\]
\ee\end{lem}
\begin{proof}
(\ref{p:touch-partial})
Let us set
\begin{align*}
\on{touch}_\partial(u)\equiv&(\exists u')[u'\subseteq u\wedge \inf(u')\wedge(\forall w)
[\on{RCB}(w,M)\longrightarrow \on{finint}(u',w)]].
\end{align*}

Suppose that $\cl U\cap\partial M\neq\varnothing$. Choose a sequence of points $\{p_i\}_{i\in\omega}$ in $U$ converging to
a point in $\partial M$, and choose small open balls $U_i\ni p_i$ in $U$ with pairwise disjoint closures and with radii tending to zero.
Let $U'$ be the union of these balls. Now, if $W$ fails to
satisfy $\on{finint}(U',W)$, then $W$ must meet infinitely many of the balls $U_i$, and so $\cl W\cap\partial M\neq\varnothing$. In
particular, $\neg\on{RCB}(W,M)$.

Conversely, suppose that $\cl U\cap\partial M=\varnothing$, and let $U'\sse U$
have infinitely many components $\{U_i\}_{i\in\omega}$. As in Proposition~\ref{prop:number-compact-infinite}, by shrinking components of
 $U'$ and passing to a subsequence, we may assume that each $U_i$ is an open ball,
that the sequence has shrinking radii and converges monotonically to the origin in an open chart in $\bR^n$. Moreover, the origin
in this chart lies in the interior of $M$, by assumption.

Thus, we may take $W$ to be a neighborhood of the origin in this chart, which then satisfies $\on{RCB}(W,M)$ and meets infinitely
many components of $U'$. Thus, $U'$ fails to witness $\on{touch}_\partial(U)$, and so $\on{touch}_\partial(U)$ does not hold.

(\ref{p:contain-partial})
Since $\partial M\setminus U= \cl\left(U^\perp\right)
\cap\partial M$,
we have that
$\partial M\not\sse U$
iff
$\on{touch}_\partial(U^\perp)$.
Hence, it suffices for us to set $\on{contain}_\partial(u)\equiv\neg\on{touch}_\partial(u^\perp)$.

(\ref{p:stab-partial})
We define \[\on{stab}_{\partial}(
\gamma)\equiv (\forall u,\hat u)[(\hat u\in\pi_0(u)\wedge\on{contain}_\partial(u)\wedge
\on{touch}_{\partial}(\hat u)\rightarrow \hat u\cap\gamma(\hat u)\neq\varnothing.\]

Suppose $U$ is a regular open set containing the boundary of $M$,
and let $\hat U\in\pi_0(U)$.
If $\models\on{touch}_{\partial}(\hat U)$, then
$\hat U$ must contain points of $\partial M$ in its closure. It follows
that $\hat U$ must contain at least one component of $\partial M$;
indeed, if $N\in\pi_0(\partial M)$ then a collar neighborhood $V$
of $N$ must be contained $U$, by a result of
Brown~\cite[Theorem 2]{Brown1962}. The set $V$ is connected
and meets $\hat U$, and if it also met $U\cap\hat U^{\perp}$ then
the connectedness of $V$ would be violated. Hence, if $\models\on{stab}_\partial(g)$ then setting $U$ to be a sufficiently small collar neighborhood of $\partial M$, we see that $g$ cannot permute the boundary components of $M$ nontrivially.

Conversely, if $g$ stabilizes each component of $\partial M$ then if $V$ is a collar neighborhood of a component $N\in\pi_0(\partial M)$,
we have $g(V)\cap V\neq\varnothing$. Since each component $\hat U$
of a set $U$ containing $\partial M$ that meets $\partial M$ contains
such a collar neighborhood $V$, we have
    $\models\on{stab}_\partial(g)$.
\end{proof}

For a later use, we will define
\[
G_\partial=\{g\in G\mid \act_{\bG,\ro}(M,G)\models \on{stab}_\partial(g)\},\]
which is clearly a definable subgroup of $G$.

\section{Interpretation of arithmetic}\label{sec:arith}
The goal of this section is to prove the case of $i=1$ in Proposition~\ref{prop:induct}, establishing that the group $G$
interprets second order arithmetic and analysis uniformly for $(M,G)\in\cM_{(\vol)}$.

\subsection{Second order arithmetic}\label{ss:second-arith}
We begin by interpreting second order arithmetic first.
The proof is achieved by interpreting second order arithmetic in $\act_{\bf G,\ro}(M)$ with a definable parameter space, and then eliminating parameters.
We begin by interpreting first order arithmetic as the quotient of the collection of all sets in $\ro(M)$ with finitely many connected components, i.e.~the collection of solutions of the formula $\on{fin}(u)$ by the equivalence relation consisting defined by the formula $\#_{=}(u,v)$, relating two such sets if they have the same number of connected components.

In the discussion below, all regular open sets under consideration will be assumed to have finitely many connected components. We break up the proof into several steps, interpreting each of the symbols in the language one at a time.

    	{\bf Addition.}
    	We need to define a ternary formula $\#_{+}(u,v,w)$ such that \[\models\#_{+}(U,V,W)\quad \textrm{if and only if}\quad \#(W)=\#(U)
    	+\#(V).\]
Recall $\on{ucc}(U',U)$ means $U'$ is a  union of connected components of $U$.
We have that
    	$$
    	\#_{+}(u,v,w)\equiv(\exists w_{0},w_{1})[\on{ucc}(w_{0},w)\wedge \on{ucc}(w_{1},w)\wedge \#_{=}(w_{0},u)\wedge
	 \#_{=}(w_{1},v)\wedge (w_0\cap
    	w_1=\varnothing)]
    	$$
    	satisfies the required property.

    	{\bf Multiplication.}
    	We also need to define a ternary formula $\#_{\times}(u,v,w)$ such that
    	\[\#_{\times}(U,V,W)\quad \textrm{if and only if}\quad \#(W)=\#(U)\cdot\#(V).
    	\]
    	As with the formula $\on{ucc}$, it is trivial to write a formula $\on{subcc}(u',u)$ which holds for $(U',U)$ if and only if each
    	connected component of $U'$ is contained in some connected component of $u$ and then we can simply write
    	$$
    	\#_{\times}(U,V,W)\equiv(\exists w')[\#_{=}(w,w')\wedge \on{subcc}(w',u)\wedge(\forall \hat{u})\,\,\on{cc}(\hat{u},u)
	\rightarrow\#_{=}(\hat{u}\cap w',v)].
    	$$

    	{\bf Interpreting $\bN$ with parameters I: defining the parameter space.}
    	The previous discussion suffices to interpret first order arithmetic, since $\#_+$ and $\#_{\times}$, and $\on{ucc}$ suffice to define
    	the successor function and order relation.
    	However, in order to be able to quantify over subsets of the natural numbers we need to be able to do two things.
    	\begin{itemize}
    		\item Provide a bijection, definable with parameters, between the cardinality classes given by $\#_{=}$ and the connected components of a set $U$ with infinitely many connected components. Subsets of $\N$ are then in bijection with unions of connected components of $U$, i.e. sets $U'$ satisfying $\on{ucc}(U',U)$.
    		\item Show that the definition can be taken to be uniform and yields the same result for any choice of the
		parameter (which includes $U$) within certain $\varnothing$-definable set $Y$ is irrelevant.
    	\end{itemize}

    	\newcommand{\scc}[0]{\subset_{cc}}

    	We will start by giving $Y\subseteq RO^{2}(M)$. We declare a pair $(U,V)$ to be an element of $Y$ if
    	both $U$ and $V$ have infinitely many connected components, i.e.~$\inf(u)\wedge \inf(v)$ holds for $(U,V)$,
    	and if the following list of conditions is satisfied. It is clear that all of them are definable in the language of actions.

    	\begin{enumerate}
    		\item  $\on{conn}(U\oplus V)$.
    		\item For all $\hat{U}\in\pi_0 U$ and $\hat{V}\in\pi_0V$ the intersection $\hat{U}\cap \hat{V}$ is either empty or connected.

    		\item
    		\label{point 3}Any $\hat{V}\in\pi_0V$ intersects exactly two connected components of $U$.

    		\item
    		There exists a unique $\hat{U}_0\in\pi_0 U$ such that $\hat{U}_{0}\cap \hat{V}\neq\varnothing$ for exactly one $\hat{V}\in\pi_0 V$.
    		That is
    		$$\models\exists!\, \hat{w}\,\,\on{cc}(\hat{w},U)\wedge \on{int}_1(\hat{w},V),\,\,\,\text{where}$$
    		\begin{align*}
    			 \on{int}_1(\hat{w},v):= \on{cc}(\hat{w},U)\wedge \exists! \,\hat{v}\,\, \on{cc}(\hat{v},V)\wedge
    			\hat{v}\cap \hat{w}\neq\varnothing.
    		\end{align*}
    		\item
    		For all $\hat{U}\in\pi_0 U$ distinct from $\hat{U}_{0}$ and for any $\hat{U}\in\pi_0 U$, there are exactly two distinct
    		$\hat{V}_1,\hat{V}_2\in\pi_0 V$ such that $\hat{U}\cap \hat{V}_i\neq\varnothing$.
    		\item
    		For any $\hat{V}\in\pi_0 V$ we have $U\oplus (V\cap \hat{V}^{\perp})$ has exactly two connected components, i.e. \[\models\forall \hat{v}\,\,\on{cc}(\hat{v},V)\rightarrow \on{cc}_{2}(U\oplus (V\cap \hat{v}^{\perp})).\]
    	\end{enumerate}

    	The preceding conditions collectively define $Y$.

    	Observe that after replacing $U$ and $V$ by subsets that are relatively compact,
    	we may assume that $\hat{U}\oplus \hat{V}=\hat{U}\sqcup \hat{V}$
    	whenever $\hat{U}\cap \hat{V}=\varnothing$.
    	Precisely, if $\phi(u,v)$ is the formula defining $Y$, we let $Z$ be the set definable by the formula
    	\begin{align*}
    		\psi(u,v)\equiv\phi(u,v)\wedge(\exists u',v'\,\phi(u',v')\wedge \on{subcc}!(u,u')\wedge \on{subcc}!(v,v') \\(\forall \hat u_0,\hat v_0)[
    		(\on{cc}(\hat u_0,u)\longrightarrow \on{RCB}(\hat u_0,u'))\wedge (\on{cc}(\hat v_0,v)\longrightarrow \on{RCB}(\hat v_0,v'))]),
    	\end{align*}
    	where here  $\on{subcc}!(u,v)$ means that every connected
    	component of $v$ is contains a unique connected component of $u$.
	 Here, we are abusing notation slightly with the formulae $\on{RCB}$
    	since $U'$ may not be connected; we simply extend the definition to mean $\on{RCB}$
    	for the hatted variable and the primed variable within the connected component containing the hatted variable.

    	{\bf Interpreting $\bN$ with parameters II: the interpretation.}
    	We retain the notation from the definition of the parameter space, and we fix $(U,V)\in Z$.
    	For arbitrary $\hat{V}\in\pi_0 V$, we have that $U\oplus (V\setminus \hat{V})$ consists of two components
    	$U_1^{\hat{V}}$ and $U_2^{\hat{V}}$.

    	Without loss of generality, $\hat{U}_{0}$ is a component of $U\cap U_1^{\hat{V}}$.
    	We claim that \[U\cap U_1^{\hat{V}}\] contains finitely many connected components,
    	and that for any $k\in\omega\setminus\{0\}$ this number is precisely $k$ for a unique $\hat{V}\in\pi_0 V$.

    	Indeed, build a graph $\Gamma$ by taking one vertex for every component of $U$ and every
    	component of $V$, and putting an edge between
    	two vertices if the corresponding regular open sets have nonempty intersection. Observe that a path in $U\oplus V$ gives rise to a path in
    	$\Gamma$ in a canonical way, and thus the components of $U\oplus (V\setminus \hat{V})$ are in canonical bijection with those of the graph
    	$\Gamma'$ obtained by deleting the vertex of $\Gamma$ that corresponds to $\hat{V}$. Clearly, $\Gamma$ is a semi-infinite ray, whence the claim.

    	Let $k\in\omega$.
    	If $\#(U\cap U_1^{\hat{V}})=k+1$ then we write \[U_k:=U\cap U_1^{\hat{V}},\quad V_k=\hat{V}\] for this particular component $\hat{V}$,
    	and we write $\hat{U}_k$ for the unique component of
    	$U_k$ that meets $V_k$.
Let $\pi_0(U)$ denote the definable set $$\{W\,|\,\models \on{cc}(W,U)\}\subseteq\ro(M).$$
	The discussion above yields naturally an interpretation with parameters of
	$(\N,+,\times)$ and therefore of $(\N,0,S,<,+,\times)$ in $\act^1(G,M)$ with underlying map
    	\[\iota_{U,V}\colon\ro(M)\longrightarrow \bN , \quad \hat{U}_{k}\mapsto k.\]
    	Checking that the pull-back of the graphs of $+$ and $\times$ in $\N$ are the set of solutions in
    	$\pi_0(U)^{3}$ of formulas $+(u_1,u_2,u_3)$ and $\times(u_1,u_2,u_3)$ in $\act^1(G,M)$ over $(U,V)$ is now easy.

    	It is clear that one can find a formula with parameters $\on{first}(\hat{u},U,V)$, which is defined uniformly in $(U,V)$,
    	that holds for $W$ if and only if $W=\hat{U}_{0}$, as defined above. Likewise, the formula with parameters
    	\begin{align*}
    		\on{corr}(\hat{u},w,U,V)\equiv& \exists \hat{v}\,\,\on{cc}(\hat{v},V)\wedge \hat{v}\cap \hat{u}\neq \emptyset\wedge\exists w'\,\,\on{first}(w',U,V)\wedge\\
    		& \on{cc}(w,U\oplus(V\cap \hat{v}^{\perp})) \wedge\hat{u}\subseteq w\wedge w'\subseteq w
    	\end{align*}
    	holds for $(\hat{U}_{k},W)\in\ro(M)^{2}$ if and only if $W=U_{k}$.

    	Therefore, we may write
    	\begin{align*}
    		+(u_{1},u_{2},u_{3})\equiv&\exists w,u'_{1},u'_{2},u'_{3}\,\,\on{first}(w,U,V)\wedge\bigwedge_{i=1}^{3}\on{corr}(u_{i},u'_{i})\wedge\\
    		&\#_{+}(u'_{1}\cap w^{\perp},u'_{2}\cap w^{\perp},u'_{3}\cap w^{\perp}),
    	\end{align*}
    	and the formula $\times(u_{1},u_{2},u_{3})$ can be defined similarly using $\#_{\times}$ instead of $\#_{+}$.\\

    	{\bf Interpreting arbitrary subsets of $\bN$.}
    	We will now finish interpreting second order arithmetic
    	\[\mathrm{Arith}_2=(\N,\mathcal{P}(\N),0,1,<,+,\times,\in,\subseteq),\] with parameters.

    	Let $\pi_0(U)^*$ the collection of all those regular open sets that are unions of connected components
    	of $U$. As seen above, this is definable by a formula $\on{ucc}(u,U)$. Since the union of any collection of connected components of a regular open set is again regular, we have a canonical bijection:
    	\[\iota^*_{U,V}\colon \pi_0(U)^*\longrightarrow \mathcal P(\bN) \quad \quad
    	U_P:=\bigoplus_{k\in P} \hat{U}_k \mapsto P.\]

Notice that
    	$$k\in P  \quad \text{if and only if} \quad \iota^{-1}_{U,V}(k)=\hat{U}_{k}\subseteq U_{P}=(\iota_{U,V}^{*})^{-1}(P),$$ so the pair
    	$(\iota_{U,V},\iota^{*}_{U,V})$ gives an interpretation of $\mathrm{Arith}_2$ in  $\act(G,M)$,
    	over the parameter $(U,V)$. \\

    	{\bf Elimination of parameters.}
    	Finally, we wish to find an interpretation of $\mathrm{Arith}$ without parameters.
    	In order to do this, we show that the interpretations of arithmetic obtained
    	from different choices of parameters $(U^1,V^1)$ and $(U^2,V^2)$ are canonically equivalent in a definable way.
More precisely,
    	we need to show the existence of formulae \[\on{eqint}(\hat{u}_{1},\hat{u}_{2},u_{1},v_{1},u_{2},v_{2}),\quad
    	\on{eqint}^{*}(\hat{u}_{1},\hat{u}_{2},u_{1},v_{1},u_{2},v_{2})\] such that
    	for any \[(U_{1},V_{1}),\,(U_{2},V_{2})\in Y,\quad \hat{U}_{1}\in \pi_0(U_{1}),\,\hat{U}_{2}\in \pi_0(U_{2}),\]
	the intersection of the definable sets
    	\begin{align*}
    		\{(\hat{U}_{1},\hat{U}_{2})\in \pi_0(U_1)\times \pi_0(U_2)\,|\,\models \on{eqint}(\hat{U}_{1},\hat{U}_{2},U_{1},V_{1},U_{2},V_{2})\}\\
    		\{(U_{1}^*,U_{2}^*)\in \pi_0(U_{1})^*\times \pi_0(U_{2})^*\,|\,\models \on{eqint}^{*}(\hat{U}_{1},\hat{U}_{2},U_{1},V_{1},U_{2},V_{2})\}
    	\end{align*}

	define bijections
    	\[f^{U_{1},V_{1}}_{U_{2},V_{2}}:\pi_0(U_1)\to \pi_0(U_2)\quad \textrm{and} \quad
    	g^{U_{1},V_{1}}_{U_{2},V_{2}}:\pi_0(U_{1})^*\to \pi_0(U_{2})^*\] respectively, compatible with the interpretations corresponding to
    	$(U_{1},V_{1})$ and $(U_{2},V_{2})$;
	that is, we require
    	$$
    	\iota_{U_{2},V_{2}}\circ f^{U_{1},V_{1}}_{U_{2},V_{2}}=\iota_{U_{1},V_{1}} \quad\quad \iota^{*}_{U_{2},V_{2}}\circ g^{U_{1},V_{1}}_{U_{2},V_{2}}=\iota^{*}_{U_{1},V_{1}}.
    	$$
    	This can be achieved simply by letting:
    	\begin{align*}
    		\on{eqint}(\hat{u}_{1},\hat{u}_{2},u_{1},v_{1},u_{2},v_{2})\equiv
    		& \exists u'_{1},u'_{2}\,\,\bigwedge_{i=1}^{2}\on{corr}(\hat{u}_{i},u'_{i},u_{i},v_{i})\wedge\#_{=}(u'_{1},u'_{2}),
    	\end{align*}
    	and then choosing \[\on{eqint}^{*}(\hat{u}_{1},\hat{u}_{2},u_{1},v_{1},u_{2},v_{2})\] in the obvious way, using the
    	interpretation of the $\in$ symbol.

  \subsection{Analysis}
The interpretation of $\bR$ is now standard. From $\bN$, we interpret $\bZ$, together with addition, multiplication, and order, by imposing a suitable definable equivalence relation on a suitable definable subset of $\bN^2$. We similarly
    interpret $\bQ$ by imposing a suitable definable equivalence relation on a definable subset of $\bZ\times \bZ$.
Thus, we may assume that $\act_{\bG,\ro,\bN,\mathcal{P}(N)}$ is expanded to interpret the sorts $\bZ$ and $\bQ$. We define $\bR$ together with addition, multiplication, and order via Dedekind cuts of $\bQ$, is interpretable because of our access to $\PP(\bN)$. Finally, we have canonical identifications of \[\bN\subseteq\bZ\subseteq\bQ\subseteq\bR,\] wherein we set $=_{\bR}$ to be the relation identifying natural numbers with their images under this sequence of inclusions. In the sequel, we will simply talk about natural numbers,
integers, or rationals as elements of $\bR$ without further comment. This completes the proof of Proposition~\ref{prop:induct} for the case $i=1$.
The expanded language containing action structures, second order arithmetic, and analysis will be written $\act^2=\act_{\bG,\ro,\bR}$.

\section{Interpretation of points}\label{sec:points}
We now wish to be able to talk about points of $M$ more directly, and prove Proposition~\ref{prop:induct} for the case $i=2$.
This will be crucial in later parts of the proof of the main result.
  Rubin~\cite{Rubin1989}
  accesses points in a manifold by considering certain filters in the collection of regular open sets, an approach we wish to
  avoid in order to stay within the first order theory of $\cH$.

  \newcommand{\lst}[0]{\on{St}^{\lim}}
  \subsection{Encoding individual points}
    We begin by encoding singleton subsets of $M$ by certain equivalence classes of regular open sets. We will establish the following fact.

        \begin{thm}\label{thm:points}
Let $(M,G)\in\cM_{(\vol)}$.
There exists a definable subset $X\sse \Ro(M)$ and a definable equivalence relation $E$
    	on $X$, and a canonical bijection \[\pmb{p}\colon X/E \longrightarrow \PP(M).\]
     Moreover, there is a definable function
	\[\appl\colon \cH\times X/E
    	\longrightarrow X/E\] such that for all $p,q\in \inte M$ and $g\in\cH$, we have \[g(p)=q\quad\textrm{if and only if}\quad \appl(g,\pmb{p}^{-1}(p))=\pmb{p}^{-1}(q),\]
    	and a definable relation $\epsilon\sse X/E\times\ro(M)$ such that for all
    	$p\in  M$ with $\pmb{p}^{-1}(p)=[W]\in X/E$, we have \[([W],U)\in \epsilon\quad \textrm{if and only if}
    	\quad p\in U.\]
    \end{thm}

    We will say that each element $[W]_E\in X/E$ \emph{isolates} a unique point of (the interior of) $M$.
    Combining Theorem~\ref{thm:points} with our interpretation of second order arithmetic, we obtain the following:

    \begin{cor}\label{cor:include-points}
For $M$ arbitrary, there exists an expansion by definitions of $\cH(M)$ which interprets the
	sort $\mathcal P(M)$.
    \end{cor}

We introduce a few definitions regarding $U\in\ro(M)$.
We call each point in the set
\[
\fr U\setminus\left(\bigcup_{\hat U\in\pi_0(U)} \fr \hat U\right)
\]
as an \emph{essential accumulation point} of $U$.
In the case where $U$ has infinitely many connected components,
we say $U$ \emph{converges} to a point $p\in M$ if for all neighborhood $W\in\ro(M)$ of $p$, the set
\[
\{ \hat U\in\pi_0(U)\mid \hat U\not\sse W\}
\] is finite.

 A regular open set $U$ with infinitely many components
 is \emph{scattered}
if for all $\hat U\in\pi_0(U)$     we have    	\[\cl \hat U\cap\cl (U\setminus \hat U)=\varnothing.\]
Let us make the following two observations:
\begin{obs}
    	\label{o: convergence and essential accumulation}
     Let $U$ be a scattered regular open set. If $p$ is the unique
     essential accumulation point of $U$, then $U$ converges to $p$.
     The converse is also true.
    \end{obs}

    Consider the formula:
    $$
    \on{scattered}(u)\equiv \inf(u)\wedge(\forall u_{0}\in\pi_{0}(u))[\on{RCB}(u_{0},u^{\perp}\oplus u_{0})]
    $$
    Clearly $\models \on{scattered}(U)$ implies that $U$ is scattered.
    It is now a trivial task to write a formula $\on{cof}(u,v)$
    that holds for $(U,V)$ if and only if:
	  \begin{itemize}
     \item $U\subseteq V$
     \item $\models \on{scattered}(U)$
		 \item each connected component of $V$ contains at most one connected component of $U$
	  \end{itemize}

    The following is also a straightforward consequence of the
    compactness of $M$.
    \begin{obs}
       \label{o: convergence and cofinality}
       If $U\in\ro(M)$ is scattered with a single
       essential
       accumulation point $p$, then $p$ is also the unique essential accumulation point of any $U'\in\ro(M)$ satisfying $\on{cof}(U',U)$.

       For any scattered $U\in\ro(M)$
       and any essential accumulation point $p$ of $U$, there is a $U'\in\ro(M)$ such that \[\models \on{cof}(U',U)\]
       and such that $U'$ converges to $p$.
    \end{obs}

  Now, consider the formula
  $$\on{gstab}(\gamma,u)\equiv (\exists w)[\on{cof}
  (w,u)\wedge\gamma\in  G[w^{\perp}]].$$

We abbreviate $\on{gstab}(\gamma,u)$ by
$\gamma\in \lst(u)$, which stands for \emph{limit stabilizer}
and avail ourselves of quantifiers bounded in terms of the
latter expression.

   Finally, consider the formula $\on{sep}(u,v)$ given by the following expression.
    \begin{align*}
    \on{sep}(u,v)\equiv(\forall\gamma)[\on{stab}_\partial(\gamma)\rightarrow (\exists \gamma_1,\gamma_2\in \lst(u))(\exists\delta\in\lst(v))[ \gamma_1\delta\gamma_2=\gamma^2]].
    \end{align*}

    \begin{lem}\label{lem:sep}
    Suppose that $U$ and $V$ are open sets converging to points $p$ and $q$ respectively. Then $\on{sep}(U,V)$ holds if and only if $p\neq q$,
    \end{lem}
   \begin{proof}
  	  By virtue of the first claim of Observation \ref{o: convergence and cofinality} if $p=q$ then all elements of both
  	  $\lst(U)$ and $\lst(V)$ must fix $p$ and thus $\on{sep}(U,V)$ cannot possibly hold.

  	  Assume now that $p\neq q$ and let $g\in G_{\partial}$.
     Write $p'=g^2(p)$. Assume first that $p'\neq q$. Since $U$ converges to $p$ and $V$ converges to $q$, there exist $U'$ and $V'$ such that
     \[\models \on{cof}(U',U),\quad \models \on{cof}(V',V);\] moreover,
     we may assume that there are disjoint closed sets $F$ and $K$
     such that  $U'\subseteq F$ and $V'\subseteq K$,
     and which satisfy the following:
  	  \begin{enumerate}
  	  	\item $K\cap(F\cup g^2(F))=\emptyset$
  	  	\item each $B\in\{F,K\}$ is the image of a closed $n$-ball which either:
      \begin{enumerate}
      \item
      Is a good ball contained in $\inte M$;
      \item
      Meets $\partial M$ in an $(n-1)$-dimensional disk, and satisfies $M\cong M\setminus B$.
      \end{enumerate}
  	  \end{enumerate}

Any group element $h\in
     G_{\partial}$ fixing $K$ automatically lies in $\lst(V)$.
  	  Since $g\in G_{\partial}$, there exists an $h\in
     G_{\partial}$ fixing $K$ such that
  	  $(hg^2)(F)=F$. If $hg^2$ preserves orientations on $F$ then we can find an isotopy from this map to the identity on $F$ avoiding $K$, by the Stable Homeomorphism Theorem~\cite{Kirby1969}.

We claim that there exists some $h_1\in\lst(V)$ such that $h_1hg^2$ preserves orientations on $F$. From this claim, we will deduce that $h_1hg^2\in\lst(U)$.
In the case where $M$ is orientable, the homeomorphism $g^2$ is orientation preserving. So, $(hg^2)\restriction_F$ can be chosen to be the identity; that is, we can set $h_1=1$. Alternatively, one can consider a lift to the orientation double cover of $M$ and use the deck transformation to find $h_1$.

Suppose now that $M$ is nonorientable. If $p\in \inte M$, then one can use a neighborhood of an orientation--reversing path based at $p$ that avoids $K$, and push $F$ along this path to find the desired $h_1$.

It only remains to consider the case that $M$ is nonorientable and $p$ belongs to some component $ \partial_0$ of $\partial M$. If $\partial_0$ is orientable, then $g^2$ preserves orientations on $\partial_0$ and hence, $hg^2$ cannot reverse orientations of $F$. So, we assume $\partial_0$ is nonorientable.
Then we can use a similar trick as above by pushing $F$ along an orientation--reversing path on $\partial _0$ based at $p$.
It follows that $g^2\in\lst(V)\lst(U)$.

  	  We may therefore assume that $g^2(p)=q$.
     Consider then an element $h'\in\lst(U)$ such that $h'(q)\neq q$. The previous argument shows that \[g^2\in (h')^{-1}\lst(V)\lst(U)\subseteq\lst(U)\lst(V)\lst(U),\]
  the desired conclusion.
   \end{proof}

  Now consider the formula:
    \begin{align*}
    \on{uniqacc}(u)\equiv (\forall u_{1},u_{2})[(\bigwedge_{i=1}^{2}\on{cof}(u_{i},v))\longrightarrow \neg \on{sep}(u_{1},u_{2})].
    \end{align*}

  \begin{lem}
  	\label{lem:uniq-acc} Let $U\in\ro(M)$ be such that $\models \on{scattered}(U)$. Then $U$ has a unique essential accumulation point if and only if $\models\on{uniqacc}(U)$.
  \end{lem}
  \begin{proof}
  	If $U$ has a unique essential accumulation point, then this is also the unique accumulation point of any $U'$ satisfying
  	$\on{cof}(U',U)$ by the first part of Observation \ref{o: convergence and cofinality}. Therefore, by the if part of Lemma \ref{lem:sep}, we have that $\lst(U_{1})$ and $\lst(U_{2})$ cannot generate $G_{\partial}$ for any sets $U_{1}$ and $U_{2}$ which
   satisfy $\on{cof}(U_i, U)$ for $i\in\{1,2\}$.

  	Conversely, if $p_{1}$ and $p_{2}$ are distinct essential accumulation points of $U$, then by
   Observation \ref{o: convergence and cofinality} there exist sets $U_{1}$ and $U_{2}$ such that $\models \on{cof}(U_{i},U)$, and
   such that
   $p_{i}$ is the unique essential accumulation point of $U_{i}$ for
   $i\in\{1,2\}$. By Observation \ref{o: convergence and essential accumulation}, it follows that $U_{i}$ must converge to $p_{i}$.
   From the only if part of Lemma \ref{lem:sep}, it follows
   that $\on{sep}(u_{1},u_{2})$ holds.
  \end{proof}

We write
\[\on{pcode}(u)\equiv \on{scattered}(u)\wedge\on{uniqacc}(u),\]
and we let
\[X:=\{U\in\ro(M)\mid \models\on{pcode}(U)\}.\]
   Lemma \ref{lem:uniq-acc} establishes the existence of a well-defined map \[\pmb{p}\colon X\longrightarrow \mathcal{P}(M).\]  This map assigns to a regular
   open set $U\in X$ its unique essential accumulation point
   $\pmb{p}(U)$.
   By Lemma \ref{lem:sep}, the formula $\neg \on{sep}(u,v)$ defines an equivalence relation on $X$ whose equivalence classes are precisely the fibers of $\pmb{p}$. This will be the definition of the relation
   $E$.

   {\bf The relation $\epsilon$.}
   To interpret the membership
   relation \[\epsilon\subseteq\mathcal{P}(M)\times\ro(M).\]

   \begin{obs}
   Consider the map
   \[\pmb{p}\times \on{Id}\colon X\times\ro(M)\longrightarrow\mathcal{P}(M)\times\ro(M),\]
   and write
     $$
   \on{membership}(u,v)\equiv(\forall u')[\on{pcode}(u')\wedge \neg \on{sep}(u,u'))\longrightarrow u'\cap v\neq\emptyset].
   $$
   The preimage $Y$ of the relation $\epsilon$ by $\pmb{p}\times \on{Id}$
coincides with the intersection
\[(X\times\ro(M))\cap \{(U,V)\mid\models\on{membership}(U,V)\}.\]
   \end{obs}

   This completes the interpretation of the relation $\epsilon$.
   Given $p,q\in\partial M$, it is similarly easy
   to define a first order formula that is satisfied by two points
   $p$ and $q$ precisely when they lie in the same component of
   $\partial M$.

   {\bf The function $\on{appl}$.}  To interpret the function $\on{appl}$, we note that for $U\in X$, we have
   $\pmb{p}(g(U))=g(\pmb{p}(U))$, and so the function $\on{appl}$ on points in $\PP(M)$ is simply defined via the action of group elements on $\ro(M)$.

      In the sequel, we will simply make reference to points in $M$ via this encoding of points as equivalence classes of regular open sets.
    We will abbreviate $\appl(g,[W]_E)$ by $g(p)$, whenever $\pmb{p}^{-1}(p)=[W]_E$, and we will simply write $p\in U$ whenever
    $(\pmb{p}^{-1}(p),U)\in\epsilon$. Thus, we have established Theorem~\ref{thm:points}.

   {\bf Union and closure.}
    More direct access to points allows us to make more direct reference to unions. We can now define $\union(u,v,w)$ by
    \[\union(u,v,w)\equiv(\forall\pi)[(\pi\in u\vee\pi\in v)\leftrightarrow \pi\in w].\] Clearly, $\union(U,V,W)$ for regular open sets $\{U,V,W\}$
    if and only if $W=U\cup V$. Henceforth, we will use the usual set-theoretic union symbol in formulae as an abbreviation for the formula
    $\union(u,v,w)$.

We are also able now to talk directly about the closure $\cl U$ of a regular open set $U$,
both in $M$ and in $V$ for arbitrary
    $U\subseteq V$.
    We have that $p\in \cl U$ if either $p\in U$ or $p\in(\fr U\cap V)$. Indeed, note that $p\in\fr U$ if and only if $g(p)=p$ for all
    $g\in G[U]G[U^{\perp}]$.
   Clearly any such $g$ stabilizes $p\in \fr U$, while if $p$ is not contained in the frontier of $U$ then
     there is a neighborhood of $p$ that is contained in the interior of $U$ or in the interior of $U^{\perp}$, and hence $p$ is moved by
    a suitable element of the rigid stabilizers of these sets. Finally, if $U\subseteq V$ then the closure of $U$ in $V$ is simply
    $U\cup \fr(U)\cap V$.

    Thus, we may interpret a symbol $(\cl {\epsilon})\sse M\times \ro(M)$ interpreted as the relation containing a pair
    $(p,U)$ if and only if $p\in\cl {U}$.
    We will use the abbreviation $p\in \cl(U)$ for this relation,
    since its meaning coincides with the topological meaning in the metalanguage.

\subsection{Encoding finite collections of points}

    We now extend the preceding encoding of points (together with the function $\appl$ and the relation $\epsilon$) to finite collections
    of points, by interpreting the sort $\PP^{<\omega}$.
 This is now straightforward. We begin by considering sets $V\in\ro(M)$ with finitely many connected components, and then consider regular open sets $U\subseteq V$ which have the property that for each $\hat V\in\pi_0(V)$, we have
   \[\models\on{pcode}(U\cap\hat V).\] We write $Y$ for the set of such suitable pairs $(V,U)$. We then obtain a natural map \[\pmb{p}^{<\omega}\colon Y\longrightarrow \PP^{<\omega}(M)\] that sends $(Y,U)\in Y$ to the set of essential accumulation points of $U\cap\hat V$, as $\hat V$ ranges over connected components of $V$.

   Interpreting an extension of $\appl$ to  $\PP^{<\omega}(M)$ is similarly straightforward, as well as seeing that the relation \[\epsilon_{\restriction}\subseteq\epsilon_{pt}\sse \PP(M)\times
    \PP^{<\omega}(M)\] is definable: $p\in T\in\PP^{<\omega}(M)$ if and only
    if there exists a component $\hat{V}\in\pi_0 V$ such that \[[\hat{V}\cap W']_E=[W]_E,\] where here $p=\pmb{p}(W)$.
    The collection of pairs $(T,m)\in\PP^{<\omega}\times\N$ such that $\#T=m$ is clearly also definable by a suitable
    formula $\#_{\on{fs}}(\tau,\alpha)$. We will occasionally need to quantify over arbitrary finite sets of points, in which case we will
    write $\tau\in S_{\on{fin}}$ for variables in this sort; the reader may compare to the G\"odel $\beta$--function, which allows one to
    quantify over finite sequences of natural numbers in arithmetic.

    We now use
    $\act_{G,\ro,\bR,\PP^{\on{fin}}}$ to denote the resulting structure
that includes finite subsets
    of $M$ together with membership and $\appl$.

 \iffalse

    \begin{proof} [Proof of Theorem~\ref{thm:points}]
    	We break the proof up into several steps.

    	{\bf Defining $X$.}
    	We define $X$ as the collection of regular open sets $W$ satisfying the following conditions, which is clearly definable by a first order
    	formula in the expanded language.

    	    	\begin{enumerate}
    		\item
    		The set $W$ has infinitely many components, i.e. $\models \inf(W)$; see Proposition~\ref{prop:number-compact-infinite}.
    		\item
    		For all components $\hat{W}\in\pi_0 W$, we have \[\#(\hat{W}^{\perp})=2,\]
    		and exactly one of these two components contains infinitely many connected components of $W$; that is,
    		\[\models(\forall u)[\on{cc}(u,W)\longrightarrow (\cc_{2}(u^{\perp})\wedge(\exists!u_{1}\in\pi_0(u^{\perp}))[\inf(u_{1}\cap W)])].\]
    		The two components of  $\hat W^{\perp}$ in $M$ will be named $V_{\hat{W}}^+$ and $V_{\hat{W}}^-$, where
		$V_{\hat{W}}^{-}\cap W$ has infinitely many connected components. We refer to $V_{\hat{W}}^+$
		as an \emph{outer set} of $W$ and to $V_{\hat{W}}^{-}$ as an \emph{inner set} of $W$.

    		\item
		Each natural number $k$ is the number of connected components of $V_{\hat{W}}^{+}\cap W$ for a unique $\hat{W}$ as above:
    		\[\models(\forall\alpha)(\exists! \hat{w}\in\pi_0(W))[(\exists v\in\pi_0(\hat w^{\perp}))(\#_=(v\cap W,\alpha))],\]
    		where
    		we will denote the $\hat{W}$ defined by this formula by $W_k$, and write $V_k^{\pm}:= V_{W_k}^{\pm}$. Here, $\#_=(v,\alpha)$
		makes sense as a formula for natural numbers $k$, since we have a canonical definable equivalence class of regular open sets
		corresponding to $k$.
    		\item\label{cond4}
		We have
    		\[ \models (\forall\hat{w}_{1},\hat{w}_{2},v_{1},v_{2})[(\bigwedge_{i=1}^2\on{outer}(v_{i},\hat{w}_{i},W)\wedge v_{1}\subsetneq
		v_{2})\longrightarrow \on{RCB}(v_{2}^{\perp},v_{1}^{\perp}\cap w_1^{\perp}) ],\]
    		where here
		$$
    		\on{outer}(v,\hat{w},w)\equiv \on{cc}(\hat{w},w)\wedge \on{cc}(v,\hat{w}^{\perp})\wedge\neg \on{inf}(v\cap w);
    		$$
    		\item \label{cond5}
We have
\begin{align*}
\models(\forall u_1,u_2)[(\on{RCB}(u_1,u_2^{\perp})\wedge\on{RCB}(u_2,u_1^{\perp}))
\longrightarrow \\(\exists\hat w\in\pi_0(W)\,\exists v\in\pi_0(\hat w^{\perp}))[
\on{outer}(v,\hat{w},W)\wedge\bigvee_{i=1}^2 u_i\subseteq v]].
\end{align*}

    	\end{enumerate}

    	{\bf Each element of $X$ isolates a unique point of $M$.}
	The intuition behind the definition of $X$ is that elements of $X$ are first order versions of
	ultrafilters used by Rubin to isolate points; cf.~Lemma 3.6.13 of~\cite{KK2021book}.
    	Given $W\in X$ we let \[p=\bigcap_{i\in\bN} V_i^-,\] where $V_{i}^{-}$ are defined as in the previous part of the proof. First, this intersection
    	is nonempty. Indeed, note that $\cl V_{i+1}^-\subsetneq V_i^-$, as is guaranteed by Condition~\ref{cond4}. In more detail, we have that
	$V_i^+\subsetneq V_{i+1}^+$, and so \[\on{RCB}((V_{i+1}^+)^{\perp},(V_i^+)^{\perp}\cap W_i^{\perp}).\] By definition,
	$(V_i^+)^{\perp}\cap W_i^{\perp}=V_i^-$.
	Since $V_{i+1}^-$ is contained in $V_{i+1}^{\perp}$,
	it follows that $\on{RCB}(V_{i+1}^-,V_i^-)$, and so the frontier of $V_{i+1}^-$ cannot meet the frontier of $V_i^-$.

	Thus,
	 for arbitrary components $W_{i_1},\ldots,W_{i_k}$ of $W$ with \[i_1<i_2<\cdots<i_k,\] we have
    	\[\varnothing\neq \cl V_{i_k+1}^-=\bigcap_{j=1}^k\cl V_{i_j+1}^-,\] and so the collection of compact sets
    	$\{\cl V_{i}^-\}_{i\in\bN}$ has the finite intersection property, and hence we have \[\varnothing\neq\bigcap_{i\in\bN}
    	\cl V_{i+1}^-\subseteq\bigcap_{i\in\bN} V_i^-.\]

    	Next, this intersection consists of exactly one point. This follows from condition \ref{cond5} above. Suppose that $p_1$ and $p_2$ are distinct points in the intersection.
    	Choose small open balls $p_1\in U_1$ and $p_2\in U_2$ such that $U_1\oplus U_2=U_1\cup U_2$.
	We then have that at least
    	one of these neighborhoods, say $U_2$, is contained in $V_i^+$ for $i\gg 0$. It follows then that $p_2$ is not contained in the intersection
    	of the sets $\{V_i^-\}_{i\in\bN}$, a contradiction.

    	Note that in fact the following stronger property holds:
    	\begin{obs}
    		\label{o: inner set convergence}For any neighborhood $U$ of $p$ there exists an index $k\in\omega$ such that
    		$V_{i}^{-}\subseteq U$ for $i\geq k$.
    	\end{obs}
    	\begin{proof}
    		If not, then the family of non-empty compact sets \[\{\cl {V}_{i}^{-}\setminus U\}_{i\in\omega\setminus\{0\}}\]
		has the finite intersection property, contradicting the uniqueness of $p$.
    	\end{proof}

    	{\bf Defining $E$.}
    	We now define an equivalence relation $E$ on $X$ so that $W_1\equiv_E W_2$ if and only if $W_1$ and
    	$W_2$ isolate the same point of $M$.
    	We define it as
    	\begin{align*}
	E(w_1,w_2)\equiv(\forall v_1)[(\exists\hat{w}_{1})[\on{outer}(v_{1},\hat{w}_{1},w_{1})]\\
	\longrightarrow (\exists v_2\exists\hat{w_{2}})[\on{outer}(v_{2},\hat{w}_{2},w_{2})\wedge v_{1}\subseteq v_{2}] ].\end{align*}

    	We first look at the only if direction. Suppose for a contradiction that $E(W_1,W_2)$ but
    	that the points $p_1$ and $p_2$ isolated by $W_{1}$ and $W_{2}$ respectively are distinct,
	and let $U_1$ and $U_2$ be small ball neighborhoods of $p_{1}$ and $p_{2}$ respectively such that
	\[U_1\oplus U_2=U_1\cup U_2\quad \textrm{and}\quad U_{1}\cap U_{2}=\emptyset.\] Writing
    	$\{V_i^-\}_{i\in\bN}$ for the collection of inner sets associated to $W_1$, observe that for all $i>1$, we have
    	\[K_i=(\cl V_i^-)\cap M\setminus U_1\] is
    	compact, and \[\bigcap_i K_i=\varnothing.\] By the finite intersection property characterization of compactness
    	and since the sets $K_i$ are nested, we have that $K_i=\varnothing$ for sufficiently large $i$. In particular,
    	$V_i^-\subseteq U_1$ for $i\gg 0$,
    	and so $U_2\subseteq V_i^+$ for $i\gg 0$. Choosing such an $i$, there is no component $W_0$ of $W_2$ for which
    	$V_{W_0}^-\subseteq V_i^-$,
    	the desired contradiction.

    	If $W_{1}$ and $W_{2}$ isolate the same point, then the formula holds by Observation \ref{o: inner set convergence}.
    	The bijection $M\to X/E$ is defined by sending $p\in M$ to $[W]_E$, where $W\in X$ is any regular open set isolating $p$.

    	{\bf The function $\appl$.} The definition of the function $\appl$ is now clear. If $[W]_E\in X/E$ then we define $\appl(g,[W]_E)=[gW]_E$.
    	It is straightforward to check that $\appl$ is well-defined and that for points $p,q\in M$, we have $g(p)=q$ if and only if
    	$\appl(g,\iota(p))=\iota(q)$.

    	{\bf The relation $\epsilon$.} The definition of the relation $\epsilon$ is also clear. We have that $([W],U)\in \epsilon$ if
	and only if the pair $(W,U)$ satisfies the formula
	\[\in(w,u)\equiv(\exists v,\hat{w})[\on{outer}(v,\hat{w},w)\wedge v^{\perp}\subseteq u],\] whence the result
    	follows.
    \end{proof}

    A finite collection of points $\{p_1,\ldots,p_k\}\sse M$ can be encoded by a pair of regular open set $(V,W)\in\ro(M)^{2}$ such that $V$ has finitely many components and each of them meets $W$ in an element of the definable set $X$ described above. That is
    \[\models \on{fin}(V)\wedge (\forall \hat{v})[\on{cc}(\hat{v},V)\longrightarrow (\hat{v}\cap W\in X)].\]
    The resulting collection $Y\subseteq\ro^{2}$ is clearly definable without parameters.

    We then have a surjective assignment $\kappa:Y\longrightarrow\PP^{<\omega}(M)$ given by
    \[(V,W)\mapsto  \{[V_i\cap W]_E\}_{i=1}^{k}\in \PP^{<\omega}(X/E),\] where $\{V_{i}\}_{i=1}^{k}$ is the
    collection of connected components of $V$. Consider the formula
    \[R(v_{1},w_{1},v_{2},w_{2})\equiv(\forall \hat{v}_{1})(\exists! \hat{v}_2)[\on{cc}(\hat{v}_1,v_{1})
    \wedge \on{cc}(\hat{v}_2,v_2)\wedge E(\hat{v}_1\cap w_1,\hat{v}_2\cap w_2)].\]
    It is straightforward to check that \[\models R(V_{1},W_{1},V_{2},W_{2})\wedge R(V_{2},W_{2},V_{1},W_{1})\] if and only if $(V_{1},W_{1})$ and $(V_{2},W_{2})$ correspond to the same finite set of points.

    \fi

  \subsection{The exponentiation function}
    We now show that the map
    $$G\times\N\times M\to M, \quad (g,n,p) \mapsto g^{n}\cdot p$$
    is definable in $\act_{\N,\mathcal{P}(N),\bR,\PP^{<\omega}}$, which will then clearly imply that the map \[\exp:G\times\N\to G\] is itself
    definable.
    It is easily seen that $\exp(g,n)\cdot p=p'$ if and only if the tuple $(g,n,p,p')$ satisfies the formula
    \[\exp(\gamma,\alpha,\pi,\pi')\equiv \exp_{\on{lin}}(\gamma,\alpha,\pi,\pi')\vee \exp_{\on{cyc}}(\gamma,\alpha,\pi,\pi'),\]
    where

    \begin{align*}
    	\exp_{\on{lin}}(\gamma,\alpha,\pi,\pi')\equiv&(\exists\tau\in S_{\on{fin}})(\#_{\on{fs}}(\tau,\alpha)\wedge(\forall\pi_1)
	[(\pi\in \tau)\wedge (\pi'\in\tau)\wedge\\
    	&(\pi_1\neq \pi\longrightarrow (\exists!\pi_2\in\tau)[\gamma\cdot \pi_2=\pi_1])\wedge \\
    	&(\pi_1\neq \pi'\longrightarrow (\exists!\pi_2\in \tau)
    	[\gamma\cdot \pi_1=\pi_2])\wedge\\
    	&\neg(\exists\tau'\in S_{\on{fin}})[\tau'\subsetneq\tau\wedge\gamma\cdot\tau'=\tau']],\\
    	\exp_{\on{cyc}}(\gamma,\alpha,\pi,\pi')\equiv&(\exists\tau_{1},\tau_{2}\in S_{\on{fin}}\exists\beta_{1},\beta_{2})
	[\tau_{1}\subseteq\tau_{2}\wedge\gamma\cdot\tau_{2}=\tau_{2}\wedge\bigwedge_{i=1}^{2}\#_{\on{fs}}(\tau_{i},\beta_{i})\wedge\\
    	&\exp_{\on{lin}}(\gamma,\beta_{1},\pi,\pi')\wedge(\exists\alpha')[\alpha'\cdot\beta_{2}+\beta_{1}=\alpha]],&
    \end{align*}
    where again $S_{\on{fin}}$ denotes variables in the sort for $\PP^{<\omega}(M)$.

It is now clear that the sort $\cont$ can be interpreted in $L_{\bf G,\ro,\bR}$.

\section{Interpretation of collared balls}\label{sec:balls}

  \newcommand{\sq}[0]{\sqrt{2}}
  \newcommand{\U}[0]{\mathbb{U}}
  \newcommand{\mathrm{pr}}{\mathrm{pr}}
  \newcommand{\pr}[0]{\mathrm{pr}}
  \newcommand{\cord}[0]{\mathrm{cord}}
  \newcommand{\conv}[0]{\mathrm{conv}}
  \newcommand{\flw}[0]{\mathrm{flw}}
  \newcommand{\refn}[0]{\mathrm{refn}}
  \newcommand{\flws}[0]{\mathrm{flws}}

  \newcommand{\trunc}[0]{\mathrm{trunc}}
  \newcommand{\iflws}[0]{\mathrm{iflws}}
  \newcommand{\scflws}[0]{\mathrm{scflws}}

Throughout this section, we will assume that we work in the language
containing second order arithmetic and finite sets of points, i.e.~$\act_{\N,\mathcal{P}(N),\bR,\PP^{<\omega}}$.
The main objective of this section is to interpret standard balls (in $\bR^n$) inside of an $n$--manifold.

Define a map $\trunc\co\bR^n\to[-1,1]^n$ by
\[\trunc(r_1,\ldots,r_n):=\left(\max(-1,\min(1,r_i))\right)_{i=1,\ldots,n}.\]
See Figure~\ref{fig:trunc}.
\begin{figure}[!htb]
\tikzstyle {bv}=[black,draw,shape=circle,fill=black,inner sep=1pt]
  \begin{center}
\begin{tikzpicture}
  \draw[->] (-3, 0) -- (4.2, 0) node[right] {$x$};
  \draw[->] (0, -1) -- (0, 1) node[above] {$y$};
  \draw[thick] (-3,-1) -- (-1,-1) --  (1,1) -- (3,1);
\end{tikzpicture}
\caption{The graph of the map $\on{trunc}$ for the case $n=1$.}
\label{fig:trunc}
\end{center}
\end{figure}

By a \emph{collar (neighborhood)} $U$ of a set $B$ in a manifold $M$,
we mean the image of a homeomorphism $h\co B\times [0,1)\to U$ such that $h(b,0)=b$ for all $b\in B$.
A fundamental result due to Brown~\cite{Brown1962} is that
 the boundary of every non-closed manifold admits a collar.
A collar $U$ of the boundary is \emph{extendable} if $\cl U$ is contained in a larger collar of the boundary.
The output of this section are the first two conclusions of the following; we relegate the discussion of collars to Section~\ref{sec:boundary}.

\begin{thm}\label{thm:output-balls}
The following hold.
\begin{enumerate}
\item\label{p:output1}
There is a sentence  $\dim_n$
such that for all $(M,G)\in\cM_{(\vol)}$,
we have
\[
\agape(M,G)\models\dim_n\]
 if and only if $M$ is an $n$--manifold.
\item
For each $n\ge2$, there exist formulae
$\on{flws}_n(\underline\gamma,u,\pi)$ and $\param_n(u,\underline{\gamma},\pi,\underline{\rho},\pi')$ such that the following hold
for each pair $(M,G)\in\cM_{(\vol)}$
satisfying $\dim M=n$:
\be[(i)]
\item
if $U\in\ro(M)$, $\underbar g\in \cH^n$ and $\pi\in M$,
and if    	\[    	\agape(\cH,M)\models\on{flws}_n(U,\underbar g,p)    	\]
then we have a unique homeomorphism
\[
h=h_{U,\underline{g},p}\co B^n(2)\to \cl U\]
which sends $0$ to $p$ and which satisfies
\[ h (r)=q\text{ iff }\agape(M,G)\models	\param_n(U,\underbar g,p,r,q)\]
for all $r\in B^n(2)$ and $q\in M$.
\item Conversely, whenever $U$ is a good ball in a manifold $M$ (with its measure being sufficiently small if $(M,G)\in\cM_{\vol}$), there exist $\underbar g\in \cH^n$ and $p\in U$ such that $\on{flws}_n(U,\underbar g,p)$ holds.
\ee

\item
There exists an $\agape$ formula $\partial\collar(u)$
such that for all $(M,G)\in\cM_{(\vol)}$ with $\dim M\ge 2$ and $\partial M\ne\varnothing$,
and  for all $U\in\ro(M)$,
we have
\[
\agape(M,G)\models \partial\collar(U)\]
iff $\partial M\subseteq U$ and $U$ is an extendable collar of $\partial M$.
\end{enumerate}
  \end{thm}

We emphasize again that the above formulae for $\cM$ and $\cM_{\vol}$ may differ; for instance, the sentence $\dim_n$ may be more precisely denoted as $\dim_n$ and $\dim_n^{\vol}$ separately depending on the context.

  \subsection{Detecting the dimension of a manifold}
    We prove the existence of the a formula $\dim_n$ as in Theorem~\ref{thm:output-balls} by interpreting a sufficient amount of dimension
    theory. Recall that an open cover $\mathcal U=\{U_i\}_{i\in I}$ of a topological space $X$ is \emph{locally finite}
    if every point in $X$ is contained
    in finitely many elements of $\mathcal U$;
in this case, we define the \emph{order} of $\mathcal{U}$ as the number
\[
\sup_{x\in X} \abs*{\{U\in\mathcal{U}\mid x\in U\}}.\]
A topological space $X$ has \emph{topological dimension} at most
    $n$ if an arbitrary cover of $X$ admits a refinement
    of order at most $n+1$, and has topological dimension at least $n$ if it does not have dimension at most $n-1$.
    It is a standard result from dimension theory that if $M$ is an $n$--manifold then $M$ has topological dimension $n$.

We will prove the following, which trivially implies part (\ref{p:output1}) of Theorem~\ref{thm:output-balls}.

\begin{prop}\label{prop:detect-dim}
For each $n\in\omega$,
there is a sentence  $\dim_{\le n}$
such that for all $(M,G)\in\cM_{(\vol)}$,
we have
\[
\agape(M,G)\models\dim_{\le n}\]
 if and only if the topological dimension of $M$ is at most $n$.
\end{prop}

A collection $\mathcal{U}$ of open sets is said to \emph{shrink} to another collection $\mathcal V$ of open sets if each connected component of an element in $\mathcal V$ is contained in some element in $\mathcal U$.
Ostrand's theorem~\cite{ostrand} states that a normal topological space has topological dimension at most $n$
iff every locally finite open cover of $X$ shrinks to a cover with cardinality at most $n+1$.
A key observation for Proposition~\ref{prop:detect-dim} is the following.
\begin{prop}\label{p:order-cech}
For each $n>0$, there exists a regular open cover of a unit cube $I_n\sse\bR^n$ which does not shrink to a regular open cover of $I_n$ with cardinality at most $n$.
    \end{prop}
\begin{proof}
For $n,\ell\geq 1$, write $I^{\ell}_n:= [0,\ell]^n$, and $I_n:=I^1_n$. We subdivide $I^{\ell}_n$ into
    cubes of unit dimension, say $\{C_1,\ldots,C^{\ell^n}\}$. We define a certain cover of $I^{\ell}_n$ by a bounded number of open sets
    $\{U_1,\ldots,U_{k(n)}\}$, where the number of these open
    sets depends only on $n$, where the diameter of each component of these open sets is at most $1$, and which is uniform in $\ell$.
    The construction of this cover is almost the same as the one in Section 50 (page 306) of Munkres' book~\cite{munkres}, modified slightly
    to guarantee that the resulting sets are regular. The only change that has to be made is that the first open set $U_1$ cannot be the union
    of the interiors of the cubes $\{C_1,\ldots,C^{\ell^n}\}$. Instead, we take balls of radius $1/2$ centered at the integer points of
    $I^{\ell}_n\subset\bR^n$, together with balls of radius $1/2$ centered at $1/2$--integer points in the interiors of the cubes.
    The union of these two families of balls form regular open sets, which we call $U_1$ and $U_2$ respectively.
    The construction of the remaining open sets is identical to what is done by Munkres, wherein the sets are drawn explicitly in the case
    $n=2$. In that case, $k(n)=3$. Thus, for each $\ell$ we obtain a cover $\mathcal U^{\ell}_0$
    of $I^{\ell}_n$ by $k(n)$ regular open sets. This cover has order $n+1$.

\begin{claim*}\label{cla:order-cech}
For some value of $\ell$, the cover $\mathcal U^{\ell}_0$ has no refinement of order at most $n$.
\end{claim*}

The proof is a standard argument in \v{C}ech homology, and we include it for the convenience of the reader.
By scaling down $\mathcal U^{\ell}_0$ by a factor of $\ell$ we obtain a cover of $I_n$ by $k(n)$ regular open sets, each of whose components has diameter at most $1/\ell$.
We fix the notation \[\mathcal U^{\ell}=\{U_1^{\ell},\ldots,U_{k(n)}^{\ell}\}\] for this specific open cover of $I_n$. Note that
    $\mathcal U^{\ell}_0$ has a refinement of order less than $n+1$ if and only if $\mathcal U^{\ell}$ does.
    Note from Lebesgue covering lemma that an arbitrary arbitrary cover of $I_n$ admits a refinement of the form $\mathcal U^{\ell}$ for some $\ell$. In other words, the covers $\{\mathcal U^{\ell}\}_{\ell\in\bN}$ are cofinal in the poset of finite covers of $I_n$, with the partial order
    being given by refinement.

Assume the claim is not true, and let $\mathcal V^{\ell}_0$ be such a refinement for all $\ell$.
    We obtain a corresponding refinement $\mathcal V^{\ell}$ of
    $\mathcal U^{\ell}$ by scaling. The covers $\{\mathcal V^{\ell}\}_{\ell\in\bN}$ are cofinal in the poset of finite covers of $I_n$ as well.

    Fix the notation $S_n=\partial I_n$. The covers $\{\mathcal U^{\ell}\}_{\ell\in\bN}$ induce covers of $S_n$. Recall the construction
    of the \emph{nerve} of a cover, which is a simplicial complex with $k$--simplices corresponding to nonempty intersection of $k+1$
    distinct open sets in the cover, and the face relation being inclusion. The cover $\mathcal U^{\ell}$ and its restriction to $S_n$ thus
    naturally results in pairs $(N_u^{\ell},A_u^{\ell})$
    and $(N_v^{\ell},A_v^{\ell})$, given by the geometric realization of the nerves of $\mathcal U^{\ell}$ and $\mathcal V^{\ell}$
    respectively, and the geometric
    realization of the nerves of the restrictions to $S_n$.

    We obtain the \v{C}ech homology groups of the pair $(I_n,S_n)$ as the inverse limit of the homology groups of the pairs
    $(N_u^{\ell},A_u^{\ell})$ and $(N_v^{\ell},A_v^{\ell})$ respectively. Because the systems of covers
    $\{\mathcal U^{\ell}\}_{\ell\in\bN}$ and $\{\mathcal V^{\ell}\}_{\ell\in\bN}$ are both cofinal, the \v{C}ech homology groups obtained
    from these two pairs are canonically isomorphic.

    The natural comparison map \[H_*(I_n,S_n)\longrightarrow \check{H}_*(I_n,S_n)\] is an isomorphism. It follows
    that $\check{H}_n(I_n,S_n)$ is nonzero, since it coincides with the top dimensional homology of the $n$--sphere.

    Since $\{\mathcal V^{\ell}\}_{\ell\in\bN}$ has order less than $n+1$, we have that the homology of the pair
    $(N_v^{\ell},A_v^{\ell})$ vanishes in dimension $n$. Since the homology of this pair agrees with the homology of the $n$--sphere,
    this is a contradiction.
\end{proof}

    \begin{proof} [Proof of Proposition~\ref{p:order-cech}]
For fixed integers $m,n>0$ it is clearly first order expressible that a collection $\{U_1,\ldots,U_m\}$ shrinks to another collection $\{V_1,\ldots,V_n\}$ with $U_i$ and $V_j$ being regular open sets; that is, we may require that each connected component of $U_i$ is contained in some $V_j$.
Also, being a cover of a regular open set $U$ is also expressible since we have an access to the union in the action structure with points.
Hence, the existence of the formula $\dim_n$ is immediate from the following claim.
Recall the definition of $k(n)$ from the previous proof.

\begin{claim*}
A manifold $M$ has dimension at most $n$ if and only if
for all $U\in\ro(M)$ and for all $\mathcal{U}\sse\ro(M)$ satisfying $\cl U\sse\bigcup \UU\sse\inte M$ with cardinality $k(n)$
the cover $\mathcal{U}$ shrinks to some regular open cover $\mathcal{V}$ of $\cl U$ with cardinality at most $n+1$.
\end{claim*}

For the backward direction, we consider a collared ball $B$ in $M$, which has dimension $m:=\dim M$.
Assume for contradiction that $m>n$.
Recall from Proposition~\ref{p:order-cech} that a unit cube in $\bR^n$ admits a regular open cover $\mathcal U^{\ell}$ with cardinality $k(n)$
which does not shrink to a regular open cover with cardinality at most $n$.
By taking the Cartesian product of this cover with an open cube of $m-n$,
we obtain a regular open cover $\mathcal W^{\ell}$ of $B$ with cardinality still $k(n)$.
If $\mathcal W^{\ell}$ shrinks to a cover of $B$ with cardinality at most $n$,
then by intersection this would produce a shrinking of $\mathcal U^{\ell}$ with cardinality at most $n$, contradicting Proposition~\ref{p:order-cech}.
This violates the hypothesis.

The forward direction of the claim for open subsets of $M$ is precisely implied by
Ostrand's theorem mentioned above~\cite{ostrand}. To obtain the conclusion with regular open sets, we may simply follow the proof of Lemma 3 in~\cite{ostrand}, using Lemma~\ref{lem:shrink} to guarantee
that the resulting sets are regular.
\end{proof}

    In the proof of Proposition~\ref{prop:detect-dim},
we recall that $\cl u$ and the union symbol are abbreviations for certain formulae coming from the interpretation of points in $M$,
    and have the intended meanings.

  \subsection{Parametrizing balls in $M$ in dimension two and higher}
We now continue the proof of Theorem~\ref{thm:output-balls}.
We continue to assume $\dim M\ge 2$.
    Let \[\pr_{\sq}:\R\longrightarrow \R/\sq\Z\] be the quotient map sending $x\mapsto x+\sq\Z$,
    so that the image of $\bZ$ is dense.
    The following observation is
    straightforward and left to the reader:
    \begin{obs}
    	\label{o: order}There exists a formula $\cord(\rho_{1},\rho_{2},\rho_{3})$ in the language of ordered rings such that
    	for $\{r_{1},r_{2},r_{3}\}\subset\R$, we have \[\R\models \cord(r_{1},r_{2},r_{3})\] if and only if
    	the sequence \[\{\pr_{\sq}(r_{1}),\pr_{\sq}(r_{2}),\pr_{\sq}(r_{3})\}\]
consists of three distinct points appearing
 clockwise in the circle
    	$\R/\sq\Z$.
    \end{obs}

    We use Observation~\ref{o: order} to interpret convergence of powers of group elements, in a suitable sense.

    \begin{lem}
    	\label{l: flow}There exist formulae
    	\[\conv(\gamma,\delta,u,\rho), \quad\flw(\gamma,u)\] such that the following hold:
    	\begin{enumerate}
    		\item For all $r\in\R$ and all $g,h\in \cH$ preserving $U\in\ro(M)$ setwise,
    		we have \[\models \conv(g,h,U,r)\] if and only if  $(g^{k_{n}})_{\restriction U}$ converges uniformly to
    		$h_{\restriction U}$, with respect to any compatible metric on $M$, whenever $\pr_{\sq}(k_{n})$ converges to $\pr_{\sq}(r)$.
    		\item For any $U\in\ro(M)$ and any $g\in G$, we have \[\models \flw(g,U)\] if and only if
    		$U$ is  invariant under the action of $g$, there exists a  (necessarily unique) continuous homeomorphic embedding
    		\[\Gamma:\R/\sq\Z\longrightarrow \cH[U]\] with $\Gamma(m)=g^{m}_{\restriction U}$ for all $m\in\N$,
    		and such that for all $p\in U$ the map \[\R/\sqrt{2}\Z\ni [s]\mapsto \Gamma([s])\cdot p\] is injective.
    	\end{enumerate}
    \end{lem}

    We remark that Lemma~\ref{l: flow} is formulated independently of the dimension of the ambient manifold, though the formula $\flw_g(g,U)$ may never be satisfied for one-dimensional manifolds.

    \begin{proof} [Proof of Lemma~\ref{l: flow}]
    	Let $K=n+1$, let $\underline{v},\underline{v}'$ be tuples of $K$--many variables, and consider the formula
\begin{align*}
    		&\conv(\gamma,\delta,u,\rho)\equiv(\forall \underline{v})[\,\on{fcov}(u,\underline{v})\rightarrow
    		((\exists \underline{v}')[\,\on{fcov}(u,\underline{v}')\wedge\bigwedge_{i=1}^{K}v'_{i}\subseteq v_{i}\wedge\\
    		&\exists\sigma_{1},\sigma_{2}\,\,\cord(\sigma_{1},\rho,\sigma_{2})\wedge
    		\forall\alpha\,(\cord(\sigma_{1},\alpha,\sigma_{2})\rightarrow \refn(\delta^{-1}\gamma^{\alpha},\underline{v},\underline{v}',u))]],
    	\end{align*}
      where here
      \[\on{fcov}(u,\underline{v})\equiv (\cl u)
		\subseteq\bigcup_{i=1}^{K}v_{i}\wedge\bigwedge_{i=1}^{K}\on{fin}(v_{i}),\] and where
		\begin{align*}
	    	\refn(\gamma,\underline{v},\underline{v'},u)\equiv&\bigwedge_{i=1}^{K}(\forall w\in\pi_{0}(v_{i}))(\forall w'\in\pi_{0}(v'_{i}))
		[w'\subseteq w\rightarrow\gamma\cdot (w'\cap\cl u)\subseteq w].
    	\end{align*}
      That the formula
      $\conv$ has the required properties follows easily from Ostrand's Theorem; see the proof of Proposition~\ref{prop:detect-dim}.
It is now easy to check that
    	  	\begin{align*}
    				\flw(\gamma,u)\equiv& \neg\on{touch}_\partial(u)\wedge
				[(\forall\rho \exists \delta)\conv(\gamma,\delta,u,\rho)]\wedge [(\forall \delta\forall\rho\forall \pi\in u)
    				\\&\,[(( \delta\cdot \pi=\pi\wedge \conv(\gamma,\delta,u,\rho))\rightarrow \sfrac{\rho}{\sq}\in\Z)]]
    		\end{align*}
    	satisfies the desired condition, completing the proof.
    \end{proof}

    In the situation of Lemma~\ref{l: flow}, we will say that $g$ defines a circular flow on the open set $U$.
    The formula $\conv(\gamma,\delta,u,\rho)$ is encoding the fact that certain powers of $g$ are converging to $h$; the element $g$
    is viewed as an irrational rotation through a specified angle, and $h$ is an arbitrary rotation. We spell out the meaning of
    the formula $\on{conv}$ in English for the convenience of the reader:

\begin{lem}
For a regular open $U$, for $g,h\in \cH$ setwise stabilizing $U$, and for $r\in \bR$, the following are equivalent.
\be[(A)]
\item For all $\epsilon>0$ there exists $\delta>0$ such that
whenever \[|s+t\sqrt{2}-r|<\delta\] with $s,t\in\bZ$,
we have that
\[
 d_\infty(h^{-1}\circ g\restriction_U^s,\Id_U)<\epsilon.\]
\item
For an arbitrary cover $\{V_i\}_{1\leq i\leq n+1}$ of $\cl U$ with each $V_i$ having finitely many connected components,
we have some $\delta>0$
and another cover $\{V_i'\}_{1\leq i\leq n+1}$ of $\cl U$
 with each $V_i'$ having finitely many connected components
 such that the properties below hold:
\be[(i)]
\item $V_i'\sse V_i$ for each $i$;
\item for each $s,t\in\bZ$ satisfying  $|s+t\sqrt{2}-r|<\delta$,
and for each $\hat V\in\pi_0(V_i)$ and $\hat V'\in \pi_0(V_i')$ satisfying $\hat V'\sse \hat V$,
we have
\[h^{-1}g^s\left(\cl U\cap \hat V'\right)\sse \hat V.\]
\ee\ee
\end{lem}

    \begin{rem}
    	We choose the value $\sqrt{2}$ for concreteness but clearly we could have chosen any other irrational number
    	that is definable in arithmetic without parameters.
    \end{rem}

    The next proposition completes the second part of
    Theorem~\ref{thm:output-balls}. Here, underlined tuples consist of $n$ variables or objects of relevant
    types.
    \begin{prop}\label{prop:parametrize}
    	There exist formulae $$\flws_{n}(\underline\gamma,u,\pi),\quad
    	\param_{n}(\underline\gamma,\pi,\underline\rho,\pi'),\quad n\geq 1$$
    	such that the following holds.

    	\begin{enumerate}
    		\item If $\models \on{flw}(V,g)$ and \[\Gamma:\R/\sq\R\longrightarrow
		\cH[V]\] is as given by Lemma \ref{l: flow}, then for \[p,p'\in V,\quad r\in\R,\] we have
		$\models\param_{1}(g,p,r,p')$ if and only if $\Gamma([r])\cdot p=p'$.
    		\item For $n\geq 2$, if \[\models \flws_{n}(\underline g,U,p)\] then the formula with parameters $\param_n(\underline{g},
		p,\underline{\rho},\pi')$
    		determines a unique homeomorphism  \[h_{U,\underline{g},p}:[-1,1]^{n}\longrightarrow \cl U\sse\inte M\]
    		sending the origin $\bar{0}$ to $p$.
		Specifically, for all $\underline{r}\in\R^{n}$ and $p'\in M$
		we have that \[\models \param_{n}(\underline{g},p,\underline{r},p')\] if and only if
    		\[h_{U,\underline{g},p}(\trunc(\underline{r}))=p'\in\cl U.\]
    		\item
    		For any collared open ball $U\sse X$, of sufficiently small measure in case $(M,G)\in\cM_{\vol}$,
    		we have \[\models(\exists \underline{\gamma}\exists \pi)\,\flws_{n}(U,\pi,\underline{\gamma}).\]
    	\end{enumerate}
    \end{prop}
    \begin{proof}
    	Using the formulae from Lemma \ref{l: flow} and Observation \ref{o: order}, we write:

    	\begin{align*}
    		\flws_{n}(\underline{\gamma},u,\pi)\equiv& \exists \underline{v}\,\,\bigwedge_{i=1}^{m}
    		\flw(\gamma_{i},v_{i})\wedge \pi\in u\wedge \cl u\subseteq\bigcap_{i=1}^{m}v_{i}\wedge\\
    		& \scflws_{n}(\underline{\gamma},u,\underline{v},\pi)\wedge \iflws_{n}(\underline{\gamma},u,\underline{v},\pi)\wedge
		\on{wdflws}_{n}(\underline{\gamma},u,\underline{v},\pi),
    	\end{align*}

    	where here we use the notation

    	\begin{align*}
    		\scflws_{n}(\underline{\gamma},u,\underline{v},\pi)\equiv&  (\forall \pi'\in \cl u\,\exists\underline{\rho},\exists \underline{\delta})\,
    		\bigwedge_{i=1}^{m}(\rho_{i}\in[0,1]\wedge \conv(\gamma_{i},\delta_{i},v_i,\rho_{i}))\wedge\\
    		&\bigwedge_{\mathfrak{s}\in \mathfrak{S}_{m}}\prod_{i=1}^{m}\delta_{\mathfrak{s}(i)}\cdot \pi=\pi',  \\
    		\iflws_{n}(\underline{\gamma},u,\underline{v},\pi)
		\equiv& (\forall\underline{\rho},\underline{\sigma}\forall \underline{\delta},\underline{\delta'})\,
    		](\bigvee_{i=1}^{m} \rho_{i}\neq\sigma_{i}\wedge\bigwedge_{i=1}^{n}\{\rho_{i},\sigma_{i}\}\subseteq [0,1]\wedge\\
&\bigwedge_{i=1}^{m}\conv(\gamma_{i},\delta_{i},v_i,\rho_{i})\wedge
\conv(\gamma_{i},\delta'_{i},v_i,\sigma_{i}))
\\
  &
\rightarrow \prod_{i=1}^{m}\delta_{i}\cdot \pi\neq\prod_{i=1}^{m}\delta'_{i}\cdot \pi], \\
    	 \on{wdflws}_{n}(\underline{\gamma},u,\underline{v},\pi)
	 \equiv&(\forall\underline{\rho}\forall\underline{\delta})\,[(\bigwedge_{i=1}^{n}\rho_{i}\in[0,1] \wedge\bigwedge_{i=1}^{n}\on{conv}(\gamma_{i},\delta_{i},v_i,\rho_{i}))
  \\
  &\rightarrow \prod_{i=1}^{n}\delta_{i}\cdot\pi\in \cl u]
    	\end{align*}

    	and where $\mathfrak{S}_{m}$ stands for the symmetric group in $m$ elements. It is easy to see that
    	$\flws_{n}(\underline{g},U,p)$ holds if and only if:
	\begin{enumerate}
	\item
	There exists $m$ circular flows in the sense of  Lemma \ref{l: flow};
	\item
    	The combined restrictions of the flows to the circular interval $[0,1]$ define a homeomorphism \[[0,1]^n\longrightarrow \cl U;\]
	\item
	Such flows exist for any collared ball $U$, which is assumed to be
	of sufficiently small measure in the measure preserving case.
	\end{enumerate}

    	On the other hand, the function \[\trunc\colon\R^{n}\to\R^{n}\] is  clearly definable in $\R$ without parameters.
    	We leave the task of combining the definitions with the formula $\conv(\gamma,\delta,u,\rho)$ from
    	Lemma \ref{l: flow} into a formula $\param$ with the required properties to the reader.
    \end{proof}

    \section{Manifolds with boundary}\label{sec:boundary}
In this section, we finish the proof of Theorem~\ref{thm:output-balls}, by producing the desired formula $\partial\collar(u)$.
The basic strategy is to express that certain neighborhoods of boundary components in an $n$--dimensional manifold $M$ admit direct product decompositions of the form $M_0\times [0,1)$, where $M_0$ has dimension $n-1$. For that, we need to characterize certain parametrized bundles of the form $M_0\times (0,1)$, and to control their interactions with boundary components of $M$. This will require us to interpret the boundary of $M$.

   \subsection{Parametrized bundles}

\begin{lem}
	\label{l: interior bundles}There exist formulae \[\bdle_{n}(u),\quad \adbdle_{n}(u,v)\] such that the following are satisfied:
	\begin{enumerate}
  		\item Whenever $\dim(M)=n$ we have that $\models \bdle_{n}(U)$ if and only if:
		\begin{enumerate}
		\item
		$M\setminus \cl U$ has two connected components;
		\item
		 We have $\neg\on{touch}_\partial(u)$;
		 \item
		 $\cl U$ is homeomorphic to a product $I\times M_{0}$, where $M_{0}$ is a closed $(n-1)$-dimensional manifold and
		 $U\cong(0,1)\times M_{0}$;
		 \end{enumerate}
  		\item If \[\models \bdle_{n}(U)\wedge \bdle_{n}(V)\] holds then $\models \adbdle_{n}(U,V)$ holds if and only if $\fr U$
		has one connected component in common with $\fr V$.
	\end{enumerate}
  \end{lem}

  The names $\bdle$ and $\adbdle$ stand for bundle and adjacent bundle, respectively.

\begin{proof} [Proof of Lemma~\ref{l: interior bundles}]
	Write

	\[\underline{\gamma}=(\gamma_{1},\ldots, \gamma_{n+1}),\quad \underline{v}=(v_{1},\ldots, v_{n+1}).\]

  	Our formulae are constructed simply by expressing that $U$ is obtained as a union of $(0,1)$-fibered open sets,
	where the fibrations agree on any pairwise intersection and the fibration extends to the closure:
 \begin{align*}
	\bdle_{n}(u)\equiv&\on{cc}_{2}(u^{\perp})\wedge\exists\underline{\gamma}\exists\underline{v}\exists\underline{v}'\,\,(u=\bigcup_{j=1}^{n+1}v_{j}\wedge \bigwedge_{j=1}^{n+1}(\on{flw}(\gamma_j,v_j')\wedge\cl v_{j}\subseteq v'_{j}\wedge
	\cfibr(\gamma_{j},v_{j})\wedge\\
	&\forall\pi\in v_{j}\,\exists\underline{\delta}\,\exists w\,\exists\pi_{0}\,\,[w\subseteq v_{j}\wedge \flws(\underline{\delta},\gamma,w,\pi_{0})\wedge\\
	&\forall\pi_{1}\in w \,\forall\pi_{2}\in v_{j}\,(\orb(\gamma_{j},\pi_{1},\pi_{2})\longrightarrow\pi_{2}\in w)])\wedge\\

		&\bigwedge_{1\leq j_{1}<j_{2}\leq n+1}\comp(\gamma_{j_{1}},\gamma_{j_{2}},v_{j_{1}},v_{j_{2}})),
 \end{align*}
 where here $\orb(\gamma,\pi_{1},\pi_{2})$ is a (straightforward to find) formula expressing the fact that $\pi_{1}$ and $\pi_{2}$
 are in the same orbit with respect to the flow defined by $\gamma$, the formula
 $\cfibr(\gamma,v)$ expresses the fact that the intersection of any orbit of the flow defined by $\gamma$ with $v$ is connected. Specifically,
 the fact that any orbit is a circle is being used, so that if the intersection of a circle with an open set is disconnected, then at least two intervals
 in the circle lie in the open set and two lie outside.

 The formula $\comp(\gamma_{1},\gamma_{2},w_{1},w_{2})$ expresses the fact that the flows defined by
$\gamma_{1},\gamma_{2}$ agree on $\cl w_{1}\cap \cl w_{2}$, which is a union of full orbits by the flow on both $w_{1}$ and $w_{2}$:
 \begin{align*}
  		\cfibr(\gamma,v)\equiv \neg(\exists \rho_{1},\dots \rho_{4}\exists\pi_{1},\dots \pi_{4}\,\,
		\bigwedge_{i=1}^{3}\cord(\rho_{i},\rho_{i+1},\rho_{i+2})\wedge\\
  		\exists\pi\,\bigwedge_{i=1}^{4}\param_{1}(\gamma,\pi,\rho_{i},\pi_{i})\wedge \bigwedge_{k=1}^{2}(\pi_{2i}\in v
		\wedge\pi_{2i+1}\notin v)),\\
  		\comp(\gamma_{1},\gamma_{2},w_{1},w_{2})\equiv
		(\forall\pi_{1},\pi_{2}\forall\rho)(\forall\pi\in \cl w_{1}\cap \cl w_{2})
		\,\,\\(\bigwedge_{i=1}^{2}\param_1(\gamma_{i},\pi,\rho,\pi_i)\rightarrow
  	  \bigwedge_{i=1}^{2}(\pi_i\in w_{i}
	  \longrightarrow(\pi_{3-i}\in w_{3-i}\wedge\pi_1=\pi_2)).
 \end{align*}

  The fact that the covering of $U$ can be taken to be the collection of connected components in $n+1$ open sets follows from
Ostrand's theorem. We now can write:
  \begin{align*}
  	\adbdle_{n}(u,v)\equiv(\exists u_{0})[\bdle_{n}(u_{0})\wedge \cl u_{0}\subseteq u\wedge \exists w\,\,(\on{cc}(w,u_{0}^{\perp}\cap u)
	\wedge w\cap\fr u\subseteq \fr v)],
  \end{align*}
  which has the desired properties.
\end{proof}

First, we build a formula $\on{seqbdle}_n(\underline\gamma,v)$, which
expresses that an open set $V$ is a union of components so that:
\begin{enumerate}
\item
Each component of $V$
satisfies the formula $\on{bdle}_n$.
\item
The closures of the components of $V$ are disjoint.
\item
If $p\in\inte M$ then there is a regular open set $U$ containing
$p$ such that $U\cap V$ has finitely many components.
\item
The bundle structure on the components of $V$ is parametrized by
a single tuple $\underline g$ of group elements.
\end{enumerate}

The first three requirements here are evidently first order expressible,
while the requirement that the parametrizations be encoded by
a single tuple of group elements is easy to implement. Namely, for every component $\hat V$ of $V$, we find a tuple coming from
circular flows $\underline g_{\hat V}$ parametrizing the bundle structure on $\hat V$, so that each group element is supported in a slightly larger open set containing $\hat V$. Then, for distinct components $\hat V_1$ and $\hat V_2$, we insist that the supports of elements in $\underline g_{\hat V_1}$ and $\underline g_{\hat V_2}$ be disjoint. Taking component-wise products of tuples of the form
$\underline g_{\hat V}$ over finite collections of components of $V$
gives a bounded and equicontinuous family of
tuples of homeomorphisms of $M$, whereby we may simple extract
a limit by the Arzel\`a--Ascoli Theorem.

   \subsection{Characterizing collar neighborhoods}

Recall from Brown~\cite[Theorem 2]{Brown1962} that the boundary of a (topological) manifold is always collared. Let us characterize such a collared neighborhood.

We build a formula $\on{altbdle}_n(\underline\gamma_1,\underline\gamma_2,v_1,v_2)$ which expresses the following.

\begin{enumerate}
\item
The pair $(\underline g_i,V_i)$ satisfies the formula $\on{seqbdle}_n$
for $i\in\{1,2\}$.
\item
The graph whose vertices are the components of $V_1$ and $V_2$ and
whose adjacency relation is the $\on{adbdle}_n$ relation, is
isomorphic to an infinite ray.
\item
The regular open set $V=V_1\oplus V_2$ contains a component $N$ of $\partial M$ in its frontier.
\item
The parametrized bundle structures on adjacent components of $V_1$ and $V_2$ agree.
\end{enumerate}

These conditions are all now easily seen to be first order
expressible. The last condition means that parametrized balls in
components of $V_1$ align with parametrized balls in components of
$V_2$, and the fiber directions piece together coherently.

Observe that $V\cong (0,1)\times M_0$, where $M_0$ is an $n-1$--dimensional manifold. It is not imediate that $V$ is homeomorphic to a collar neighborhood of $M$;
for example, see Theorem 2 in~\cite{kwasik-rosicki-04} for some possible phenomena.

Finally, we put further conditions on the tuple
$(\underline\gamma_1,\underline\gamma_2,v_1,v_2)$ to guarantee
that the set $V$ is a tubular neighborhood of the boundary. First, in each component of the regular open set \[V_1\cong\bigsqcup_{i=1}^{\infty} M_0\times (0,1),\] we choose a preferred copy of $M_0$, say $M_0\times \{1/2\}$. We can directly access points in $M_0\times \{1/2\}$ because we have parametrized balls covering each component of $V_1$. Moreover, because the bundle structure on each component of $V_1$ is  parametrized by a single tuple of group elements, we may coherently identify copies of $M_0$ in each component of $V_1$ separately. The components of $V_1$
naturally have order type $\omega$. That is, $V_1$ is a scattered regular open set as is forced by the formula $\on{seqbdle}_n$, and all of its essential accumulation points lie in $\partial M$. In particular, only finitely many components of $V$ meet any compact subset of $M\setminus\partial M$.
We obtain a canonical labeling of the copies of $M_0$ in each component, which we write $\{M_0^i\}_{i\in\omega}$.

Now, let $x\in M_0$, and write $x_0\in M_0^0$ be the corresponding
point. There is a copy of $\bR$ in the fiber direction passing through
$x_0$, which meets $x_i\in M_0^i$ for all $i\in\omega$, since the
parametrized bundle structures were chosen coherently. We require
that there exists a unique \[y_x=\lim_{i\to\infty} x_i\in N\in\pi_0(\partial M),\] which is then an accumulation point of the sequence $\{x_i\}_{i\in\omega}$. Because we have direct access to points in $\partial M$, the existence and uniqueness of such a point $y_x$ is first order expressible.

To guarantee that $V\cup N\cong N\times (0,1]$ is a tubular neighborhood of the boundary component $N$, we need only require that the map $x\mapsto y_x$ is a continuous bijection. Guaranteeing that it is bijective is trivial. To guarantee continuity, it suffices to guarantee that if $z_i\to x$ is a convergent sequence in $M_0$ then $y_{z_i}$ is a convergent sequence in $N$, which is similarly straightforward.

Combining this discussion, we have that following.

\begin{cor}\label{cor:collar}
There is a formula $\on{collar}(u)$ such that \[\models\on{collar}(U)\]
if and only if $U$ is a collar neighborhood of the boundary of $M$.
\end{cor}

\iffalse
\section{Sketch of the construction of the collar}

To begin with one notes it is trivial to write down a formula $seqbdl_{n}(\underline{\gamma},v)$ which holds for $(\underline{g},V)$ if $V$ is a disjoint union of an infinite chain of connected components with disjoint closures such that each of them $V_{0}$ satisfies $bdle_{n}(V_{0})$, as witnessed by some tuple of group elements extending $\underline{g}$ (that is fulfilling the role of $\underline{\gamma}$ in the formula $bdle_{n}(u)$ [it might be worth renaming the intermediate formula in which the outermost block of variables of $bdl_{n}$ are not quantified.).

The somewhat less trivial part is to show that in fact for any collared neighbourhood $U\cong\partial M_{0}\times(0,1]$ of some component $\partial M_{0}$ of $\partial M$ and any subset $V\subseteq U$ which is the image of some set of the form $\sqcup_{i\in\omega}V_{l}$ with $V_{l}$ in correspondence by the homeomorphism above with $J_{l}\times\partial M$, where $J_{l}$ is an open interval, there exist some $g\in G$ such that $\models seqbdl(g,V)$ holds. For this, it suffices to consider a sequence of coverings $\mathcal{W}^{l}=\{W^{l}_{i}\}_{i=1}^{N}$ of $\partial M_{0}$, where the connected components of $W^{l}_{i}$ have disjoint closures and have diameter $D_{n}$ tending to $0$ with $n$. One can then define $g_{i}$ on a union of ring-like open sets, $R_{i}^{l,\hat{W}}$ where $1\leq i\leq N$, $l\in\omega$ and $\hat{W}$ ranges among all connected components of $W^{l}_{i}$ so that $R_{i}^{{l,\hat{W}}}$ intersects $V^{l}$ in two components:
$C_{0}$ and $C_{1}$, where $C_{0}$ is in bijection with $W_{0}\times J_{l}$ and its flow lines intersect said set in fibers of the form ${w}\times J_{l}$. It is easy to see one can in fact do it in such a way that $\lim_{l\to\infty}sup_{i,\hat{W}}diam(R_{i}^{l,\hat{W}})=0$. This guarantees that $g_{i}$ as defined on the union of all
$R_{i}^{l,\hat{W}}$ extends continuously to the entire manifold.

Notice that the data that the formula $bdl_{n}$ quantifies existentially includes collection of the sets $C_{0}$. Since being in the same orbit by the flow defined by $g_{i}$ is defined (uniformly in any such $g$) by a formula with parameter $g$, it follows that the same holds for the relation on $V_{l}$ under which two points are equivalent if and only if they belong to the same fiber $\{w\}\times J_{l}$ for one of the sets $C_{0}$ as above and the same applies trivially to the intersection of $\cl C_{0}$ with $\partial V_{l}$.

One can then consider a formula $altbdl_{n}(\underline{\gamma}^{1},\underline{\gamma}^{2},v^{1},v^{2})$ that holds for
$(\underline{\gamma}^{1},\underline{\gamma}^{2},V_{1},V_{2})$ whenever $seqbdl_{n}(\underline{g}^{i},V^{i})$ holds, the components of $V^{1}$ and $V_{2}$ form a chain with respect to to the $adbdl_{n}(u,v)$ relation and $U=V^{1}\oplus V^{2}$ contains a unique boundary component $\partial M_{0}$ of $M$.

We then need to define a formula $longflw_{n}(\underline{\gamma}^{1},\underline{\gamma}^{2},v^{1},v^{2},\pi,\xi)$ that holds for $(\underline{g}^{1},\underline{g}^{2},V^{1},V^{2},p,q)$ if and only if $p$ and $q$ are related by the transitive closure of the union of the fiber relations on the closure of each of the components of $V^{1}$ and $V^{2}$. If we were allowed to quantify over all closed sets this would be immediate, since then it would suffice to be able to assert that $q$ belongs to the smallest closed set in $\tilde{U}:=\inte M\cap U$ (closed relative to $\inte M$) $F_{p}$ that containis $p$ and is closed under each of the fiber relations on the components of $V^{1}$ and $V^{2}$, which as we have seen are definable with parameters $(\underline{g}^{1},V^{1})$ and $(\underline{g}^{2},V^{2})$ respectively. We cannot guarantee as much. Notice however that it suffices to be able to quantify over a collection $\mathcal{F}$ of closed sets so that some first order statement in terms of $(\underline{g}^{1},\underline{g}^{2},V^{1},V^{2})$ implies that $F_{q}\in\mathcal{F}$. This is now easy, since $\models altbdl_{n}(\underline{g}^{1},\underline{g}^{2},V^{1},V^{2})$ ensures that $F_{q}$ is homeomorphic to a ray whose complement can be expressed as the intersection with $\inte M$ of the union of three regular open sets in $M$ (by considering the complement of a small cylinder around the ray and a partition of the cylinder into two regular open sets).

We will henceforth refer to the collection of points in $V^{1}\oplus V^{2}$ that are $longflw_{n}(\underline{g}^{1},\underline{g}^{2},V^{1},V^{2})$-related to $q$ simply as the fiber of $p$.

Once this is done pick $(\underline{g}^{1},\underline{g}^{2},V^{1},V^{2})$ satisfying $altdl_{n}$. One can require further first order conditions on the tuple above ensuring the following is satisfied.
First of all, for every $q\in\tilde{U}$ the fiber $F_{q}$ has a unique accumulation point $f(q)\in\partial M_{0}$. Notice that the formula $altbdl_{n}$ already ensures that $\cl U\cap\inte M$ is homeomorphic to $N\times[0,1)$ by a homeomorphic sending $Fr U$ onto $N\times\{0\}$ and that $N$ contains a single accumulation point of each such fiber $F_{q}$. We thus have a well-defined map $f:\fr U\to \partial M_{0}$ which is definable with parameter $(\underline{g}^{1},\underline{g}^{2},V^{1},V^{2})$ and it is a trivial matter to further impose the condition that $f$ is a homeomorphism between $\fr U$ and $\partial M_{0}$. This guarantees that the homeomorphism above extends to a homeomorphism
between $\cl U$ and $N\times[0,1]$ sending $N\times{1}$ to $\partial M_{0}$.
\fi

\section{Completing the proof}\label{sec:homeo}

Cheeger and Kister~\cite{CK1970} proved that there exist only countably many homeomorphism types of compact manifolds. A key step in their proof was that the topological type of a manifold is invariant under ``small'' perturbations, in some quantitatively precise sense, of parametrized coverings of the manifold.
As more concretely described below,
this step will be crucial for the construction of the sentences $\phi_M^{(\vol)}$.

For each positive integer $k$, we denote by  $\EE(n,k)$  the set of all $k$--tuples $\underline{f}=(f_1,\ldots,f_k)$
of embeddings
\[
f_j\co B^n(2)\longrightarrow \bR^{2n+1}\]
such that the following hold:
\begin{itemize}
\item $C(\underline{f}):=\bigcup_j \im f_j$ is a compact manifold;
\item If $C(\underline{f})$ is closed, then $C(\underline{f})=\bigcup_{j}  f_j \left(B^n(1)\right)$;
\item If $C(\underline{f})$ has boundary, then there exists a collar $U_\partial$ of $\partial C(\underline{f})$ such that
$C(\underline{f})\setminus U_\partial=\bigcup_{j}  f_j \left(B^n(1)\right)$.
\end{itemize}

Every compact $n$--manifold $M$ is homeomorphic to $C(\underline{f})$
for some $\underline{f}\in \bigcup_k\EE(n,k)$, which we call as a \emph{parametrized covering} of $M$.
The space $\EE(n,k)$ inherits the uniform separable metric from $C^0(B^n(2),\bR^{k(2n+1)})$. The proof of Cheeger and Kister essentially boils down to the following rigidity result,
along with a deep result of Edwards and Kirby
on
deformation of embeddings in manifolds~\cite{EK1971}.
\begin{lem}\cite{CK1970}\label{lem:ck}
For each $\underline{f}\in\EE(n,k)$, there exists $\epsilon>0$ such that
    	every $\underline{ g}\in\EE(n,k)$ that is at most $\epsilon$--far from $\underline f$
    	satisfies \[
     C(\underline{f})\cong C(\underline{g}).\]
    \end{lem}

We choose a sufficiently small $\epsilon>0$ for which the conclusion of Lemma~\ref{lem:ck} holds, and call it as a \emph{Cheeger--Kister number} of $\underline f\in\EE(n,k)$;
for our purpose we can further require $\epsilon$ to be rational.

Our strategy of proving Theorem~\ref{thm:main} is providing a sentence in $L_{\agape}$ that is modeled by an input manifold $M$ such that the sentence holds for the structure $\agape(N,G)$
iff $N$ admits an embedding into Euclidean space that is within the Cheeger--Kister distance of a fixed parametrized covering of $M$.

Let us recall the notation $h_{U,\underline{g},p}$ from Proposition~\ref{prop:parametrize}. To execute the strategy above,  suppose we have  $(M,G)\in\cM_{(\vol)}$ with $\dim M=n$
and
\[f_1,\ldots,f_k\in C^0(B^n(2),\bR^{2n+1}).\]
Let us consider the following condition:
there exist some $U_1, \ldots, U_k\in \ro(M)$ not touching $\partial M$,
some open collars $U_\partial\sse V_\partial$ of $\partial M$,
some points $p_1,\ldots,p_k$ of $\inte M$,
 and some $n$--tuples $\underline{g}_1,\ldots,\underline{g}_k\in G^n$
 such that all of the items below hold with respect to
 the homeomorphism
\[ h_i:=h_{U_i,\underline{g}_i,p_i}\co B^n(2)\to \cl U_i\sse\inte M\]
\be[(a)]
\item\label{p:emb3} each $f_i$ is an embedding;
\item\label{p:emb1}
we have that $\bigcup_i \im h_i=M\setminus U_\partial$;
\item\label{p:emb2}
we have that $\bigcup_i h_i(B^n(1))=M\setminus V_\partial$;
\item\label{p:emb4} for all $1\le i,j\le k$, whenever $x\in U_i\cap U_j$ we have \[f_i\circ h_i^{-1}(x)=f_i\circ h_i^{-1}(y).\]
\ee
In particular, the tuple $\underline{f}=(f_1,\ldots,f_k)$ is a parametrized cover of $M\setminus U_\partial$.

By the preceding results, there exists a formula $\on{Embed}(\chi_1,\ldots,\chi_k)$ expressing the combinations of the above conditions for $\chi_i=f_i$ in $\agape(M,G)$.
We emphasize that although the maps $h_i$ do not belong to the universe of $\agape(M,G)$,  Proposition~\ref{prop:detect-dim}
and Corollary~\ref{cor:collar} along with our access to the real numbers enable us to have such expressions.
The converse is also immediate:

\begin{lem}\label{lem:emb}
For each compact connected  manifold $M$ with $n:=\dim M$,
there exist $f_1,\ldots,f_k\in C^0(B^n(2),\bR^{2n+1})$ such that \[\agape(M,G)\models\embed_n(f_1,\ldots,f_k).\]
\end{lem}

    We can now establish the main result of this paper.
    \begin{proof}[Proof of Theorem~\ref{thm:main}]
Recall we may assume $n:=\dim M>1$.
Setting $\ell:=2n+1$, we have a parametrized covering
\[\underline{f}=(f_1,\ldots,f_k)\in\EE(n,k)\sse C^0(B^n(2),\bR^{k\ell})\] of $M$.
We have a corresponding Cheeger--Kister rational number $\epsilon=\epsilon(M,\underline{f})>0$.
    Let us pick  $\delta>0$ such that \[\sup_{|x-y|\le \delta}| \underline{f}(x)-\underline{f}(y)|<\epsilon/3.\]
    We can find a partition $\{C_1,\ldots,C_s\}$ of $B^n(2)$ having diameters less than $\delta$ such that
    each $C_i$ is the intersection of $B^n(2)$ with a cube with rational corners,
    after suitably choosing equalities and inequalities for the faces.
    Using that a rational number is ($0$--)definable in $L_{\agape}$,
    we can require that each $C_i$ is definable as well.
    We also arbitrarily pick $x_i$ in $C_i$, and choose $q_i\in\bQ^{k\ell}$ such that
    \[
    |\underline{f}(x_i)-q_i|<\epsilon/3.\]

Let us now consider the following conditions
for an arbitrary $(N,G)\in\cM_{(\vol)}$, which are first order expressible in $L_{\agape}$ by preceding results:
\be[(a)]
\item $\dim N=n$;
\item some $\underline{g}\in C^0(B^n(2),\bR^{\ell})^k=C^0(B^n(2),\bR^{k\ell})$ satisfies that \[\agape(N,G)\models \embed_n(\underline{g}),\]
and that
\[\sup_{x\in C_i}| \underline{g}(x)-q_i|<\epsilon/3.\]
    \ee
The above conditions are obviously met in the case when $N\cong M$.
We also note for each $x\in C_i$ that
    \[
    |  \underline{g}(x) - \underline{f}(x)|
    \le
    |  \underline{g}(x) - q_i| + |q_i - \underline{f}(x_i)| +  |\underline{f}(x_i) - \underline{f}(x)|<\epsilon.\]
By Lemma~\ref{lem:ck}, we see that $N$ is homeomorphic to $M$.\end{proof}
\iffalse
\subsection{\sam{Do we need this?}}
We now generalize the above proof to bounded manifolds. The main difficulty is
that we cannot directly parametrize the boundary of a manifold $M$ using flows (as in Section~\ref{sec:balls}); in other words, the above compact sets $\cl U_i$ can only be required to be contained in $ M\setminus\partial M$.
The basic idea for the bounded case is that
we excise a neighborhood $U$ of the boundary $\partial M$ that is an extendable collar neighborhood of the boundary;
this is possible by Brown~\cite{Brown1962}.
The result is that $M\cong M\setminus U$. Since the frontier of $U$ in $M$ lies in the interior of $M$, it is then possible to parametrize the boundary
of $M\setminus U$ and leverage the Cheeger--Kister methods.

We begin with a regular open subset $U_0$ of $M$ satisfying $\collar(U_0)$;
in particular,  we have $M\cong M\setminus U_0$.
There exist a parametrized covering $\{U_i\}_{1\le i\le k}$ of the compact manifold $M\setminus U_0$ such that $\flws(U_i,\underline{g_i},p_i)$ holds for some $\underline{g_i}\in \Homeo(M)^n$ and $p_i\in M$; modifying $U_0$ if necessary, we can further require that
those $U_i$ meeting  $\fr(U_0)$

Setting $\ell:=2n+1$ as before, we get a map
\[\underbar u\co B^n\longrightarrow\R^{k\ell}\] which comes from this parametrized covering $\{U_i\}_{1\le i\le k}$.
The existence of such $\{U_0\}\cup\{U_i\}_{1\le i\le k}$ is first order expressible in $L_{\agape}$.

We build a finite--valued approximating map that is within half of the Cheeger--Kister number on the boundary and in the interior of
$M\setminus U_0$. Finally, any map \[B^n\longrightarrow\R^{k\ell}\] satisfying
the above conditions for $\{U_i\}$ and compatibility condition (i.e.part \ref{p:emb4} in Lemma~\ref{lem:emb}) that is within half of the Cheeger--Kister constant on the approximating map will witness that
the union of the images of the balls is homeomorphic to $M\setminus U\cong M$.
\fi

\iffalse
\begin{lem}
	\label{l: recognizing boundary points} There exists some formula $bd(\pi)$ such that $\models\pi(p)$ if and only if
	$p\in\partial M$.
\end{lem}
\begin{proof}
	Simply let
	$$
	bd(\pi):=\neg(\exists\underline{\gamma}\exists u\exists \pi')\,\,flows(\underline{\gamma},u,\pi')\wedge\pi\in u
	$$
\end{proof}

\begin{lem}
	\label{l: interior bundles2}There exists formulas $bdle_{n}(u),adbdle_{n}(u,v)$ such that
	\begin{itemize}
  		\item whenever $dim(M)=n$ we have that $\models bdle_{n}(U)$ if and only if $M\setminus \cl U$ has two connected components, $\cl U$ is contained in $\inte M $ and it is homeomorphic to a product $I\times M_{0}$, where $M_{0}$ is a closed $(n-1)$-dimensional manifold and $U\cong(0,1)\times M_{0}$
  		\item if $\models bdle_{n}(U)\wedge bdle_{n}(V)$ holds then $\models adbdle_{n}(U,V)$ holds if and only if $\fr U$ has some boundary component in common with $\fr V$
	\end{itemize}
  \end{lem}
\begin{proof}
	Write
		$	\underline{\gamma}=(\gamma_{1},\dots \gamma_{2^{2n-1}})$,$\underline{v}=(v_{1},\dots v_{2^{2n-1}})$.
  			 \todo{probably need to change this number to something more like $3^{2n-1}$}

  	Our formula is constructed as simply saying that $U$ is obtained as a union of $(0,1)$-fibered open sets, where the fibrations agree on any pair-wise intersection and the fibration extends to the closure:
 \begin{align*}
	bdle_{n}(u)\equiv&cc_{2}(u^{\perp})\wedge\exists\underline{\gamma}\exists\underline{v}\exists\underline{v}'\,\,(u=\bigcup_{j=1}^{2^{2n+1}}v_{j}\wedge\bigwedge_{j=1}^{2^{2n-1}}(v_{j}\subseteq v'_{j}\wedge cfibr(\gamma_{j},v_{j})\wedge\\
	&\forall\pi\in v_{j}\exists\underline{\delta}\exists w\exists\pi_{0}\,\,[w\subseteq v_{j}\wedge flows(\underline{\delta},\gamma,w,\pi_{0})\wedge\\
	&\forall\pi_{1},\pi_{2}\,((\pi_{1}\in w\wedge\pi_{2}\in v_{j}\wedge orb(\gamma_{j},\pi_{1},\pi_{2}))\longrightarrow\pi_{2}\in w)]\\
		&\bigwedge_{1\leq j_{1}<j_{2}\leq 2^{2n+1}} \forall\hat{v}_{1},\hat{v}_{2}\,\,((\bigwedge_{\ell=1}^{2}cc(\hat{v}_{\ell},v_{j_{\ell}})\longrightarrow comp(\gamma_{j_{1}},\gamma_{j_{2}},\hat{v}_{1},\hat{v}_{2}))))
 \end{align*}
 where $orb(\gamma,\pi_{1},\pi_{2})$ is the obvious formula expressing the fact that $\pi_{1}$ and $\pi_{2}$ are in the same orbit with respect to the flow defined by $\gamma$, the formula $cfibr(\gamma,v)$ expresses the fact that the intersection of any fiber of the flow defined by $\gamma$ with $v$ is connected and
the formula $comp(\gamma_{1},\gamma_{2},w_{1},w_{2})$ expresses the fact that the flows defined by $\gamma_{1},\gamma_{2}$ agree on $\cl w_{1}\cap \cl w_{2}$, which is a union of full orbits by the flow on both $w_{1}$ and $w_{2}$:
 \begin{align*}
  		cfibr(\gamma,v)\equiv \neg\exists \rho_{1},\dots \rho_{4}\exists\pi_{1},\dots \pi_{4}\,\,\bigwedge_{i=1}^{3}cord_{\sq}(\rho_{i},\rho_{i+1},\rho_{(i+2)\div 4})\wedge\\
  		\exists\pi\,\bigwedge_{i=1}^{4}param_{1}(\gamma,\pi,\rho_{i})\wedge \bigwedge_{k=1}^{2}(\pi_{2i}\in v\wedge\pi_{2i+1}\notin v)\\
  		comp(\gamma_{1},\gamma_{2},w_{1},w_{2})\equiv \forall\delta_{1},\delta_{2}\forall u_{1},u_{2}\forall\rho\,\,(\bigwedge_{i=1}^{2}w_{i}\subseteq u_{i}\wedge\bigwedge_{i=1}^{2}conv(\gamma_{i},\delta_{i},u_{i},\rho)\rightarrow\\
  	  \forall\pi\in \cl w_{1}\cap \cl w_{2}\,\,\bigwedge_{i=1}^{2}(\delta_{i}\cdot p\in w_{i}\longrightarrow(\delta_{3-i}\cdot p\in w_{3-i}\wedge\delta_{1}^{-1}\delta_{2}\cdot p=p))
 \end{align*}
  The fact that the covering of $U$ can be taken to be the collection of connected components in $2^{2n-1}$ open sets follows from
  the discussion in \ref{}. We now can write:
  \begin{align*}
  	adbdle_{n}(u,v)\equiv\exists u_{0}\,\,bdle_{n}(u_{0})\wedge \cl u_{0}\subseteq u\wedge \exists w\,\,(cc(w,u_{0}^{\perp}\cap u)\wedge w\cap\fr u\subseteq \fr v)
  \end{align*}
\end{proof}

\begin{cor}
	There exists some formula $\partial collar(u)$ which holds for $U\in\ro(M)$ if and only if $\partial M\subseteq U$ and $U$ is an \ja{extendable} open collar of $\partial M$.
\end{cor}
\begin{proof}
	We will omit making the following formulas explicit, since in this case this does not seem very elucidatory. We can characterize the property in question as follows:
	\begin{itemize}
		\item $\fr M\subseteq U$
		\item Every connected component $\hat{U}$ of $U$ can be written as $\hat{U}_{1}\oplus \hat{U}_{2}$, where $U_{1}\cap U_{2}=\emptyset$.
		\item Each connected component of the $\hat{U}_{i}$ above satisfies the formula $bdle_{n}$.
		\item The graph structure induced on the collection $\pi_{0}(\hat{U}_{1})\cup\pi_{0}(\hat{U}_{2})$ by the relation $adbdle_{n}(u,v)$ is isomorphic to a single infinite ray. The fact that this is first order expressible follows from the same arguments used in part \ref{} of Section \ref{}.
		\item $M\cap \hat{U}^{\perp}$ is non-empty and connected.
		\item For each $\hat{W}\in\pi_{0}(\hat{U}_{1})$ we have that $M\cap W^{\perp}$ has two connected components there is one of them $V$ such that $\fr M\cap V=\fr M\cap\cl \hat{U}$
		\item $\cl U\subseteq U'$ for some $U'$ that also satisfies all the conditions above
	\end{itemize}
\end{proof}

\fi

\section{Further questions}\label{sec:questions}
A large number of interesting open questions remain. We already mentioned Question~\ref{que:homeo-action}.
Part of the motivation for this question is the theory of critical regularity of groups, which seeks to distinguish between diffeomorphism groups of various regularities of a given manifold by the isomorphism types of finitely generated subgroups; cf.~\cite{KK2020crit,Mann:aa}.
Along this line, one may ask whether or not the $C^k$--analogue of Theorem~\ref{thm:main} holds.

    \begin{que}\label{que:first-order-diffeo}
    Let $M$ be a compact, connected, smooth manifold, and let $N$ be an arbitrary smooth manifold. Is there a sentence $\phi_{k,M}$
    in the language of groups such that if $\Diff^k(N)$ satisfies $\phi_{k,M}$ then $N$ is $C^k$--diffeomorphic to $M$?
    \end{que}

    Relatedly, leaving the framework of first order rigidity, we have the following.

    \begin{que}\label{que:critical-reg}
    Let $M$ be a compact, connected, smooth manifold. Is there a finitely generated (or countable) group $G_M$ such that $G_M$
    acts faithfully by $C^k$ diffeomorphisms of a manifold $N$ if and only $N$ is $C^k$ diffeomorphic to $M$?
    \end{que}

    The discussion in the present article depended heavily on the compactness of the comparison manifold.

    \begin{que}\label{que:noncompact}
    Let $M$ be an arbitrary manifold. Under what conditions is there a sentence $\phi_M$ in the language of groups
    such that if $N$ is an arbitrary manifold then
    $\Homeo(N)$ satisfies $\phi_M$ if and only if $N$ is homeomorphic to $M$?
    \end{que}

    We conclude by asking what the weakest hypotheses on $\cH$ can be.

    \begin{que}\label{que:minimal assumptions}
    For what classes of subgroups of $\Homeo(M)$ do the conclusions of Theorem~\ref{thm:main}
    hold?
    \end{que}

\section*{Acknowledgements}
The first and the third author are supported by Samsung Science and Technology Foundation under Project Number SSTF-BA1301-51. The first and the third authors are also supported by KIAS Individual Grants (MG073601 and MG084001, respectively) at Korea Institute for Advanced Study. The second author is partially supported by NSF Grant DMS-2002596. The authors are grateful to M.~Brin, J.~Hanson, O.~Kharlampovich, and C.~Rosendal for helpful discussions.

  \bibliographystyle{amsplain}