% Ian Pratt, Dominik Schoop  Kluwer general version
% klu_axiom.tex
%
% An axiom system for polygonal mereotopology of the real closed plane
%
% last change: 15/10/96, 16/10/, 17/10/, 18/10, 22/10/, 28/10/, 29/10, 30/10, 
%              31/10, 1/11, 3/11, 4/11, 5/11,9/11,3/12,10/12,12/12,6/1/97, 17/1
%              3/2, 4/2, 5/2, 6/2, 7/2, 10/2, 11/2, 6/3, 7/3, 9/3, 10/3, 12/3, 
%              13/3, 14/3, 17/3, 19/3, 21/3, 13/3/98, 15/3, 17/3, 18/3, 19/3
%              10/6

\documentclass[numreferences]{kluwer}
\newcommand{\dson}{\renewcommand{\baselinestretch}{1.5}\large\normalsize}
\newcommand{\dsoff}{\renewcommand{\baselinestretch}{1}\large\normalsize}


\newcommand{\ewh}[3]{\setlength{\epsfxsize}{#2}\setlength{\epsfysize}{#3}
  \epsfbox{#1}}
\newcommand{\ew}[2]{\setlength{\epsfxsize}{#2}\epsfbox{#1}}
\newcommand{\eh}[2]{\setlength{\epsfysize}{#2}\epsfbox{#1}}
\newcommand{\R}{{\rm I\!R}}
\newcommand{\lb} {\:[\![}
\newcommand{\rb} {]\!]\:}

\usepackage{graphicx}
\usepackage{epsfig}

\newcommand{\N}{{\rm I\!N}}
\newcommand{\Q}{{\sf Q\hspace*{-1.1ex}\rule{0.15ex}%
{1.5ex}\hspace*{1.1ex}}}
\newcommand{\C}{{\sf C\hspace*{-0.9ex}\rule{0.15ex}%
{1.3ex}\hspace*{0.9ex}}}

\newcommand{\fR}{\ensuremath{\mathfrak{R}}}      % fraktur R for model
\newcommand{\fS}{\ensuremath{\mathfrak{S}}}      % fraktur S for model
\newcommand{\fQ}{\ensuremath{\mathfrak{Q}}}      % fraktur Q for model
\newcommand{\fP}{\ensuremath{\mathfrak{P}}}      % fraktur P for model
\newcommand{\fA}{\ensuremath{\mathfrak{A}}}      % fraktur A for model
\newcommand{\cL}{\ensuremath{\mathcal{L}}}       % caligraphic L for language
\newcommand{\F}[1]{\ensuremath{\mathcal{F}(#1)}} % frontier with one parameter
\newcommand{\proof}[1]{{\bf Proof:} #1 \boxterm} % Proof: ...  box
\newcommand{\boxterm}{\hspace*{\fill} $\Box$ \\ \vspace{0.25cm} \\ \noindent}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{remark}[theorem]{Remark}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{observation}[theorem]{Observation}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{claim}{Claim}


\setlength{\unitlength}{0.75mm}
\setcounter{tocdepth}{3}

\input{epsf}
\begin{opening}


\title{A complete axiom system for polygonal mereotopology of the real plane}
%\subtitle{graphics as formal languages}

%\dedication{This paper has not been submitted elsewhere in identical or similar form.}

\author{Ian \surname{Pratt}
}

\author{Dominik \surname{Schoop}}
\institute{Department of Computer Science \\ 
            University of Manchester,\\ Manchester, U.K.}
\date{March 1998}
\end{opening}


\hyphenation{two-dimen-sional}
\hyphenation{super-scripts}


\begin{document}
\begin{ao}
Department of Computer Science, \\
           University of Manchester, Oxford Road, Manchester, M13 9PL, United Kingdom
\end{ao}                   

\begin{abstract}
This paper presents a calculus for mereotopological reasoning in which 
two-dimen\-sional spatial regions are treated as primitive entities.  A 
first order predicate language \cL~with a distinguished unary predicate 
$c(x)$, function-symbols $+, \ .\ $ and $-$ and constants $0$ and $1$ is 
defined.  An interpretation \fR~for \cL~is provided in which polygonal open 
subsets of the real plane serve as elements of 
the domain. Under this interpretation the predicate $c(x)$ is read as 
``region $x$ is 
connected'' and the function-symbols and constants are given their 
meaning in terms of a Boolean algebra of polygons. 
We give an alternative interpretation \fS~based on the real closed plane 
which turns out to be isomorphic to \fR.
A set of axioms and a rule of inference are introduced.  We 
prove the soundness and completeness of the calculus with respect to the 
given interpretation.

\noindent
{\bf Keywords: } mereology, topology, logic, spatial, reasoning
\end{abstract}

\section{The problem}

As anyone who has read a book on point-set topology knows, Euclidean
spaces contain regions which could not possibly be useful for
representing the shapes of everyday objects. Fractal dust,
infinitely convoluted boundaries and other pathological constructions
simply do not arise in the world of desks and chairs arranged in a
room, or of plots of land drawn on a map, or of electronic components
etched on a silicon chip.  They are mere artifacts of a model of space
according to which all spatial entities are sets of points, and all
spatial properties are analysable in terms of the metric relations
between points.

Perhaps, then, we can develop more efficient and parsimonious ways of
representing and reasoning about space by taking regions, rather than
points, as primitive. The best known theory of this kind is
Tarski's \cite{Tarski56b} axiomatization of Euclidean geometry based
on spheres. But the policy of taking regions as primitive is perhaps
most attractive when considering problems involving mereological
(part-whole) and other topological notions---that is, where no metric
information is to hand.  Recent interest in ``mereotopology'', much of
it from within the AI community, dates from the work of
Clarke~\cite{clarke81},\cite{clarke85}, following earlier work of
Whitehead~\cite{whitehead29}. See, for example, Randall, Cui and
Cohn~\cite{Randell+92}, Gotts, Gooday and Cohn~\cite{Gotts+96}, and
Borgo, Guarino and Masolo~\cite{Borgo+96}.

A {\em mereotopological calculus} is an axiomatic system in a formal
language whose variables are to be thought of as ranging over spatial
regions, and whose nonlogical constants are to be thought of as
expressing primitive topological properties and relations involving
these regions.  Mereotopological calculi vary as to which primitives
they employ, and the axioms they propose.  Clarke's calculus has a
single binary relation of ``connection'' with the gloss that two
regions are connected if they share a common point.  Randall, Cui and
Cohn also use a binary connection relation, but take two regions be
connected if their {\em closures} share a common point.  Borgo,
Guarino and Masolo, by contrast, use a primitive ``part-of'' relation
(the mereological component) together with a primitive property of
``self-connectedness'' (the topological component).  However, all
three approaches are motivated by the prospect of an adequate account
of space in which regions are not identified with sets of
points.

With any such calculus, the question arises as to whether the proposed
axioms constitute a {\em good} theory of space---one that will lead to
{\em correct} inferences about the everyday situations whose spatial
features the calculus purports to model. More technically, we must ask
whether physical space---at least approximately, and on everyday
scales---is a model of the proposed axioms under the intended
interpretation, and if so, how completely those axioms capture its
features.  This question has been answered for Clarke's system by
Biacino and Gerla~\cite{BiacinoGerla96}, who prove a completeness result
guaranteeing that the regular sets of a Euclidean space are a model of
Clarke's axioms (regular sets are explained below).  This result is
of interest because, whatever their faults, $\R^{2}$ and $\R^{3}$ are
at least known to be workable models of physical space.
Unfortunately, as Biacino and Gerla note, under the proposed
interpretation, the language really allows only mereological
relations to be expressed. In particular, Clarke's
suggestions for capturing topological notions such as, for example,
the relation of two objects' touching tangentially, do not have the
desired effect.  So although Biacino and Gerla's theorem is the kind
of result needed to validate a mereotopological calculus, the
particular interpretation to which it applies is too weak to be
topologically interesting.

Another approach to mereotopology in which semantics plays an
important part is taken by Asher and Vieu~\cite{AsherVieu95}.  They present a
calculus---also based on a binary relation of connection---together
with a formal semantics in which the individuals are identified with
certain subsets of a particular type of topological space. Soundness
and completeness proofs are duly provided.  Unfortunately, Asher and
Vieu's topological spaces are strange objects, far removed from the
standard Euclidean model of space. (In particular, as Asher and Vieu
point out, these spaces are not dense.) While Asher and Vieu would
reply that their aim is to present a mereotopological theory
responsive to the demands of modelling cognition and natural language,
rather than to reconstruct the mereotopology of Euclidean space, the
radical nature of their models makes the axioms hard 
to assess.

In this paper, we present a mereotopological calculus for
2-dimensional spatial reasoning. Our axiom system, though considerably
more complex than others that have been proposed, has the advantage of
being sound and complete with respect to a familiar and topologically
nontrivial spatial interpretation. By {\em familiar}, we mean a
spatial interpretation based on an ontology known to provide a
workable model of physical space.  By {\em topologically nontrivial},
we mean one under which the formulae of the calculus express a wide
range of topological (not just mereological) properties and
relations.  Thus, although regions are still regarded as primitive
{\em within} the calculus, the axiom system is shown to characterize a
familiar spatial ontology of proven utility.

\section{A mereotopological calculus}
%
\subsection{The syntax of $\cL$}
%
Formally, $\cL$ is a first-order language 
with equality, having the nonlogical constants $c(x)$, $0$, 
$1$, $-$, $+$ 
and $\ . \ $,
where $c(x)$ is a 1-place predicate,
$0$ and $1$ are constant symbols,
$-$ is a 1-place function symbol 
and $+$ and $\ . \ $ are 2-place function symbols.
%
In other words, $\cL$, is the language of Boolean
algebra with a distinguished predicate $c(x)$. 

Having defined our mereotopological language, we give a formal
semantics in terms of familiar spatial constructions. We stress that
the calculus itself cannot talk about these constructions: as far as it
is concerned, spatial regions are primitive, and the interpretations
of its nonlogical constants are simply functions and relations
defined over these primitives. But the familiar interpretation will
guarantee that our mereotopological calculus really is an appropriate
calculus for spatial reasoning.

In fact, we present two formal models for our
mereotopological language $\cL$, which we denote $\fR$ and $\fS$ and which turn out to be isomorphic. We 
begin with the more intuitive of the two.
%
\subsection{The model $\fR$}
%
Our first task is to establish our domain of interpretation, $R$.
It is now fairly standard in treatments of mereotopology to confine
attention to {\em regular} sets.
\begin{definition}
Let $X$ be a topological space and $x \subseteq X$. Then the set
 $\bigcup\{y \subseteq X | y $ open, $ y \cap x = \emptyset\}$ is an open set in 
$X$ called the {\em pseudocomplement of} $x$, written $x'$. We say 
that $x \subseteq X$ is {\em regular} if $x = x''$.
\label{def:regular}
\end{definition}

The following well-known theorem underlies the 
importance of the regular sets to mereotopology. We state it here 
without proof. (See, e.g.~Johnstone~\cite{Johnstone82}, chapter I,
section 1.13.)
\begin{theorem}
Let $X$ be a topological space. Then the set of regular sets in $X$ 
forms a Boolean algebra ${\rm RO}(X)$ with
top and bottom defined by $1 = X$ and $0 = \emptyset$, and Boolean 
operations defined by $x . y = x \cap y$,  $x + y = (x \cup y)''$ and
$-x = x'$. 
\label{theo:1:regular}
\end{theorem}
Let $\R^2$ denote the real plane with the usual Euclidean topology.
Our domain $R$ will form a Boolean subalgebra of
${\rm RO}(\R^2)$. 

\begin{figure}
\begin{center}
\begin{minipage}{5cm}
\resizebox{5cm}{!}{\includegraphics{axiom.fig1a.eps}} \\
a) Three regular sets (each differently shaded)
\end{minipage} \hspace{1cm}
\begin{minipage}{5cm}
\resizebox{5cm}{!}{\includegraphics{axiom.fig1b.eps}} \\
b) Three nonregular sets
\end{minipage} \hspace{1cm}
\end{center}
\begin{center}
\begin{minipage}{5cm}
\resizebox{5cm}{!}{\includegraphics{axiom.fig1c.eps}}\\
c) Three pairs of regular sets and their sums 
\end{minipage} \hspace{1cm}
\begin{minipage}{5cm}
\resizebox{5cm}{!}{\rotatebox{-90}{\includegraphics{axiom.fig1d.eps}}} \\
d) Three polygons (each differently shaded)
\end{minipage} \hspace{1cm}
\end{center}
\caption{Some regular sets of the plane and their Boolean combinations} 
\label{fig:intuition}
\end{figure}
Before turning to its construction, let us pause to fix our 
intuitions 
about ${\rm RO}(\R^{2})$. 
Basically, we can think of regular sets in $\R^{2}$ as open sets with 
no internal cracks or point-holes (compare fig.~\ref{fig:intuition}a with
fig.~\ref{fig:intuition}b).
The product, $x.y$, of two regular sets  $x$ and $y$ is
simply their intersection, which is guaranteed to be a regular set.
The sum, $x + y$, of two regular sets $x$ and $y$ is
a little more complicated; {\em very} roughly, 
it is the union of $x$ and $y$ with any 
internal boundaries removed (fig.~\ref{fig:intuition}c). Finally,
the pseudocomplement, $-x$, of a regular set $x$ 
is simply that part of the plane not
occupied by $x$ or its boundary.

Any line in the plane cuts the plane into two connected, open sets,
called {\em half-planes}. It is easy to see that these sets are
regular, with each being the pseudocomplement of the other.  Hence, we
can speak about their sums, products and complements in ${\rm RO}(\R^2)$.
\begin{definition}
A {\em basic polygon in} $\R^2$ 
is the intersection of finitely many half-planes
in $\R^2$.

\noindent
A {\em polygon in } $\R^2$ is the  sum, in the Boolean algebra
${\rm RO}(\R^2)$, of any finite set of basic polygons in $\R^2$.
\end{definition}
We denote the set of polygons in $\R^2$ by $R$.
Fig.~\ref{fig:intuition}d shows some polygons. Note that polygons, in this
sense, need not be connected and need not be bounded. 
Note that $\emptyset$ and $\R^{2}$ also count as polygons.
We have the following result:
\begin{lemma}
$R$ is a Boolean subalgebra of ${\rm RO}(\R^2)$.
\label{lma:0:booleanR}
\end{lemma}
\proof{
We need only show that $R$ is closed under the Boolean operations.
But this is obvious given the distribution laws for ${\rm RO}(\R^2)$.  
}
%
Idealizing slightly, $R$ is the set of regions recognized by most
computer systems specialized for handling plane spatial data, such as
geographic information systems ({\em GIS}s). That is, such systems are
limited to regions whose boundaries are made up of finitely many 
lines and line segments. Experience has shown that, for many practical 
purposes, no loss of useful expressive 
power results from limiting attention to polygons.

At last, then, we can define our familiar model $\fR$.
\begin{definition} 
The model \fR\ has the domain $R$ and the following interpretations of the 
predicate, constant and function symbols in $\cL$:
        \begin{enumerate}
                \item $[c(x)]^\fR = \{ r \in R | r \mbox{ connected }\}$
        
                \item  $0^\fR = \emptyset$; $1^\fR = \R^{2}$
        
                \item  {\rm For all} $r \in R$: $-^\fR(r) = -r$
        
                \item {\rm For all} $r_{1},r_{2} \in R$: 
                $+^\fR(r_{1},r_{2}) = r_{1} + r_{2}$ {\rm and} 
                $.^\fR(r_{1},r_{2}) = r_{1} .  r_{2}$
\end{enumerate}
\label{def:2:R}
\end{definition}

Thus, the function symbols $+$, $\ . \ $ and $-$ have the obvious 
interpretation in terms of the  Boolean algebra ${\rm RO}(\R^{2})$, and a 
region satisfies the predicate $c(x)$
just in case it is connected in the usual sense of point-set topology.
(Recall that an open set is connected if and only if it is not the
union of any two disjoint, open, nonempty sets.)
It turns out that, for disjoint, connected polygons
$r$ and $s$, $r+s$ is connected just in case $r$ and $s$ have a (nontrivial) edge
in common; hence, the formula $c(x) \wedge c(y) \wedge x.y = 0 \wedge
c(x + y)$ says (assuming $x$ and $y$ to be nonzero)
that $x$ and $y$ are disjoint, connected regions
touching externally along one or more edges. As a shorthand,
if two regions satisfy the formula $c(x+y)$, we say that
they are {\em connected to each other}.
 
To show that the pains we took to define our
domain of interpretation were not in vain, consider the
following formula of $\cL$:
\begin{eqnarray}
\mbox{
\begin{minipage}{10cm}
\begin{tabbing}
$\displaystyle \forall x_1 \forall x_2 \forall x_3 
   ((\bigwedge_{1 \leq i \leq 3} c($\=$\displaystyle x_i) \wedge 
     c(x_1 + x_2 + x_3)) \rightarrow$ \\
\> $\displaystyle ( c(x_1 + x_2) \vee c(x_1 + c_3))).$
\end{tabbing}
\end{minipage}
}
\label{eq:1} 
\end{eqnarray}
This formula asserts that, if the sum of three 
connected regions is connected, then the first must be connected to at
least one of the other two. Question: should this formula be a theorem
of our mereotopological calculus? 

The answer is that it depends on what, exactly, we count as regions.
Formula ~(\ref{eq:1}) is true for the domain $R$ (in fact, for
any domain of reasonably well-behaved regions), but false for 
regular sets of the plane in general. 
For consider the regions $a_1$, $a_2$ and $a_3$ defined by
\begin{eqnarray*}
a_1 & = & \{ (x,y) | -1 < x < 0 \ ; \ -1 -x < y < 1 +x \} \\
a_2 & = & \{ (x,y) | 0 < x < 1 \ ; \ -1 -x < y < \sin(1/x) \} \\
a_3 & = & \{ (x,y) | 0 < x < 1 \ ; \ \sin(1/x) < y < 1 + x \} \ , \\
\end{eqnarray*}
and depicted in fig.~\ref{fig:counterexample}. 
\begin{figure}
\begin{center}
\resizebox{6cm}{!}{\includegraphics{axiom.fig2.eps}}
\end{center}
\caption{Some counterintuitive regions}
\label{fig:counterexample}
\end{figure}
It is not difficult to show that $a_{1}$, $a_{2}$ and $a_{3}$ are 
regular and connected, that $a_1 + a_2 + a_3$ is the interior of the large 
triangle in 
fig.~\ref{fig:counterexample} and so is connected, but
that neither $a_1 + a_2$ nor $a_1 + a_3$ is connected.

In fact, for the purposes of {\em practical} mereotopological 
reasoning,~(\ref{eq:1}) is quite a sensible formula to have as a 
theorem of our calculus,
since---as it turns out---the 
only counterexamples are rather pathological and seem to be
artifacts of the Euclidean model of space rather than anything
that one could come across in real life. (Adopting
such a stance is very much within the spirit of mereotopological
research in AI, where the ability to reason efficiently in everyday
situations is in focus.)  But this case does demonstrate the importance
of having a precise characterization of the regions our mereotopological
calculus talks about: we ought to be clear, {\em if}~(\ref{eq:1}) is a 
theorem of our calculus, what interpretations it is true in.
%
\subsection{The model $\fS$}
%
Before introducing our mereotopological calculus, we present an
alternative interpretation, based on the closed plane $\R^{2} \cup \{
\infty \}$, under the usual topology.  In the sequel, we denote the
closed plane by $Z^{2}$.  For technical reasons, we shall be working
mostly in $Z^{2}$.

Every line in the closed plane is taken to pass through the point $\infty$. It is easy to show (e.g.~by considering the stereographic projection of the sphere onto the plane) that every line divides $Z^2$ into two regular connected sets, which we shall again refer to as half-planes. Since lines contain the point $\infty$, half-planes in the closed  plane are literally the same sets of points as half-planes in the open plane.

\begin{definition}
A {\em basic polygon in} 
$Z^2$ is the intersection of finitely many half-planes
in $Z^2$.

\noindent
A {\em polygon in} $Z^2$ is the  sum, in the Boolean algebra
${\rm RO}(Z^2)$, of any finite set of basic polygons in $Z^2$.

\noindent
We denote the set of polygons in $Z^2$ by $S$.
\label{def:closeddomain}
\end{definition}
Again, it is easy to show that $S$ is a Boolean subalgebra of 
${\rm RO}(Z^2)$, so
we define the closed-plane model $\fS$ as follows.
\begin{definition} 
The model \fS\ has the domain $S$ and the following interpretations of the 
predicate, constant and function symbols in $\cL$:
        \begin{enumerate}
                \item $[c(x)]^\fS = \{ r \in S | r \mbox{ connected }\}$
        
                \item  $0^\fS = \emptyset$; $1^\fS = Z^{2}$
        
                \item  {\rm For all} $r \in S$: $-^\fS(r) = -r$
        
                \item {\rm For all} $r_{1},r_{2} \in S$: 
                $+^\fS(r_{1},r_{2}) = r_{1} + r_{2}$ {\rm and} 
                $.^\fS(r_{1},r_{2}) = r_{1} .  r_{2}$.
\end{enumerate}
\label{def:2:S}
\end{definition}
%
\subsection{The models $\fR$ and $\fS$ are isomorphic.}
Denote the set of open sets in $Z^{2}$ (under the usual topology) by 
$\Omega$.  Let $\hat{x} = x \setminus \{ \infty \}$ for all $x \in \Omega$ 
and let $\hat{\Omega} = \{\hat{x} | x \in \Omega\}$.  Then $\langle \R^{2}, 
\hat{\Omega}\rangle$ is the usual topology on the open, real plane. 
Moreover, $\hat{\Omega} \subseteq \Omega$. If $u 
\in \hat{\Omega}$, then the pseudocomplement $u^{*}$ of $u$ in 
$\hat{\Omega}$ is in general different to the pseudocomplement $u'$ of $u$ 
in $\Omega$; and the property of being regular in $\hat{\Omega}$ is 
different to the property of being regular in $\Omega$.  However, we have 
the following results:
\begin{lemma}
\label{lma:iso:1}
  If $x \in \Omega$, then $\hat{x}^{*} = \widehat{x'}$.
\end{lemma}
\proof{Straightforward.}
%
\begin{lemma}
\label{lma:iso:2}
If $x \in \Omega$ is regular in $\Omega$, then $\hat{x}$ is regular in
$\hat{\Omega}$.
\end{lemma}
\proof{By two applications of 
lemma~\ref{lma:iso:1}, $\hat{x}^{**} = \widehat{x''} = \hat{x}$.}
%
\begin{lemma}
\label{lma:iso:3}
  If $u \in \hat{\Omega}$ is regular in $\hat{\Omega}$, then there exists an 
  $x \in \Omega$ regular in $\Omega$ such 
  that $\hat{x} = u$.
\end{lemma}
\proof{Recall that $\hat{\Omega} \subseteq \Omega$.
It is easy to show that $u \in \Omega$ implies that
$u''$ is regular in $\Omega$. But again, by lemma~\ref{lma:iso:1}, 
$\widehat{u''} = \hat{u}^{**} = u^{**} = u$.}
%
Thus, although  $\fR$ and $\fS$ are based on nonhomeomorphic 
topological spaces, we have:
\begin{lemma}
\label{lma:iso:4}
  The models $\fR$ and $\fS$ are isomorphic.
\end{lemma}
\proof{Lemmas~\ref{lma:iso:2} and~\ref{lma:iso:3} show that
$f:x \mapsto \hat{x}$ maps the set of regular sets in $\Omega$ onto the set 
of regular sets in $\hat{\Omega}$.  And since no two regular sets in 
$\Omega$ differ by a single point, this mapping is 1--1.  Moreover, given 
the fact that, for all $x,y \in \Omega$, $\hat{x} \cap \hat{y} = \widehat{x
\cap y}$, lemma~\ref{lma:iso:1} further guarantees that $f$ induces
a Boolean algebra isomorphism taking ${\rm RO}(Z^{2})$ to ${\rm RO}(\R^{2})$.  And since 
$f$ maps half-planes in $Z^{2}$ to half-planes in $\R^{2}$, $f:S 
\rightarrow R$ is also a Boolean algebra isomorphism.  Finally, we observe 
that $x \in \Omega$ is connected in $\Omega$ iff $\hat{x}$ is connected in 
$\hat{\Omega}$, so that $f:\fS \rightarrow \fR$ is a model isomorphism.} It 
follows of course that ${\rm Th}(\fR) = {\rm Th}(\fS)$.
%
\section{Axiomatization}
Our mereotopological 
calculus, \$, consists of a set of axioms and rules of inference stated in 
$\cL$.
The following abbreviations simplify the axioms.
\begin{enumerate}
                \item Let $x \leq y$ stand for $x.y = x$.  Intuitively, $x 
                \leq y$ states that $x$ is a subset of $y$.

                \item Let $j(x)$ stand for $c(x) \wedge x \neq 0 \wedge c(-x) 
                \wedge -x \neq 0$. In $\fS$ (but not in $\fR$)
                we can think of $j(x)$ as stating that $x$ is a 
                Jordan region.  (See lemma~\ref{lma:0:jordan}.)

                \item If $n \geq 1$, let $x_{1} \oplus \ldots \oplus x_n = y$ 
                stand for \[x_{1} + \ldots + x_n = y \wedge \bigwedge_{1 \leq 
                i < j \leq n}x_{i}.x_{j} = 0 \wedge \bigwedge_{1 \leq i \leq 
                n}(c(x_{i}) \wedge x_{i} \neq 0) \] Intuitively, $x_{1} \oplus 
                \ldots \oplus x_n = y$ states that $x_{1}, \ldots, x_n$ form 
                a partition of $y$ each element of which is connected.  

                \item If $n \geq 1$, let $\beta_{n}(x)$ stand for \[ \exists 
                z_{1} \ldots \exists z_{n} \left( \bigwedge_{1 \leq i \leq n} 
                c(z_{i}) \wedge \Big( x = \sum_{1 \leq i \leq n} z_{i} \Big) 
\right) \]
           
           Intuitively, $\beta_n(x)$ states that $x$ can be formed by 
           summing $n$ connected regions. 
\end{enumerate}
The axiom system $\$$
consists of the axioms and rules of inference of
a complete system of first-order logic with equality, together
with the following special
axioms, axiom schemata and rules of inference.
\begin{enumerate} %\Alph{enumerate}
                \item The usual axioms of nontrivial Boolean algebra with 
                Boolean operations $+$, $.$ and $-$, and (distinct) top and 
                bottom elements $1$ and $0$.
        \label{ax:boolean}
        
        \item  $\forall x \forall y \forall z 
                   \Big(\big(c(x +y) \wedge c(y + z) \wedge y \neq 
0\big) \rightarrow
                         c(x + y + z)\Big)$
\label{ax:2}
        \item  Where $n >1$, the axioms
                  \[\forall x_{1} \ldots \forall x_{n} 
                     \Big(\big(c\left(\sum_{1 \leq i \leq n} 
x_{i}\right) \wedge
                          \bigwedge_{1 \leq i \leq n}c(x_{i})\big) 
\rightarrow
                        \bigvee_{2 \leq i \leq n}c(x_{1} + 
x_{i})\Big)\]
\label{ax:3a}
        \item  Where $n >1$, the axioms
                  \[\forall x_{1} \ldots \forall x_{n} 
                \Big(\big(c\left(\sum_{1 \leq i \leq n} x_{i}\right) 
\wedge
                          \bigwedge_{1 \leq i \leq n}c(x_{i})\big) 
\rightarrow
                        \bigvee_{1 \leq i \leq n}
                            c\left(\sum_{1 \leq j \leq n}^{j \neq i} 
                                                           x_{j} 
\right)
                                                            \Big)
\]
\label{ax:3b}
        \item \ %\ \ 
         
        \vspace{-1cm} 
         
\begin{center}
\begin{minipage}{10cm}
\begin{tabbing}
$\displaystyle \neg \exists x_1 \ldots \exists x_5 
   \big(\bigwedge_{1 \leq i \leq 5} ($\=$\displaystyle c(x_i) \wedge 
     x_i \neq 0) \wedge$\\

\vspace{0.2cm}

\>  $\displaystyle \bigwedge_{1 \leq i < j \leq 5} (c(x_i + x_j) \wedge x_i . x_j = 0)\big)$
\end{tabbing}
\end{minipage}
\end{center}
\label{ax:4a1}
        \item \ %\ \ 
         
        \vspace{-1cm} 
         
\begin{center}
\begin{minipage}{10cm}
\begin{tabbing}
$\displaystyle \neg \exists x_1 \ldots \exists x_6 
   \big(\bigwedge_{1 \leq i \leq 6} ($\=$\displaystyle  
      c(x_i) \wedge x_i \neq 0) \wedge$\\

\vspace{0.2cm}

\> $\displaystyle 
   \bigwedge_{1 \leq i < j \leq 6} x_i . x_j = 0 \wedge 
     \bigwedge_{{1 \leq i \leq 3} \atop {4 \leq j \leq 6}} c(x_i + x_j) \big)$
\end{tabbing}
\end{minipage}
\end{center}
\label{ax:4a2}
\item
$c(0)$
\label{ax:c(0)}
\item
$c(1)$
\label{ax:4b}
        \item \ %\ \ 
         
        \vspace{-1cm} 
         
\begin{center}
\begin{minipage}{10cm}
\begin{tabbing}
                  $\forall x \forall y \forall z 
                     \Big($\=$\big($\=$c(x) \wedge c(y) \wedge c(z) 
\wedge c(x+y) \wedge c(x+z) \wedge $\\
\> \> $x.y = 0 \wedge x.z = 0 \wedge x \neq 0 
\big) \rightarrow$\\
\>                      $\exists u \exists v 
                          \big($\=$ u \oplus v = x \wedge 
                         c(u+y) \wedge c(u+z) \wedge $\\
\> \> $c(v+y) \wedge c(v+z)\big)\Big)$
\end{tabbing}
\end{minipage}
\end{center}
\label{ax:split}
        \item \ %\ \ 
        
        \vspace{-1cm} 
        
\begin{center}
\begin{minipage}{10cm}
\begin{tabbing}
                  $\forall x \forall y 
                     \Big($\=$\big(j(x) \wedge j(y) \wedge j(x+y)
                        \wedge x.y = 0\big) \rightarrow$\\
\>                     $\exists u \exists v 
                          \big($\=$ u \oplus v = x \wedge
                              c(u+y) \wedge \neg c(u+ (-x).(-y)) 
\wedge$\\ 
\> \>                       $c(v+ (-x).(-y)) \wedge \neg 
c(v+y)\big)\Big)$
\end{tabbing}
\end{minipage}
\end{center}
\label{ax:shadow}
        \item  The infinitary rule of inference
                    \[\frac{ \{ \forall x(\beta_{n}(x) \rightarrow 
\phi(x)) |
                       n \geq 1 \}} { \forall x \phi(x) } \]
\label{ax:rule}
\end{enumerate}
%

\begin{figure}
 \begin{center}
  \input{axiom.fig5.pstex_t} \\
 \end{center} 
  \caption{Instantiations of axioms \ref{ax:split} and \ref{ax:shadow}}
  \label{fig:ax:expl}
\end{figure}

\noindent
Axiom \ref{ax:2} ensures that two connected regions with a nonempty
intersection have a connected sum. Axioms \ref{ax:3a} and \ref{ax:3b}
impose restrictions on $n$-tuples $(n > 1)$ of connected regions whose
sum is connected. Specifically, axiom \ref{ax:3a} states that every
region in the $n$-tuple must be connected to some other region in the
$n$-tuple; axiom \ref{ax:3b} states that we can always find a region
in the $n$-tuple which, when removed, leaves an $(n-1)$-tuple whose
sum is connected.  Axioms \ref{ax:4a1} and \ref{ax:4a2} reflect the
nonplanarity of the graphs $K_5$ and $K_{3,3}$, respectively. (The
symbols $K_5$ and $K_{3,3}$ are explained at the beginning of
section~\ref{subsec:cpg}.)  Axioms \ref{ax:c(0)} and \ref{ax:4b} say
that the empty region and the entire space are connected.  Axioms
\ref{ax:split} and \ref{ax:shadow} guarantee the existence of enough
regions in the model.  Simple instantiations of axioms \ref{ax:split}
and \ref{ax:shadow} are shown in figure \ref{fig:ax:expl} where region
$x$ is indicated by light grey areas. The precise content of the
axioms is explained in the proof of theorem~\ref{theo:complete}.
Finally, the infinitary rule of inference serves to guarantee the
existence of models in which every region is the sum of finitely many
connected regions.  We note in passing that the axiom $c(0)$ could
have been omitted, since it can in fact be derived from the other
axioms of \$\  using the infinitary rule of
inference.

\vspace{0.5cm}

\noindent
Let us denote the set of sentences (closed formulae) of $\cL$ which 
are theorems of the system \$ by $T_{\$}$.
The main technical result of this paper is to show that the axiom system \$ is
sound and complete with respect to both of the familiar 
interpretations given above. In other words:
\[
T_{\$} = {\rm Th}(\fR) = {\rm Th}(\fS) \ .
\]
Further model theoretic aspects of the axiom system are investigated 
in Pratt and Lemon~\cite{PrattLemon97b}.

\section{The domain $S$ and its properties}
\label{sec:Rprop}
%
In this section, we establish some basic facts about $S$ needed for
the soundness and completeness proofs below.  Many of these facts
are obvious and some readers may therefore wish to skip to the next
section. However, the notation introduced in 
definitions~\ref{def:closure},~\ref{def:part},~\ref{def:0:graphs},~\ref{def:cut} 
and~\ref{def:tilde} will be used in subsequent sections.

\subsection{Results concerning regular sets}
\begin{definition}
If $x$ is any set in a topological space, let $[x]$ denote
the closure of $x$ and $(x)^0$ the interior of $x$.
We write $\F{x}$ to denote the {\em frontier of} $x$, namely $[x]
\setminus ([x])^0$. 
\label{def:closure}
\end{definition}
We will use lemmas~\ref{lma:nolabel}, \ref{lma:1:homeo}
and~\ref{lma:0:2con} repeatedly in the sequel (sometimes without
mention). Their proofs are so straightforward we omit them.
\begin{lemma}
Let $x$ be a subset of a topological
space $X$. Then $x' = X \setminus [x]$ and $x'' = ([x])^0.$
Hence, $x$ is regular iff $x = ([x])^{0}$; and 
if $x$ is any set, then $x'' \subseteq [x]$.
\label{lma:nolabel}
\end{lemma}
%
\begin{lemma}
Let $X$, $Y$ be topological spaces
and $\nu$ a homeomorphism from $X$ onto $Y$. Let $a,b$ be regular
sets in $X$. Then $\nu(a)$ and $\nu(b)$ are regular sets in $Y$ with: 
(i) $\nu(a.b) = \nu(a).\nu(b)$; (ii) $\nu(-a) = -\nu(a)$;
and (iii)  $\nu(a+b)  =  \nu(a)+\nu(b)$.
\label{lma:1:homeo}
\end{lemma}
%
\begin{lemma}
  Let $a_{1},a_{2},a_{3}$ be regular sets of a topological space $X$
with $a_{1}+a_{2}, a_{2}+a_{3}$ connected 
  and $a_{2}\neq 0$. Then $a_{1}+a_{2}+a_{3}$ is connected.
\label{lma:0:2con}
\end{lemma}
%
The concepts {\em partition} and {\em connected partition} will be
used repeatedly in the proofs to come.
\begin{definition}
Let $X$ be a topological space.
Let $M$ be any Boolean subalgebra of ${\rm RO}(X)$.  If $A$ is a finite
subset of $M$ and the elements of $A$ are pairwise disjoint and sum to
$a \in M$, $A$ is said to be a {\em partition of} $a$ in $M$. If, in
addition, every element of $A$ is connected, we call $A$ a {\em
connected partition of} $a$ in $M$. In the case $a = 1$, we refer to
$A$, simply, as a {\em (connected) partition} in $M$. 
\label{def:part}
\end{definition}
It is easy to see that, if $x$ is regular,
then $[x]$ is the disjoint union of $x$ and $\F{x}$.  The following
(rather technical) lemma, proved in Pratt and Lemon~\cite{PrattLemon97b},
will be useful later. 
\begin{lemma}[Pratt and Lemon~\cite{PrattLemon97b} lemma~3.6]
 Let $X$ be a topological space, $M$ a Boolean subsalgebra of ${\rm
 RO}(X)$ and $a_{1}, \ldots, a_{n}$ a partition in $M$. Let $m$ be such
 that $1 \leq m \leq n$. Then
\begin{center}
\begin{minipage}{10in}
\begin{tabbing}
$a_1 + \ldots + a_m = 
a_1 \cup \ldots \cup a_m \cup \{p | 
\ $\=$ p \in \F{a_i} \mbox{ for some $i$ ($1 \leq i \leq m$), }$\\
   \>$ p \not \in \F{a_j} \mbox{ for any $j$ ($m < j \leq n$)} \}$.
\end{tabbing}
\end{minipage}
\end{center}
\label{lma:0:isolcon}
\end{lemma}
%
\subsection{Basic properties of $S$}
We begin with a lemma on which much of the subsequent analysis
depends.
\begin{lemma}
Any element of $S$ is the sum of finitely many connected elements of $S$.
\label{lma:0:finitecover}
\end{lemma}
\proof{
Since half-planes in the open plane are convex
sets, so are basic polygons. So every element of $R$ is the sum of finitely 
many connected elements of $R$. The result then follows by lemma 
\ref{lma:iso:4}.
}
%
It is easy to see that this property does not hold for all Boolean
sub-algebras of ${\rm RO}(Z^2)$, even where the elements are
relatively well-behaved. For example, if $x$ and $y$ are Jordan
regions (i.e~topologically equivalent to the unit disk), the
intersection $x.y$ can have infinitely many disconnected parts. It is
precisely to prevent this possibility that we restrict ourselves to
polygons.

As usual,  we take a {\em component} of a nonempty set to be a maximal
connected subset of that set.
\begin{lemma}
Let $r \in S$ be nonzero and let $c$ be a component of $r$. Then $c \in S$.
Moreover, $r$ equals the sum of its components.
\label{lma:0:componentsR}
\end{lemma}
\proof{
By lemma~\ref{lma:0:finitecover}, let $c_{1}, \ldots, c_{n}$ be 
connected elements of $S$ such that $r = c_{1} + \ldots + c_{n}$.
For all $i$ ($1 \leq i \leq n$), if $c.c_{i} \neq 0$ then, by 
lemma~\ref{lma:0:2con}, $c_{i} + c$ is connected. If, in 
addition, $(-c).c_{i} \neq 0$, then $ c < c + c_{i}$, contradicting
the maximality of $c$. Thus, if $c.c_{i} \neq 0$, then
$(-c).c_{i} = 0$. Hence $c$ can be expressed as the sum of one or more
$c_{i}$ ($1 \leq i \leq n$), and so $c \in S$. The rest of the lemma is
trivial.}
%
Connected partitions
play an important role in understanding
$S$. In particular, we have:
\begin{lemma}
  Let $r_{1}, \ldots, r_{n} \in S$. Then there exists a connected
  partition $C$ in $S$ such that $r_{i}$ is expressible as a
  sum of zero or more elements of $C$ for each $i$ ($1 \leq i \leq n$).
\label{lma:2:sum}
\end{lemma}
\proof{ 
Let $C$ be the set of
all components of all nonzero products
of the form $\pm r_1 . \  \ldots \  . \pm r_n$.  By
lemma~\ref{lma:0:componentsR}, these components are elements
of $S$, and form a connected partition such that
every $r_i$ can be expressed as a sum of zero or more elements of $C$.
} 
%
\subsection{Connected partitions and graphs}
\label{subsec:cpg}
In this paper, we make extensive use of graph theory.  Recall that a
{\em graph} $G$ consists of a set of nodes $N$ and a set of
(undirected) edges $E$, with each edge in $E$ joining a pair of nodes
in $N$. An edge joining a node to itself is called a {\em loop}.  The
{\em degree} of a node $n$ is the number or edges joining it, with
loops from $n$ to $n$ counting as two edges. We say $G$ has {\em
multiple edges} if there exist distinct edges in $E$ which join the
same nodes.  If $G$ has no multiple edges, as do many of the graphs
considered below, then we can simply denote any edge in $E$ as a pair
of nodes, $(n_1, n_2)$. If the nodes of $G$ are points in the (open or
closed) real plane and the edges of $G$ are realized by Jordan arcs
joining the nodes at their endpoints (but not intersecting each other
except at nodes), then we say that $G$ is a {\em plane graph}.  If a
graph $G$ is isomorphic to a plane graph, then we say that $G$ is {\em
planar}. \label{page:planar} It is well-known that the graphs $K_5$
and $K_{3,3}$ are nonplanar, where $K_5$ has nodes $\{n_1, \ldots,
n_5\}$ and edges $\{(n_i,n_j)|1 \leq i < j \leq 5\}$, and $K_{3,3}$
has nodes $\{n_1, \ldots, n_6\}$ and edges $\{(n_i,n_j)|1 \leq i
\leq3, \ 4 \leq j \leq 6\}$.

It will come as no surprise that we can picture
connected partitions in $S$ as the faces of 
piecewise linear graphs drawn in the closed plane.
\begin{definition}
  A {\em graph*} $G$ is a plane graph in the closed real plane having
  no nodes of degree 0, together with a (possibly
  empty) set of {\em nodeless edges}. These nodeless edges are all
  Jordan curves intersecting no other edge of $G$ (nodeless or
  otherwise).

\noindent
An edge of a graph* is {\em piecewise linear} if it 
lies on finitely many lines. A graph* is piecewise linear
if each of its edges is.
\label{def:0:graphs}
\end{definition}
Hence, all plane graphs in the closed plane
are graphs*. Fig.~\ref{fig:graph*} shows a graph* (where the page
represents the whole closed plane). This  particular 
graph* has two nodeless edges and no nodes of degree 2.
\begin{figure}
\begin{center}
\resizebox{!}{3.5cm}{\includegraphics{axiom.fig3.eps}}
\end{center}
\caption{A graph* with two nodeless edges}
\label{fig:graph*}
\end{figure}
Finally, we observe that Euler's formula
for a $k$-component graph with $n$ nodes, $e$ edges and $f$
faces, namely $n - e + f = k +1$, applies also to
a $k$-component graph*, where nodeless edges do not count as
components.

If $G$ is a graph*, we denote by $|G|$ the set of points in the edges
and vertices of $G$.  We say that two graphs* $G$ and $G'$ are {\em
topologically equivalent} if there exists a homeomorphism $\nu$ of the closed
plane onto itself mapping $|G|$ to $|G'|$.
A graph* is said to have an \emph{isthmus} if it contains an edge whose 
removal would increase the number of its connected components.

The following theorem establishes the importance of
piecewise linear graphs*.

\begin{theorem}
  Let $r_1, \ldots, r_n$
  be a connected partition in $S$; then there exists a finite
  piecewise linear graph* with no isthmuses
  whose faces are precisely $r_1, \ldots, r_n$. Conversely,
  let $G$ be a finite piecewise linear graph*
  with no isthmuses; then the faces of $G$
  form a finite connected partition in $S$.
\label{theo:0:basic}
\end{theorem}
%\label{pg:theo:0:basic}
\proof{
Consider all the half-planes involved
in the construction of
elements $r_1, \ldots, r_n$. The lines bounding these half-planes
form a finite graph* $G_0$ in the obvious way, and the faces of $G^*$
must form a connected partition of 
basic polygons, say, $b_1, \ldots, b_N$. Moreover, 
each $r_i$ ($1 \leq i \leq n$) can certainly
be expressed as a sum of various
$b_j$ ($1 \leq j \leq N$). By renumbering if necessary, let
$r_1 = b_{1} + \ldots + b_{m}$ for some $m$ ($1 \leq m \leq N$).

\noindent
Now remove from $G_0$ all nodes
$p$ such that $p \not \in \bigcup \{\F{b_k} | m < k \leq N \}$ and all edges 
$e$ such that $e \not \subseteq \bigcup \{\F{b_k} | m < k \leq N \}$. The 
result will be a graph* $G_1$ in which the faces $b_1, \ldots, b_m$
are merged into a number of faces $f_1, \ldots, f_l$ for some $l$ ($1 \leq 
l \leq m$). The union of these faces will then be the set
\begin{center}
\begin{minipage}{10in}
\begin{tabbing}
$b_1 \cup \ldots \cup b_m \cup \{p \in |G| : $\=$
p \in \F{b_i} \mbox{ for some $i$ ($1 \leq i \leq m$), }$\\
\> 
$p \not \in \F{b_j} \mbox{ for any $j$ ($m < j \leq N$)} \}$.
\end{tabbing}
\end{minipage}
\end{center}
By lemma~\ref{lma:0:isolcon} this set is just
$b_1 + \ldots +b_m = r_1$. Since $r_1$
  is connected, $l = 1$ and $G_1$ contains the face $f_1 = r_1$.
  Proceeding in the same way for $r_2, \ldots, r_n$ yields a graph* $G
  = G_n$ with faces $r_1, \ldots, r_n$. 
That $G$ has no isthmuses follows
from the fact that each face of $G$ is regular.

\noindent
Conversely, suppose that $G$ is a finite piecewise linear graph*; then 
the edges of $G$ lie on finitely many lines $l_1,\ldots, l_n$. 
Consider the graph $G^*$ made up of all of these lines (extended in both
directions). Each face of $G^*$ is a basic polygon; hence
each face $f_i$ of $G$ will be divided into a finite number
of basic polygons, say, $b_{i,1}, \ldots, b_{i,m_i}$ by a finite
number of lines. Since $G$ has no isthmuses, $f_i$ 
is a regular set, and it is easy to check that no smaller regular
open set contains $b_{i,1}, \ldots, b_{i,m_i}$. In other words, 
$f_i = b_{i,1} + \ldots + b_{i,m_i} \in S$.}
%
\begin{lemma}
Let $r_1, r_2 \in S$ be nonempty, disjoint and connected. Then $r_1 + r_2$ is
connected iff some line-segment lies on the frontiers of both $r_1$ and
$r_2$.
\label{lma:0:connect}
\end{lemma}
\proof{
By theorem \ref{theo:0:basic}, $r_1$ and $r_2$ 
are faces of some finite graph* $G$. The lemma is then obvious.
}
%
\begin{definition}
Let $x$ be any open set in $Z^2$.  
An {\em end-cut} in $x$ is a Jordan arc lying 
in $x$ except for one of its endpoints.  A {\em cross-cut} in $x$ is a 
Jordan arc lying in $x$ except for both of its (distinct) endpoints.  
We say that $\F{x}$ is {\em accessible} from $x$ if, for any $p \in 
\F{x}$ and any $q \in x$, there is an end-cut in $x$ from $p$ to $q$.
\label{def:cut}
\end{definition}
\begin{lemma}
Let $r \in S$ be connected. Let $p \in \F{r}$ and $q \in r$. Then 
there exists a piecewise linear end-cut in $r$ from $p$ to $q$.
\label{lma:0:access}
\end{lemma}
\proof{By theorem~\ref{theo:0:basic}, $r$ is a face of some 
piecewise linear graph*. The lemma is then obvious.}
%
Hence, if $r \in S$ is connected, then $\F{r}$ is accessible from $r$.

Recall that, according to the Jordan curve theorem, a Jordan curve in
the closed (or open) plane has exactly two residual domains. In the
closed plane, all such residual domains are homeomorphic and are
referred to as {\rm Jordan regions}.  Jordan's theorem has a converse
(Newman~\cite{Newman64} theorem V.11.5)  which states that, if a closed set
has two complementary domains in the closed plane, from each of which
it is accessible, then it is a Jordan curve.

\begin{lemma}
  Let $r \in S$.  Then $r$ is a Jordan region iff $r$ is connected and 
  nonzero with a connected and nonzero complement.
\label{lma:0:jordan}
\end{lemma}
\proof{ Suppose $r$ is connected and nonzero with a connected and
  nonzero complement. But $\F{r} = \F{-r}$ has $r$ and $-r$ as its
  complementary domains, from each of which it is accessible, by
  lemma~\ref{lma:0:access}, and so must be a Jordan curve. The other
  direction is trivial.  }  
We remark that this lemma relies on the fact that our underlying
topological space is the closed plane.
%
\begin{lemma}
  Let $r, s \in S$ be disjoint Jordan regions. Then if $-(r+s)$ is
  connected, so is $\F{r} \cap \F{s}$.
\label{lma:0:conbound}
\end{lemma}
\proof{If $\F{r} \cap \F{s}$ is not connected, then, since $\F{r}$ is
a Jordan curve, we can find $p_1,p_2 \in \F{r} \cap \F{s}$ and
$q_1,q_2 \in \F{r} \setminus \F{s}$ with $q_1$ and $q_2$ separating
$p_1$ and $p_2$ in $\F{r}$. By lemma~\ref{lma:0:access}, let $\alpha$
be a cross-cut from $p_1$ to $p_2$ in $r$ and $\beta$ a cross-cut from
$p_2$ to $p_1$ in $s$, so that, by the disjointness of $r$ and $s$,
$\alpha$ and $\beta$ form a Jordan curve $\gamma$ in $Z^2 \setminus
-(r+s)$ with $q_1$ and $q_2$ on different sides of $\gamma$. But since
$q_1,q_2 \in \F{r} \setminus \F{s}$, $q_1,q_2 \in \F{-(r+s)}$, so we
can find points in $-(r+s)$ arbitrarily close to $q_1$ and $q_2$ and
hence on different sides of $\gamma$, thus contradicting the
connectedness of $-(r+s)$.  }
%
\begin{lemma}
  If $r_1, r_2$ and $r_3$ are disjoint connected elements of $S$, then
  there exist at most two points lying on the frontiers of more than
  two of these regions.  \label{lma:0:max_points}
\end{lemma}
\proof{ We suppose that $p_{1},p_{2}$ and $p_{3}$ are distinct points
all lying on the frontiers of $r_1, r_2$ and $r_3$ and derive a
contradiction.  Choose points $q_{1},q_{2},q_{3}$ such that $q_{i} \in
r_{i}$ ($i = 1,2,3$).  Since $r_{1}$, $r_{2}$ and $r_{3}$ are
polygons, it is clear that for $i = 1,2,3$, we can draw three end-cuts
in $r_i$, say $\alpha_{i,1}$, $\alpha_{i,2}$ and $\alpha_{i,3}$ from
the point $q_{i}$ to the points $p_{1}$, $p_{2}$ and $p_{3}$,
respectively.  Since we can choose $\alpha_{i,1}$, $\alpha_{i,2}$ and
$\alpha_{i,3}$ so that they intersect only at $q_i$, this gives us a
planar embedding of the graph $K_{3,3}$, which is well-known to be
nonplanar (see, e.g.~Bollob\'{a}s~\cite{Bollobas79}, p.19).  }
%
\begin{lemma}
  Let $r,s,t \in S$ be Jordan regions such that $r \oplus s \oplus t = 1$
  and $r+s$ and $r+t$ are connected. Then $\F{r} \cap \F{s}$ and 
  $\F{r} \cap \F{t}$ are Jordan arcs.
  \label{lma:0:jordan_arc}
\end{lemma}
\proof{Since $t = -(r+s)$ is connected, $\F{r} \cap \F{s}$ is
connected by lemma \ref{lma:0:conbound}. Any closed, connected subset of the
Jordan curve $\F{r}$ is either (i) empty, (ii) a point, (iii) a Jordan
arc or (iv) the whole of $\F{r}$. Since $-t = r+s$ is connected,
lemma~\ref{lma:0:connect} then guarantees that $\F{r} \cap \F{s}$ is
either a Jordan arc or the whole of $\F{r}$. By symmetry, so is $\F{r}
\cap \F{t}$. By lemma~\ref{lma:0:max_points}, then, both $\F{r} \cap
\F{s}$ and $\F{r} \cap \F{t}$ are Jordan arcs.}
%
The following general result on (abstract) graphs will be used in
several places below.
\begin{lemma}
  Let $G$ be a finite, connected graph.  Then we can find a node of
  $G$ which, when removed, still leaves a connected graph.
\label{lma:0:graphcon}
\end{lemma}
\proof{Straightforward.}
%
Now let us apply this lemma to the analysis of $S$.
Given connected, nonzero
elements $r_1, \ldots, r_n \in S$, we can form the 
abstract graph whose nodes are $\{r_1, \ldots, r_n\}$ and whose
edges are $\{ (r_{i},r_{j}) | 1 \leq i < j \leq n \mbox{ and } 
  r_{i}+r_{j} \mbox{ is connected } \}$ (i.e.~there are no multiple
edges). This graph has the following useful property.
\begin{lemma}
  Let $n \geq 1$ and let $r_{1}, \ldots, r_{n}$ be nonzero, connected 
  regions of $S$.  Let $G$ be the graph with nodes $\{ r_1, \ldots, r_n 
  \}$ and edges $\{ (r_i,r_j) | 1 \leq i < j \leq n \mbox{ and } 
  r_{i}+r_{j} \mbox{ is connected } \}$.  Then $r_{1}+ \ldots + r_{n}$ 
  is a connected element of $S$ iff $G$ is a connected graph.
\label{lma:0:semcon}
\end{lemma}
\proof{
For the if-direction, we proceed by induction on $n$.  
If $n = 1$, the result is trivial.
Otherwise, by
lemma~\ref{lma:0:graphcon}, we can suppose WLOG that the graph 
$G- \{ r_1 \}$ formed by removing $r_1$ and all its edges from $G$ 
is connected.  By inductive hypothesis, $r_{2}+ \ldots + r_{n}$ is 
connected.  Since $G$ is connected, there must be some $i$ ($2 \leq i 
\leq n$) such that $r_{1}+r_{i}$ is connected.  Since $r_{i} \neq 0$, 
$r_{1}+r_{2}+ \ldots + r_{n}$ is 
connected by lemma~\ref{lma:0:2con}.  
\vspace{0.25cm}

\noindent For the only-if-direction, it suffices to show that, for all
$i$,$j$ ($1 \leq i < j \leq n$), there is a sequence $i = i_{1},
\ldots, i_{k} = j$ such that $r_{i_{h}} + r_{i_{h+1}}$ is connected
for all $h$ ($1 \leq h < k$).  Let $p \in r_{i}$ and $q
\in r_{j}$.  By the connectedness of $r_{1}+ \ldots + r_{n}$, draw a
Jordan arc $\alpha$ from $p$ to $q$ lying within $r_{1}+ \ldots +
r_{n}$. Since $\F{r_i}$ is accessible from $r_i$, $\alpha$ can be
chosen so as to visit each region only once. And since the frontier of
each $r_i$ lies on finitely many lines, we may assume that
$\alpha$ can be chosen so that all points on $\alpha$ lie on the
frontiers of at most two of the regions.  Let the sequence of regions
visited by $\alpha$ be $r_{i} = r_{i_{1}}, \ldots, r_{i_{k}} =
r_{j}$.  Then for all $h$ ($1 \leq h < k$), either $r_{i_{h}} \cap
r_{i_{h+1}} \neq \emptyset$ or $\alpha$ visits a point $p$ on a line
segment shared by $\F{r_{i_{h}}}$ and $\F{r_{i_{h+1}}}$. Either way,
$r_{i_{h}} + r_{i_{h+1}}$ is connected.  
}
%
The following lemmas are immediate consequences of
lemma~\ref{lma:0:semcon}.
%
\begin{lemma}
  Let $r,s \in S$ be disjoint with~$r$ and $-s$ connected.
  Let $t$ be a component of $-(r+s)$.  Then $r + t$ is connected.
\label{lma:0:complexcon}
\end{lemma}
\proof{ If $r = 0$, the lemma is trivial.  Otherwise, let the
  components of $-(r+s)$ be $t_{1}, \ldots, t_{n}$.  Obviously, $t_i +
  t_j$ is not connected for all $i$,$j$ ($1 \leq i < j \leq n$).  But
  $-s = t_{1} + \ldots + t_{n} + r$ is connected. The lemma follows
  from lemma~\ref{lma:0:semcon}.  }
%
\begin{lemma}
  Let $r_{1}, \ldots, r_{n} \in S$ be connected with $r_{1}+ \ldots + 
  r_{n}$ connected.  Then, by renumbering if necessary, $r_{1}+ \ldots + 
  r_{n-1}$ is connected.
  \label{lma:consubselect}
\end{lemma}
\proof{From lemma~\ref{lma:0:graphcon} and
lemma~\ref{lma:0:semcon}.}  
%
A result related to lemma~\ref{lma:consubselect}
applies to {\em Jordan} regions
in $S$. The proof involves
a slightly stronger version of lemma~\ref{lma:0:graphcon} but is
otherwise similar.  The details are routine and will be omitted.
\begin{lemma}
  Let $r_{1}, \ldots, r_{n} \in S$ be Jordan regions with $r_{1}+ \ldots + 
  r_{n}$ a Jordan region.  
  Then, by renumbering if necessary, $r_{1}+ \ldots + 
  r_{n-1}$ is a Jordan region.
  \label{lma:jordansubselect}
\end{lemma}
%
\subsection{Finiteness properties concerning $S$}
The following lemmas are crucial to the completeness proof.
\begin{lemma}
\item 
  There exists a function $e: \N \rightarrow \N$ such that, for all 
  $n > 0$, 
  if $r_{1}, \ldots, r_{n}$ are disjoint, connected 
  elements of $S$, then there exist at most $e(n)$ points lying 
  on the frontiers of more than two of these regions.
\label{lma:0:3faces}
\end{lemma}
\proof{
By lemma \ref{lma:0:max_points} and putting $e(n) = n(n-1)(n-2)/3$.  
}
%
\begin{lemma}
There exists a function $f: \N \rightarrow \N$ such that, for all 
$n > 0$, if $A$ is any connected partition in $S$ with $n$ members and 
$G$ is a piecewise linear
graph* with no nodes of degree 2 whose faces in the closed plane
are $A$, then the size of $G$ is 
bounded by $f(n)$.
\label{lma:0:sizebound}
\end{lemma}
\proof{
It is easy to show that any node of degree greater than 2 of a plane graph 
with no isthmuses must lie on the frontier of at least 3 faces. Then, by 
lemma~\ref{lma:0:3faces}, the number of nodes in $G$ is bounded by a 
function of $n$.  The lemma then follows from Euler's formula.  }
%
We then have:
\begin{theorem}
There exists a function $g: \N \rightarrow \N$ such that, for all 
$n > 0$, there exist at most $g(n)$
$n$-element connected partitions in $S$ up to topological equivalence.
\label{theo:3:critical}
\end{theorem}
\proof{
By theorem~\ref{theo:0:basic}, any such 
partition is the set of faces of some piecewise linear graph* with no 
isthmuses, hence of some piecewise linear graph* with no isthmuses and 
no nodes of degree 2.  By lemma~\ref{lma:0:sizebound}, all such 
graphs* are of size bounded by $f(n)$.  Since it can be shown that every 
abstract graph can be embedded in the closed plane in only finitely 
many ways up to topological equivalence, the result follows 
immediately.  }
%
We note in passing that theorem~\ref{theo:3:critical} is false for Euclidean
spaces of higher dimension than 2. It is also false for arbitrary 
partitions of ${\rm RO}(Z^2)$. 
\subsection{The homogeneity of $S$}
The following lemmas are concerned with showing that $S$ is, in a
sense that will become clear below, topologically homogeneous. 

It is well-known that every finite plane graph $G$ in the closed plane
can be continuously deformed into piecewise linear plane graph $G'$.
(See, e.g.~Bollob\'{a}s~\cite{Bollobas79}, p.16.) 
Indeed, this can be done in such a way that piecewise linear edges in
$G$ are unaffected.  In effect, finite plane graphs can have their edges
`straightened out' by a homeomorphism, without affecting 
any points in those faces
whose frontiers involve only straight edges. These results can
easily be extended to finite graphs*. 

If $\nu$ is a homeomorphism of the closed plane onto itself and $x$ a
subset of the closed plane, we write $\nu|_{x}$ to denote the 
restriction of $\nu$ to $x$. Then we have:
\begin{lemma}
  Let $r, s$ be connected elements of $S$ such that there is a
  homeomorphism $\mu$ of the closed plane onto itself taking $r$ to $s$.
  Let $r_{1}, \ldots, r_{n}$ be a connected partition of $r$ in $S$.
  Then there exists a connected partition $s_{1}, \ldots, s_{n}$ of
  $s$ in $S$ and a homeomorphism $\nu$ of the closed plane onto itself
  such that $\nu |_{-r} = \mu|_{-r}$ and $\nu(r_{i}) = s_{i}$ for all
  $i$ ($1 \leq i \leq n$).
\label{lma:0:homo1}
\end{lemma}
\proof{
Let the components of $-r$ be $t_{1}, \ldots, t_{m}$.
Since $t_{1}, \ldots, t_{m}, r_1, \ldots, r_n$ is a connected partition,
theorem~\ref{theo:0:basic} guarantees that we can find a piecewise linear
graph* $G$ with no isthmuses having
these elements as faces. Now $\mu$ maps $r$ to $s$,
hence the components of $-r$ to the components to $-s$, hence
$G$ to a graph* $G'$ with faces $u_{1}, \ldots, u_{m}, f_1, \ldots, f_n$, 
say, where $f_{1} + \ldots + f_{m} = s$.
But then we can continuously deform $G'$ to a piecewise
linear graph* $G''$ without affecting any points in
$-s$ or its frontier. Hence,
the faces of $G''$ will be $u_{1}, \ldots, u_{m},s_1, \ldots, s_n$, say. 
Thus, there is a homeomorphism $\mu'$ of the
closed plane onto itself which is the identity mapping
outside $s$ and which maps $f_i$ to $s_i$, for
all $i$ ($1 \leq i \leq n$). 
Since $G''$ clearly contains no isthmuses,
theorem~\ref{theo:0:basic} guarantees that the faces of $G''$ will be in $S$,
so that $\nu = \mu' \circ \mu$ is the required homeomorphism.
}
\begin{lemma}
  Let $r, s$ be connected elements of $S$ such that there is a
  homeomorphism $\mu$ of the closed plane onto itself taking $r$ to $s$.
  Let $r' \in S$ satisfy $r' \leq r$. 
  Then there exists $s' \in S$ satisfying $s' \leq s$
and a homeomorphism $\nu$ of the closed plane onto itself
  such that $\nu |_{-r} = \mu|_{-r}$ and $\nu(r') = s'$.
\label{lma:0:homo2}
\end{lemma}
\proof{
By lemma~\ref{lma:2:sum}, we can find a finite connected partition
of $r$ in $S$ some of whose elements sum to $r'$.  The result then
follows from lemma~\ref{lma:0:homo1}.  
}
\begin{definition}
If $r_1, \ldots,
r_n$ and $s_1, \ldots, s_n$ are regions of $S$ such that there is a
homeomorphism of the closed plane onto itself mapping $r_i$ to $s_i$
for all $i$ ($1 \leq i \leq n$), then we say that $r_1, \ldots, r_n$
and $s_1, \ldots, s_n$ are {\em topologically equivalent} and write $r_1,
\ldots, r_n \sim s_1, \ldots, s_n$.
\label{def:tilde}
\end{definition}
Now we can state the lemma guaranteeing homogeneity of $S$:
\begin{lemma}
Let
$r_{1}, \ldots, r_{n},s_{1}, \ldots, s_{n},r \in S$ such that
$r_{1}, \ldots, r_{n} \sim s_{1}, \ldots, s_{n}$. Then there exists
$s \in S$ such that $r_{1}, \ldots, r_{n},r \sim s_{1}, \ldots, 
s_{n},s$.
\label{lma:0:homo}
\end{lemma}
\proof{ Let $\mu$ be a homeomorphism of the closed plane onto itself
mapping $r_{1}, \ldots, r_{n}$ to $s_{1}, \ldots, s_{n}$.  Let $c_1,
\ldots, c_N$ be all the components of all nonzero products of the form
$\pm r_1. \ \ldots \ . \pm r_n$ and let $d_1, \ldots, d_N$ be all the
components of all nonzero products of the form $\pm s_1. \ \ldots \
. \pm s_n$.  Then, by lemma~\ref{lma:0:componentsR}, $c_1, \ldots,
c_N$ and $d_1, \ldots, d_N$ are connected partitions in $S$, and by
renumbering if necessary, $\mu$ maps $c_1, \ldots, c_N$ to $d_1,
\ldots, d_N$.  It suffices to find $s \in S$ such that $c_{1}, \ldots,
c_{N},r \sim d_{1}, \ldots, d_{N},s$.

\noindent
For all $j$ ($1 \leq j \leq N$), let $c'_j = r.c_j$. By 
lemma~\ref{lma:0:homo2}, there exists a $d'_j \in S$ and a homeomorphism
$\nu_j$ of the closed plane onto itself
mapping $c'_j$ to $d'_j$ and equal to $\mu$
outside $c_j$. Then the function
\[
\nu = \bigcup \{ \nu_j |_{c_j} : 1 \leq j \leq N \} \cup
\mu|_{\F{c_1} \cup \ldots \cup \F{c_N}}
\]
is a homeomorphism of the closed plane onto itself mapping $c_j$ to
$d_j$ for all $j$ ($1 \leq j \leq N$) and mapping $r= c'_1 +
\ldots + c'_N$ to $ s= d'_1 + \ldots + d'_N \in S$ as required.
}
%
Lemma~\ref{lma:0:homo} has the immediate consequence that the model
$\fS$ is ``topological'' in the following sense:
\begin{lemma}
  Let $r_1, \ldots, r_n, s_1, \ldots, s_n \in S$ such that $r_1, 
  \ldots, r_n \sim s_1, \ldots, s_n$.  Then $r_1, \ldots, r_n$ and 
  $s_1, \ldots, s_n$ satisfy the same formulae in \fS.
\label{lma:0:homotype}
\end{lemma}
\proof{
We prove by induction on the complexity of $\phi(x_{1}, \ldots, x_{n})$ 
that, if $\fS \models \phi [r_1, \ldots, r_n]$, then $\fS \models \phi 
[s_1, \ldots, s_n]$.

\vspace{0.25cm}

\noindent
If $\phi(x_{1}, \ldots, x_{n})$ is $c(t)$, where $t$ is some Boolean
combination of the variables $x_{1}, \ldots, x_{n}$, then the result
is guaranteed by lemma~\ref{lma:1:homeo} and the fact that
connectedness is a topological property.

\vspace{0.25cm}

\noindent
The sole nontrivial recursive case is where $\phi(x_1, \ldots, x_n)$
is of the form $\exists y \psi(x_1, \ldots, x_n,y)$.  If $\fS \models
\phi [r_1, \ldots, r_n]$, there exists $r \in S$ such that $\fS
\models \psi [r_1, \ldots, r_n,r]$.  By lemma~\ref{lma:0:homo}, there
exists $s \in S$ such that $r_1, \ldots, r_n,r \sim s_1, \ldots,
s_n,s$.  By inductive hypothesis, $\fS \models \psi [s_1, \ldots,
s_n,s]$, hence $\fS \models \phi [s_1, \ldots, s_n]$.  }
%
\section{Correctness}
\label{sec:corr}
%
\subsection{Soundness}
%
\begin{theorem}[Soundness]
  Let $\Phi$ be a set of sentences.  If $\fS \models \Phi$ then $\Phi$ 
  is \$-consistent.
\label{theo:sound}
\end{theorem}
{\bf Proof:} We show that all special axioms are true in \fS\ and that
the special rule of inference is truth-preserving in \fS.

\vspace{0.5cm}

\noindent
{\bf Axioms \ref{ax:boolean}: } By lemma~\ref{lma:0:booleanR}.

\vspace{0.5cm}

\noindent
{\bf Axiom \ref{ax:2}: } By lemma~\ref{lma:0:2con}.

\vspace{0.5cm}

\noindent
{\bf Axiom schema \ref{ax:3a}: } If some $x_{i}$ is zero, then
the conditional is trivial. If every $x_{i}$ is nonzero,
it follows by lemma~\ref{lma:0:semcon}.

\vspace{0.5cm}

\noindent
{\bf Axiom schema \ref{ax:3b}: } By lemma \ref{lma:consubselect}.

\vspace{0.5cm}

\noindent
{\bf Axiom \ref{ax:4a1}: } Suppose $r_1, \ldots, r_5$ satisfied the
condition inside the existential quantifiers. Then by lemma~\ref{lma:0:access},
we could construct a planar representation of the graph $K_5$, which is known
to be nonplanar (Bollob\'{a}s~\cite{Bollobas79}, p.19). 


\vspace{0.5cm}

\noindent
{\bf Axiom \ref{ax:4a2}: } As for axiom~\ref{ax:4a1}, but with
$K_{3,3}$ instead of $K_5$.

\vspace{0.5cm}

\noindent
{\bf Axiom \ref{ax:c(0)}: } The empty region is connected.

\vspace{0.5cm}

\noindent
{\bf Axiom \ref{ax:4b}: } The closed plane is connected.

\vspace{0.5cm}

\begin{figure}
\begin{center}
\begin{minipage}{5cm}
 \begin{center}
  \resizebox{5cm}{!}{\input{axiom.fig4a.pstex_t}} \\
  a) Axiom~\ref{ax:split}
 \end{center} 
\end{minipage} \hspace{1cm}
\begin{minipage}{5cm}
 \begin{center}
  \resizebox{4.5cm}{!}{\input{axiom.fig4b.pstex_t}} \\
  b) Axiom~\ref{ax:shadow}
 \end{center} 
\end{minipage} \hspace{1cm}
\end{center}
\caption{Illustration of two axioms}
\label{fig:soundness}
\end{figure}

\noindent
{\bf Axiom \ref{ax:split}: } Refer to fig.~\ref{fig:soundness}a).
Let $r_{x}, r_{y}, r_{z}$ satisfy the
antecedent of this axiom in $\fS$.  We may assume that $r_{y}$ and
$r_{z}$ are nonzero, since similar or easier arguments apply in the cases
the cases where $r_{y} =0$ or $r_{z} =0$.  By
lemma~\ref{lma:0:connect}, there exist line-segments $\alpha_{y}$ and
$\alpha_{z}$ such that~$|\alpha_{y}| \subseteq \F{r_{x}} \cap \F{r_{y}}$
and $|\alpha_{z}| \subseteq \F{r_{x}} \cap \F{r_{z}}$.  Let $p_{1},
p_{2} \in |\alpha_{y}|, q_{1}, q_{2} \in |\alpha_{z}|$ be distinct
from each other and from the endpoints of $\alpha_{y}$ and
$\alpha_{z}$.  By lemma~\ref{lma:0:access}, let $\gamma_{1}$ be a
piecewise linear cross-cut in $r_x$ from $p_{1}$ to $q_{1}$. Either
$\gamma_1$ partitions $r_{x}$ into two connected regions $r_{u}$ and
$r_{v}$, or $r_{x} \setminus |\gamma_{1}|$ is still connected.  In the
former case, $r_{u}, r_{v} \in S$ by theorem~\ref{theo:0:basic}, and
it is easy to see that $r_x = r_u \oplus r_v$.  In the latter case, 
construct a piecewise linear cross-cut $\gamma_{2}$ in
$r_{x}\setminus |\gamma_{1}|$ joining ${p_2}$ and ${q_2}$.  Now
${p_2}$ and ${q_2}$ lie in the same component of $Z^2 \setminus
(r_{x}\setminus |\gamma_{1}|)$, since $p_2 \in [y]$, $q_2 \in [z]$ and 
$\gamma_1$ connects $[y]$ and $[z]$.  It is a standard result 
(Newman~\cite{Newman64}, chapter V., theorem~11.7) that, if $\gamma$ is a 
cross-cut in a nonempty open connected set $U$ with endpoints in the same 
component of $Z^2 \setminus U$ then $U \setminus |\gamma|$ has two components.  
Hence $\gamma_{2}$ partitions $r_{x}\setminus |\gamma_{1}|$ into two 
connected regions.  Together, then, $\gamma_1$ and $\gamma_2$ 
partition $r_x$ into two connected regions, $r_u$ and $r_v$.  Again, 
by theorem \ref{theo:0:basic}, we have 
$r_{u}, r_{v} \in S$, and it is easy to see that $r_x = r_u \oplus 
r_v$.  Since $p_1$, $p_2$, $q_1$ and $q_2$ are not endpoints of 
$\alpha_y$ or $\alpha_z$, the pairs of regions $\{r_u,r_y\}$, $\{r_v, 
r_y\}$, $\{r_u,r_z\}$ and $\{r_v,r_z\}$ all have shared line segments 
on their frontiers.  It follows from lemma~\ref{lma:0:connect} that 
$r_{x}, r_{y}, r_{z}$ satisfy the consequent of this axiom in $\fS$.

\vspace{0.5cm}

\noindent
{\bf Axiom \ref{ax:shadow}: } Refer to fig.~\ref{fig:soundness}b).
Let $r_{x},r_{y}$ satisfy the antecedent
of this axiom in $\fS$.  Let $s = -(r_x +r_y)$.  By
lemma~\ref{lma:0:jordan}, $r_x$ and $r_y$ are Jordan regions such that
$r_x + r_y$ and therefore $s$ are also Jordan regions.  Thus by 
lemma~\ref{lma:0:jordan_arc}, $\F{r_x} \cap \F{r_y}$ is the locus of 
some Jordan arc $\alpha$, and $\F{r_x} \cap \F{s}$ is the locus of 
some Jordan arc $\beta$. And
by lemma \ref{lma:0:max_points}, it is easy to see that $\alpha$ and
$\beta$ have the same end-points, say, $p$ and $q$.  
By lemma~\ref{lma:0:access}, let $\gamma$ be a piecewise linear 
cross-cut in $r_x$ from $p$ to $q$.  Since $r_{x}$ is a Jordan region, 
$\gamma$ partitions $r_{x}$ into two connected regions $r_{u},r_{v}$.  
By theorem~\ref{theo:0:basic}, $r_{u}, r_{v} \in S$, and it is easy to 
see that $r_x = r_u \oplus r_v$.  Moreover, since $r_{u} + -r_x = 
-r_v$ and $r_{v} + -r_x = -r_u$ are connected and nonzero, $r_u$ and 
$r_v$ are Jordan regions.  It is then easy to verify (exchanging $r_u$ 
and $r_v$ if necessary) that $\F{r_u} \cap \F{r_y} = |\alpha|$ and 
$\F{r_v} \cap \F{s} = |\beta|$, and that $\F{r_v} \cap \F{r_y} = 
\F{r_u} \cap \F{s} = \{p,q\}$.  It follows from 
lemma~\ref{lma:0:connect} that $r_x$ and $r_y$ satisfy the consequent 
of this axiom in $\fS$.

\vspace{0.5cm}

\noindent 
{\bf Inference rule \ref{ax:rule}: } 
Suppose that $\fS \models \forall x(\beta_{n}(x) \to \phi(x))$ for all 
$n \in \N$.  Let $r \in S$.  Then by lemma \ref{lma:0:finitecover}, there 
exist finitely many connected elements $r_{1}, \ldots, r_{N} \in S$ s.t.
$r = r_{1} + \ldots + r_{N}$.  Hence, there is an $N$ 
such that $\fS \models \beta_{N}[r]$, so that $\fS \models \phi[r]$.
Hence $\fS \models \forall x \phi(x)$.  
\boxterm
%
\subsection{Completeness}
%
\begin{theorem}[Completeness]
        Let $\Phi$ be a set of \$-consistent sentences. 
        Then $\fS~\models~\Phi$.
\label{theo:complete}
\end{theorem}
{\bf Proof: } 
The strategy is to construct a model \fA\ of $\Phi$ respecting the 
axioms and rules of inference of \$, and then to embed its domain $A$ 
into the closed plane in such a way that $\fA \subseteq \fS$.  By 
proving a result on the way in which $A$ is embedded in $S$, we then 
strengthen this relation to $\fA \preceq \fS$, from which it follows 
that $\fS \models \Phi$.  For clarity, we break the proof up into four 
stages.

\vspace{0.25cm}

\noindent 
{\bf Stage 1: } Let $T$ be the set of \$-consequences of 
$\Phi$.  Since $\Phi$ is \$-consistent, $T$ is consistent.  Consider 
the set of formulae 
\[ 
\Sigma(x) = \{ \neg \beta_{N}(x) | N \geq 1 \} \ .  
\]
 Suppose that 
$\theta(x)$ is any formula consistent with $T$.  Since $T \nvDash 
\forall x \neg \theta(x)$ and since $T$ is \$-closed, the rule of 
inference \ref{ax:rule} guarantees that \linebreak 
$T \nvDash \forall x(\beta_{N}(x) 
\rightarrow \neg \theta(x))$ for some $N \geq 1$.  Hence 
$\theta(x)$ 
consistent with $T$ implies $T \nvDash \forall x(\theta(x) \rightarrow 
\neg \phi(x))$ for some $\phi(x) \in \Sigma(x)$---or, as we say,
$T$ {\em locally omits} $\Sigma(x)$.

\vspace{0.25cm}

\noindent 
According to the Omitting Types Theorem (Chang and
Keisler~\cite{ChangKeisler90} theorem~2.2.9), if a consistent
theory $T'$ locally
omits a set $\Sigma'(x)$ of formulae, then $T'$ has a countable model
$\fA'$ such that $\fA'$ {\em omits} $\Sigma'(x)$---that is, such that
no element of $A'$ satisfies every formula in $\Sigma'(x)$.  By the
omitting types theorem, then, there exists a countable model \fA\ of
$T$ such that, for all $a \in A$, there exists $N$ such that $\fA
\models \beta_N[a]$. In other words, we can find a model $\fA$ of $T$
in which every element is the sum of finitely many connected pieces.

\vspace{0.25cm}

\noindent 
When discussing the model \fA , we use the following conventions.  If 
$a, b \in A$, we write $a + b$, $a.b$, and $-a$ to denote elements of 
$A$ in the obvious way. If $a \in A$ and $\fA \models c[a]$ then we 
say that $a$ is {\em connected}. In this 
context, then, the Boolean functions and the term ``connected'' do not 
have their normal senses, for the elements of $A$ are not 
(necessarily) spatial regions.  However, since we will be considering 
only the model \fA\ in this stage of the proof, no confusion need 
arise. If $a_1, \ldots, a_n \in A$ are 
nonzero, connected and pairwise disjoint, we denote their sum by 
$a_1 \oplus \ldots \oplus a_n$.  If 
$a_1 \oplus \ldots \oplus a_n = 1$, we say that $a_1, \ldots, a_n$ 
form a {\em connected partition}. 
\vspace{0.25cm}

\noindent
Having defined \fA, we now establish some of its basic properties.
Since \fA\ is countable, let $A = \{ a_{1}, a_{2}, \ldots \}$.  And
since it is easy to see that $|A| > 2$, we may assume WLOG that $a_1
\not \in \{0,1\}$.  We first show that, for any initial segment,
$a_{1}, \ldots, a_{n}$, we can find $c_{1}, \ldots, c_{N} \in A$
satisfying the formula $c_{1} \oplus \ldots \oplus c_{N} = 1$ in \fA\ 
such that each $a_{i}$ ($1 \leq i \leq n$) can be expressed as a sum
of some of the $c_{1}, \ldots, c_{N}$.  For consider the $M_{n}$
nonzero elements of the form:
\[ 
   e_{j} = \pm a_{1}.  \ \ldots \ .  \pm a_{n} \ .  
\] 
where $\pm a_{i}$ is either $a_{i}$ or $-a_{i}$.  
We call these $e_j$ the {\em atoms generated 
by} $a_{1}, \ldots, a_{n}$.  Since \fA\ omits $\Sigma$, we must be 
able to find, for each $j$ ($1 \leq j \leq M_{n}$), a collection of 
connected elements $d_{j,1}, \ldots, d_{j,N_{j}}$ summing to 
$e_{j}$.  
We now take any pair of these elements $d_{j,k}$ and $d_{j,l}$ such 
that $d_{j,k} + d_{j,l}$ is connected and replace these elements by 
their sum $d_{j,k}+d_{j,l}$. By repeating this process sufficiently 
often, we obtain connected
elements $d'_{j,1}, \ldots, d'_{j,N'_{j}}$ summing to 
$e_{j}$ such that no two of them have a connected sum.  It follows 
from axiom~\ref{ax:2} that these $d'_{j,k}$ are pairwise disjoint.  
If we denote by $c_{1}, \ldots, c_{N}$ all the $d'_{j,k}$ for the 
various atoms $e_{j}$ (ignoring any zero elements), it is easy to see 
that:
\begin{enumerate}
  \item $c_{1}, \ldots, c_{N}$ form a connected partition.
  
  \item the atoms generated by $a_{1}, \ldots, a_{n}$, and hence 
  $a_{1}, \ldots, a_{n}$ themselves, are expressible as sums of the 
  $c_{1}, \ldots, c_{N}$; 
  
  \item if $c_{i}$ and $c_{j}$ ($1 \leq i < j \leq N$) are contained 
  within the same atom $e_{j}$ generated by $a_{1}, \ldots, a_{n}$, 
  then $c_{i} + c_{j}$ is not connected.
\end{enumerate}
We call a collection $c_{1}, \ldots, c_{N}$ satisfying these three 
properties a {\em maximal connected partition} generated by $a_{1}, 
\ldots, a_{n}$.

\vspace{0.25cm}

\noindent 
So, given any initial segment $a_{1}, \ldots, a_{n}$ of $A$, let 
$c^{(n)}_{1}, \ldots, c^{(n)}_{N_{n}}$ be some maximal connected partition 
generated by $a_{1}, \ldots, a_{n}$.  (The $(n)$-superscripts are for 
clarity when we consider maximal connected partitions corresponding to 
different initial segments of $A$.) 
We observe
in passing that, since $a_1 \not \in 
\{0,1\}$, $M_{n} > 1$, so that $N_n >1$ for all $n \geq 1$.

\begin{claim}
  If $m \leq n$, then for each $k$ ($1 \leq k \leq N_{n}$), there 
  exists $j$ ($1 \leq j \leq N_{m}$) such that $c^{(n)}_{k} \leq 
  c^{(m)}_{j}$.
\label{claim:1.1}
\end{claim}

\noindent 
\proof{
Write $d_{1}, \ldots, d_{l}$ for those $c^{(m)}_{j}$ 
such that $c^{(m)}_{j}.c^{(n)}_{k} \neq 0$; it suffices to show that 
$l=1$.  Since $c^{(m)}_{1}, \ldots, c^{(m)}_{N_{m}}$ form a partition, 
we have:
\[ 
  \sum_{1 \leq h \leq l}(c^{(n)}_{k} + d_{h}) = \sum_{1 \leq h \leq 
l}d_h \ .  
\] 
By axiom~\ref{ax:2}, $c^{(n)}_{k} + d_h$ is connected for all $h$ ($1 
\leq h \leq l$), since $c^{(n)}_{k}$ is connected and $d_h$ is 
connected with $c^{(n)}_{k}.d_h \neq 0$.  Then, by repeated 
applications of axiom~\ref{ax:2}, $\sum_{1 \leq h \leq l}(c^{(n)}_{k} 
+ d_{h})$ is connected, since $c^{(n)}_{k} \neq 0$.  That is, 
$\sum_{1 \leq h \leq l}d_h$ is connected.

\vspace{0.25cm}

\noindent 
Suppose, then that $l > 1$.  Then by axiom~\ref{ax:3a}, 
there exists $d_{h}$, ($2 \leq h \leq l$) such that $c(d_{1}+d_{h})$
is connected.  But since $d_{1}$ and $d_{h}$ have nonzero 
intersection with $c^{(n)}_{k}$, and since $c^{(n)}_{k}$ is contained 
in some atom generated by $a_{1}, \ldots, a_{n}$ with $m \leq n$, it 
follows that $d_{1}$ and $d_{h}$ are contained in the same atom 
generated by $a_{1}, \ldots, a_{m}$.  But then it is impossible that 
$d_{1}+d_{h}$ be connected by the fact that $c^{(m)}_{1}, \ldots, 
c^{(m)}_{N_{m}}$ is a maximal connected partition.  Hence we cannot 
have $l > 1$.  }
%
It follows from claim~\ref{claim:1.1} that, if $m \leq n$ 
each $c^{(m)}_{j}$ can be expressed as a sum of various $c^{(n)}_{k}$ 
and that, for each $n$, the $c^{(n)}_{1}, \ldots, c^{(n)}_{N_{n}}$ 
are 
unique.  Hence we may speak of {\em the} maximal connected partition 
generated by the $a_{1}, \ldots, a_{n}$.

\vspace{0.25cm}

\noindent
{\bf Stage 2: } 
We now map each initial segment $a_{1}, \ldots, a_{n}$ of $A$ into 
our standard domain $S$.  Let $n$ be a positive integer. 
We denote by $w^{(n)}$ the set of functions 
$g^{(n)}: \{ c^{(n)}_{1}, \ldots, c^{(n)}_{N_{n}} \} \rightarrow S$ 
satisfying
\begin{description}
  \item G1: The regions $g^{(n)}(c^{(n)}_{1}), \ldots, 
  g^{(n)}(c^{(n)}_{N_{n}})$ form a connected partition in $S$

  \item G2: For all $i,j$ ($1 \leq i < j \leq N_{n}$), 
  $g^{(n)}(c^{(n)}_{i}) + g^{(n)}(c^{(n)}_{j})$ is connected iff 
  $c^{(n)}_{i} + c^{(n)}_{j}$ is connected.
\end{description}
We remark that, in G2, we have $g^{(n)}(c^{(n)}_{i}), 
g^{(n)}(c^{(n)}_{j}) \in S$ and $c^{(n)}_{i}, c^{(n)}_{j} \in A$.  
Hence, different senses of ``+'' and ``connected'' apply in the two 
cases.  For $n=0$ we define $w^{(0)}=\{ \emptyset \}$.

\vspace{0.25cm}

\begin{definition}
Let $b_{1}, \ldots, b_{n} \in A$. Form the graph $G$ with nodes $\{
b_1, \ldots, b_n \}$ and edges $\{ (b_i,b_j) | 1 \leq i < j \leq n \mbox{ and
  } b_{i}+b_{j} \mbox{ is connected} \}$ (i.e.~$G$ has no multiple edges).
We call $G$ the {\em binary connection graph} on $b_1, \ldots, b_n$.
\end{definition}

\noindent
\begin{claim}
  Let $b_{1}, \ldots, b_{n} \in A$ be nonzero and connected. Then 
  $b_{1}+ \ldots + b_{n}$ is connected iff the binary connection graph
  on $b_1,\ldots, b_n$ is a connected graph.
\label{claim:2.0}
\end{claim}
\proof{
We proceed by induction on $n$ for both directions. 
Let $G$ be the binary connection graph
on $b_1, \ldots, b_n$. If $n = 1$, the claim is trivial.

\vspace{0.25cm}

\noindent
Suppose that $n>1$ and $G$ is a connected graph.  By 
lemma~\ref{lma:0:graphcon}, we can suppose WLOG that the graph 
$G - \{b_1\}$ formed by removing $b_1$ and all its edges from $G$ 
is connected.  By inductive hypothesis, $b_{2}+ \ldots + 
b_{n}$ is connected.  Since $G$ is connected, there must be some $i$ ($2 \leq i 
\leq n$) such that $b_{1}+a_{i}$ is connected.  Since $b_{i}$ is 
nonzero, axiom~\ref{ax:2} ensures that $b_{1}+ \ldots + b_{n}$ is connected.

\vspace{0.25cm}

\noindent 
Suppose that $n>1$ and $b_{1}+ \ldots + 
b_{n}$ is connected.  Axiom schema~\ref{ax:3b} ensures that, by renumbering if 
necessary, $b_{2}+ \ldots + b_{n}$ is connected.  By inductive 
hypothesis, the graph $G - \{b_1\}$ is connected.  Moreover, axiom 
schema~\ref{ax:3a} ensures that, for some $i$ ($2 \leq i \leq n$), 
$b_{1}+b_{i}$ is connected.  Hence $G$ is connected.  }
%
\begin{claim}
The binary connection graph on a connected partition is planar.
\label{claim:2.5}
\end{claim}
\proof{
Let $c_1, \ldots, c_n$ be a connected partition, and let $G$ be its
binary connection graph. By a well-known theorem of Kuratowski, it
suffices to show that $G$ contains no subgraph identical to either
$K_5$ or $K_{3,3}$ to within nodes of degree 2
(Bollob\'{a}s~\cite{Bollobas79}, p.19). For definiteness, we concentrate on
the case $K_5$.

\noindent
Let $H$ be a subgraph of $G$ identical to $K_{5}$ to within nodes 
of degree 2.
If $H$ contains nodes of degree 2, then
re-number the nodes of $G$ if necessary so that 
that $c_1, \ldots, c_5$ are the nodes of $H$ of degree 
greater than 2, and $c_6, \ldots, c_{5 + h}$
are the nodes of $H$ of degree 2 lying between nodes $c_4$ and $c_5$, with
$h > 0$. Then, by claim~\ref{claim:2.0}, $d = c_5 + c_6 + \ldots + 
c_{5 +h}$
is connected, so that 
$c_1, \ldots, c_4, d, c_{6 + h}, \ldots, c_n$
is a connected partition. Moreover, this new connected partition also contains
a subgraph $H'$ identical to $K_{5}$ to within nodes of degree 2, but having
strictly fewer nodes of degree 2 than $H$. Proceeding in this way, we can
find a connected partition with a binary connection graph $G$ containing
a subgraph isomorphic to $K_5$, which is impossible by axiom~\ref{ax:4a1}.

\noindent
The case $K_{3,3}$ proceeds identically, except that we rely on
axiom~\ref{ax:4a2}.
}
%
\begin{definition}
  Let $G$ be a plane graph. Its \emph{geometric dual} $G^*$ is
  obtained in the following way (cf.~Wilson~\cite{Wilson79}, p.72). A
  point $v_i^*$ is chosen inside each face of $G$. These chosen points
  are the nodes of $G^*$. Corresponding to each edge $e$ of $G$ an
  edge $e^*$ is drawn which crosses $e$ but no other edge of $G$ and
  joins the nodes $v_i^*$ which lie in the faces adjoining $e$. These
  edges $e^*$ are the edges of $G^*$.
\end{definition}
%
\begin{claim}
  For all $n \in \N$,  $w^{(n)} \neq \emptyset$.
\label{claim:2.1}
\end{claim}
\proof{ If $n=0$ the claim is trivial.  Suppose $n \geq 1$.  We show
  that, given a maximal connected partition $c^{(n)}_{1}, \ldots,
  c^{(n)}_{N_{n}}$ ($n \geq 1$), there exists some $g^{(n)}$
  satisfying G1 and G2. We observed above that $N_{n} > 1$.  For the
  time being we shall drop the $n$-sub- and superscripts and write $N$
  for $N_n$ and $c_{i}$ for $c^{(n)}_{i}$.  Let $G$ be the binary
  connection graph on $c_{1}, \ldots, c_{N}$.  By
  claim~\ref{claim:2.5}, $G$ is planar.  By axiom~\ref{ax:4b} and
  claim~\ref{claim:2.0}, $G$ is connected. Let $H$ be an embedding of
  $G$ in the closed plane all of whose edges are piecewise linear.
  Since $H$ is plane and connected, by a standard result
  (Wilson~\cite{Wilson79}, p.73) it has a plane, connected geometric
  dual $H^{*}$ which in turn has a geometric dual $H^{**}$ isomorphic
  to $H$.  Thus there exists a 1--1 function $h^{**}:\mbox{nodes}(G)
  \rightarrow \mbox{nodes}(H^{**})$ such that, for all $i$, $j$ ($1
  \leq i < j \leq N_{n}$), $(c_{i},c_{j})$ is a $G$-edge iff
  $(h^{**}(c_{i}),h^{**}(c_{j}))$ is an $H^{**}$-edge.  By the
  construction of $H^{**}$, there exists a 1--1 function
  $h^{*}:\mbox{nodes}(H^{**}) \rightarrow \mbox{faces}(H^{*})$ such
  that, for all $n_{1}, n_{2} \in \mbox{nodes}(H^{**})$, there is an
  $H^{**}$-edge $(n_{1},n_{2})$ iff $h^{*}(n_{1})$ and $h^{*}(n_{2})$
  share an $H^{*}$-edge on their frontiers.  Also by the construction
  of $H^{**}$, if $H^{*}$ contains an isthmus, $H^{**}$ and hence $G$
  contains a loop, which is impossible by definition, so $H^{*}$
  contains no isthmus.  Moreover, $H^{*}$ can obviously be constructed
  so that all its edges are piecewise linear. It follows from
  theorem~\ref{theo:0:basic} that the faces of $H^*$ form a connected
  partition in $S$.

\vspace{0.25cm}

\noindent 
Now put $g^{(n)} = h^{*} \circ h^{**}$.  Thus,
$g^{(n)}$ is a function from $\{ c_{1}, \ldots, c_{N_{n}} \}$ into $S$ 
satisfying G1.  To see that $g^{(n)}$ also satisfies G2, we note 
that, 
for all $i$, $j$ ($1 \leq i < j \leq N$), $(c_{i},c_{j})$ is a 
$G$-edge iff $g^{(n)}(c_{i})$ and $g^{(n)}(c_{j})$ share an 
$H^{*}$-edge on their frontiers.  By lemma~\ref{lma:0:connect}, for 
all $i$, $j$ ($1 \leq i < j \leq N_{n}$), $c_{i} + c_{j}$ is 
connected 
iff $g^{(n)}(c_{i})+g^{(n)}(c_{j})$ is connected.  Hence $g^{(n)}$ 
satisfies G2 and $w^{(n)} \neq \emptyset$ as required.}
%
We remark that, while the proof of claim~\ref{claim:2.1} 
constructs an element of $w^{(n)}$, not all 
elements of $w^{(n)}$ can be constructed in this way.

We now proceed to establish some additional properties of the sets 
$w^{(n)}$ and their members.
As usual, if $C \subseteq \{ c^{(n)}_{1}, \ldots,  
c^{(n)}_{N_{n}} \}$, we write $g^{(n)}(C)$ to mean
$\{g^{(n)}(c^{(n)}_{i}) | c^{(n)}_{i} \in C \}$.

\begin{claim}
  Let $C \subseteq \{ c^{(n)}_{1}, \ldots, c^{(n)}_{N_{n}} \}$.  Then 
  $\sum C$ is connected iff $\sum g^{(n)}(C)$ is connected.
\label{claim:2.2}
\end{claim}
(Note the two different uses of `$\sum$' and `connected'.)

\vspace{0.25cm}

\noindent
\proof{
Suppose first that $C = \emptyset$. Then $\sum C = 0 \in A$
and $\sum g^{(n)}(C) = 0 \in S$. (Note the two different uses of 
`$0$'.)
By axiom~\ref{ax:c(0)}, $0 \in A$ is connected. Since $0 \in S$ is
connected, the result holds.

\vspace{0.25cm}

\noindent
Suppose next that $C \neq \emptyset$.
By lemma~\ref{lma:0:semcon}, $\sum g^{(n)}(C)$ is connected iff
the set of edges 
\[\{ (c_i,c_j) | c_{i}, c_{j} 
\in C, i \neq j, g^{(n)}(c_{i}) + g^{(n)}(c_{j}) \mbox{ 
connected} \}\]
forms a connected graph on $C$. By property G2,
applied to $g^{(n)}$, this is true iff the set of edges
\[
\{ (c_i,c_j) | c_{i}, c_{j} 
\in C, i \neq j, c_{i} + c_{j} \mbox{ 
connected} \}\]
 forms a connected graph on $C$. By claim~\ref{claim:2.0},
applied to $C$, this is true iff $\sum C$ is connected. 
}

\noindent
Let $0 \leq m \leq n$.  We now show how any mapping $g^{(n)} \in 
w^{(n)}$ can be used to construct a mapping in $w^{(m)}$.  Since, for 
any $i$ ($1 \leq i \leq N_m$), $c^{(m)}_{i}$ can be expressed 
uniquely 
as a sum of various $c^{(n)}_{j}$, let us write
\[
  c^{(m)}_{i} = c^{(n)}_{i_{1}} + \ldots + c^{(n)}_{i_{M_{i}}} \ .
\]
for all $i$ ($1 \leq i \leq N_{m}$).  In addition, let $g^{(n)} \in 
w^{(n)}$.  We define the {\em restriction} of $g^{(n)}$ to 
$c^{(m)}_{1}, \ldots, c^{(m)}_{N_{m}}$, written $g^{(n)}|_{m}$, as 
follows:
\[ 
  g^{(n)}|_{m}(c^{(m)}_{i}) = g^{(n)}(c^{(n)}_{i_{1}}) + \ldots + 
  g^{(n)}(c^{(n)}_{i_{M_{i}}}) \textrm{ for } m>0 \textrm{ and } 
  g^{(n)}|_{0} = \emptyset \ .  
\]
\begin{claim}
  Let $g^{(n)} \in w^{(n)}$ with $0 \leq m < n$.  Then $g^{(n)}|_{m} 
  \in w^{(m)}$.
\label{claim:2.3}
\end{claim}
\proof{
If $m=0$ the claim is trivial.  Suppose $m \geq 1$.
We must prove that G1 and G2 hold of $g^{(n)}|_{m}$. G1 is trivial. 
For G2, we note that, by construction,
\begin{center}
\begin{minipage}{10in}
\begin{tabbing}
$g^{(n)}|_{m}$\=$(c^{(m)}_{i})+ g^{(n)}|_{m}(c^{(m)}_{j}) \ =$\\ 
\> $g^{(n)}(c^{(n)}_{i_{1}}) + \ldots + g^{(n)}(c^{(n)}_{i_{M_{i}}})
+
g^{(n)}(c^{(n)}_{j_{1}}) + \ldots + g^{(n)}(c^{(n)}_{j_{M_{j}}}) \ .$
\end{tabbing}
\end{minipage}
\end{center}
By claim~\ref{claim:2.2}, this element of $S$ is connected iff the 
element of 
$A$
\[
c^{(n)}_{i_{1}} + \ldots + c^{(n)}_{i_{M_{i}}}
+
c^{(n)}_{j_{1}} + \ldots + c^{(n)}_{j_{M_{j}}}  = c^{(m)}_{i} + 
c^{(m)}_{j}
\]
is connected. Hence G2 holds as required.
}
% 
{\bf Stage 3: } In stage 2, we showed how any initial 
segment of \fA\ can be embedded in \fS. In this section, we show how 
these partial embeddings can be strung together into a single 
embedding of \fA\ into \fS.

\vspace{0.25cm}

\noindent 
Suppose that $g_{1}^{(n)}, g_{2}^{(n)} \in w^{(n)}$.  We say 
that $g_{1}^{(n)}$ is topologically equivalent to $g_{2}^{(n)}$, written 
$g_{1}^{(n)} \sim g_{2}^{(n)}$, if there exists a homeomorphism of 
the 
closed plane onto itself taking the elements of 
$g_{1}^{(n)}(c^{(n)})$ 
to the elements of $g_{2}^{(n)}(c^{(n)})$.

\vspace{0.25cm}

\noindent
Clearly, $g_{1}^{(n)} \sim g_{2}^{(n)}$ is an equivalence
relation on $w^{(n)}$.  By theorem~\ref{theo:3:critical}, there are only
finitely many equivalence classes under $\sim$ contained in each
$w^{(n)}$. Let us denote these by $w^{(n)}_{1}, \ldots,
w^{(n)}_{k_{n}}$. If $m \leq n$ and there exists $g^{(n)} \in
w^{(n)}_j$ such that $g^{(n)}|_{m} \in w^{(m)}_i$ then we write
$w^{(m)}_i \preceq w^{(n)}_j$.  If, in addition, $m < n$, we write
$w^{(m)}_i \prec w^{(n)}_j$.

\vspace{0.25cm}

\noindent
Now form the graph $\Omega$ whose nodes are all the $w^{(n)}_{i}$, 
and whose edges are 
\[
\{ (w^{(n)}_{i}, w^{(n+1)}_{j}) | w^{(n)}_{i} \prec w^{(n+1)}_{j} \} 
\]
%
(i.e.~$\Omega$ has no multiple edges). By claim~\ref{claim:2.3}, $\Omega$ is 
connected.

\begin{claim}
  $\Omega$ is a tree. That is, if $w^{(n)}_i \prec w^{(n+1)}_k$
and $w^{(n)}_j \prec w^{(n+1)}_k$ then $i = j$.
\label{claim:3.1}
\end{claim}
\proof{Obvious.}
By claim~\ref{claim:2.1}, $\Omega$ is infinite. 
By theorem~\ref{theo:3:critical}, $\Omega$ is locally finite. Then, by 
K\"{o}nig's infinity lemma, for any node of $\Omega$,
there exists an infinite path 
in $\Omega$ starting at that node.
Let $\pi$ be an infinite path in $\Omega$ starting at 
the node $\{\emptyset\} =w^{(0)}_{1}$. 
Since $\Omega$ is a tree, this path gives us a
sequence of equivalence classes 
$w^{(0)}_{1} \prec w^{(1)}_{i_{1}} \prec w^{(2)}_{i_{2}} \prec \ldots$.
\begin{claim}
  Let $g^{(n)} \in w^{(n)}_{i}$ and $(w^{(n)}_{i},w^{(n+1)}_{j})$ be 
  an edge of $\Omega$.  Then there exists a $g^{(n+1)} \in 
  w^{(n+1)}_{j}$ such that $g^{(n+1)}|_{n} = g^{(n)}$.
\label{claim:3.4}
\end{claim}
\proof{
Since $(w^{(n)}_{i},w^{(n+1)}_{j})$ is an edge of 
$\Omega$, there exists an $h^{(n+1)} \in w^{(n+1)}_{j}$ and a 
homeomorphism $\mu$ of the closed plane onto itself such that $\mu 
\circ (h^{(n+1)}|_{n}) = g^{(n)}$.  Denote 
those members of $c^{(n+1)}_{1}, \ldots, 
c^{(n+1)}_{N_n}$ which sum to $c^{(n)}_{1}$ by $d_1,
\ldots, d_m$, and denote 
$h^{(n+1)}|_{n}(c^{(n)}_{1})$ by $r$.
Then
$h^{(n+1)}(d_1), \ldots, h^{(n+1)}(d_m)$ 
form a connected partition of $r$ in $S$, so by
lemma~\ref{lma:0:homo1}, there exists a connected partition
$s_{1}, \ldots, s_m$ of $\mu(r)$ and a
homeomorphism $\nu_{1}$ 
of 
the closed plane onto itself, mapping $h^{(n+1)}(d_i)$ to
$s_i$, for all $i$ ($1 \leq i \leq m$)
such that 
$\nu_{1}|_{-r} = 
\mu|_{-r}$. By repeating this step 
for $c^{(n)}_{2}, \ldots, c^{(n)}_{N_{n}}$, we can construct a 
homeomorphism $\nu$ of the closed plane onto itself 
mapping every $h^{(n+1)}(c^{(n+1)})$ to
an element of $S$ such that 
$\nu(h^{(n+1)}|_{n}(c^{(n)}_{i})) = \mu(h^{(n+1)}|_{n}(c^{(n)}_{i})) = 
g^{(n)}(c^{(n)}_{i})$ for all $i$ ($1 \leq i \leq N_{n}$).  Hence 
$(\nu \circ h^{(n+1)})|_{n} = \mu \circ (h^{(n+1)}|_{n}) = g^{(n)}$.  
Clearly $\nu \circ h^{(n+1)} \in w^{(n+1)}_{j}$, since $h^{(n+1)} \in 
w^{(n+1)}_{j}$.  Hence $g^{(n+1)} = \nu \circ h^{(n+1)}$ is our 
required element.  
}
%
By claim~\ref{claim:3.4}, we can extract a sequence of 
embeddings: \[
\begin{array}{rccc}
w^{(0)}_{i_{0}} \prec & w^{(1)}_{i_{1}} \prec & w^{(2)}_{i_{2}} \prec & \ldots 
\\
\vdots \hspace{0.2cm} & \vdots  & \vdots & \vdots \\
\emptyset = f^{(0)}, & f^{(1)}, &  f^{(2)}, &  \ldots 
\end{array}
\]
with the property that, for all $m,n$ ($0 \leq m < n$), $f^{(n)}|_{m} 
= f^{(m)}$. 

\vspace{0.25cm}

\noindent
Now let $a \in A$ be such that $a = c^{(n)}_{i_{1}} + \ldots +
c^{(n)}_{i_{k}}$.  Then we define
\[
f(a) = f^{(n)}(c^{(n)}_{i_{1}}) + \ldots + f^{(n)}(c^{(n)}_{i_{k}}) \ 
.
\]
(If $a = 0$, we take the right-hand side of this definition to denote
$0 \in S$.)

The fact that $f^{(n)}|_{m} = f^{(m)}$ whenever $0 \leq m < n$ means 
that this mapping is well defined. It is 
easy to see that $f:A \rightarrow S$ is a Boolean algebra isomorphism;
moreover, by claim~\ref{claim:2.2}, $f(a)$ is connected iff $a$ is 
connected. Thus we might as well take $A$ to be a subset 
of $S$; then the previously distinct uses of the Boolean functions and
constants and the term ``connected'' become unambiguous. That is, 
we have proved:
\begin{claim} 
  $\fA \subseteq \fS$.
\label{claim:3.5}
\end{claim}

\noindent
{\bf Stage 4: } Having established claim~\ref{claim:3.5},
the next step is to prove that \fA\ has {\em enough}
elements to serve as a substitute for the whole of \fS .
In the sequel, we shall forget our previous enumeration of $A$ and 
just take $a_{1}, \ldots, a_{n}$ to be arbitrary elements of $A$.

\vspace{0.25cm}

\begin{definition}
  If $r_{1}, \ldots, r_{n} \in S$ form a partition and $r_{i}$ is a Jordan 
  region for all $i$ ($1 \leq i \leq n$), we say that $r_{1}, \ldots, r_{n}$ 
  is a {\em Jordan} partition.  If $r_{i} + r_{j}$ is connected, $i \neq j$ 
  we say that $r_{i}$ and $r_{j}$ are {\em neighbours}.  If $r_{1}, \ldots, 
  r_{n}$ is a Jordan partition such that, for any neighbour $r_{i}$ of 
  $r_{1}$, $-(r_{1} + r_{i})$ is connected, then we say that the partition is 
  {\em radial about} $r_{1}$.
\end{definition}

\noindent
By lemma~\ref{lma:0:jordan_arc}, if 
$r_{1}, \ldots, r_{n}$ is a Jordan partition radial about
$r_{1}$ such that $r_{1}$ has at least 2 neighbours, then, for any
neighbour $r_{i}$ of $r_{1}$, $\mathcal{F}(r_{1}) \cap
\mathcal{F}(r_{i})$ is a Jordan arc. Recall that, if $r_1, \ldots,
r_n$ and $s_1, \ldots, s_n$ are regions of $S$ such that there is a
homeomorphism of the closed plane onto itself mapping $r_i$ to $s_i$
for all $i$ ($1 \leq i \leq n$), then we say that $r_1, \ldots, r_n$
and $s_1, \ldots, s_n$ are {\em topologically equivalent} and write $r_1,
\ldots, r_n \sim s_1, \ldots, s_n$.
%
\begin{claim}
  Let $a_{1}, \ldots, a_{n} \in A$ be a Jordan partition radial about
  $a_{1}$ such that $a_{1}$ has at least $3$ neighbours. Let $b_{1},
  b_{2} \in S$ be Jordan regions with $a_{1} = b_{1} \oplus b_{2}$. 
Then there
  exist $c_{1},c_{2} \in A$ such that $a_{1}, \ldots, a_{n},
  c_{1},c_{2} \sim a_{1}, \ldots, a_{n}, b_{1}, b_{2}$.
\label{claim:4.1}
\end{claim}
\proof{
Since $a_1, b_{1}, b_{2}$ are Jordan regions with $a_{1} = b_{1} 
\oplus b_{2}$, $b_{1}$ and $b_{2}$ must be separated by a cross-cut 
$\gamma$ in $a_{1}$.  For any neighbour $a_i$ of $a_1$, 
$\mathcal{F}(a_{1}) \cap \mathcal{F}(a_{i})$ is a Jordan arc.  By 
inspection, any point on $\mathcal{F}(a_{1})$ 
lies on either one or two Jordan arcs of the form $\mathcal{F}(a_{1}) 
\cap \mathcal{F}(a_{i})$ where $a_{i}$ is a neighbour of $a_{1}$.
(See fig.~\ref{fig:radial}a for examples.) 
\begin{figure}[tbp]
        \centerline{
        \begin{tabular}{ccc}
         \resizebox{!}{3.5cm}{\input{axiomfig2a.pstex_t}} 
          & \resizebox{!}{3.5cm}{\input{axiomfig2b.pstex_t}}
          & \resizebox{!}{3.3cm}{\input{axiomfig2c.pstex_t}} \\
         $\chi(p) = \{i\} \ \ \chi(q)=\{i, j\}$
          & $\chi(\gamma) = \{\{i, j\}, \{k\}\}$
          & $\chi(\gamma) = \{\{i\}\}$ \\
         a & b & c 
        \end{tabular} }
        \caption{The hub $a_{1}$ of a radial partition}
        \protect\label{fig:radial}
\end{figure}

Let $p \in \mathcal{F}(a_{1})$.  We define the {\em character of} $p$,
written $\chi(p)$ to be the set of those $i$ ($2 \leq i \leq n$) such
that $a_{i}$ is a neighbour of $a_{1}$ and $p \in \mathcal{F}(a_{i})$.
Then, $\chi(p)$ has either
1 or 2 elements. If $\chi(p)$ has one element, then $p$ lies on the Jordan arc
$\mathcal{F}(a_{1}) \cap \mathcal{F}(a_{i})$, but not at its
endpoints.  If $\chi(p)$ has two elements, 
then since $a_{1}$ has at least three
neighbours, $\chi(p)$ determines $p$.  Now let $\gamma$ be a cross-cut
in $a_{1}$.  We define the {\em character of} $\gamma$, written
$\chi(\gamma)$ to be the set of characters of its endpoints.  (See
fig.~\ref{fig:radial}b and c for examples.)  It is routine to show
that, if $\gamma_{1}$ and $\gamma_{2}$ are two such cross-cuts and
$\chi(\gamma_{1}) = \chi(\gamma_{2})$, there is a homeomorphism of the
closed plane onto itself taking $a_{i}$ to itself for all $i$ ($1 \leq
i \leq n$) and taking $\gamma_{1}$ to $\gamma_{2}$.  So, to prove the
lemma, it suffices to establish that, if $\gamma_{1}$ is any cross-cut
in $a_{1}$, there exist Jordan regions $c_{1}, c_{2} \in A$ with
$a_{1} = c_{1} \oplus c_{2}$ such that the cross-cut $\gamma_{2}$
separating $c_{1}$ and $c_{2}$ in $a_{1}$ satisfies $\chi(\gamma_{1})
= \chi(\gamma_{2})$.

\vspace{0.25cm}

\noindent 
Let the endpoints of $\gamma_{1}$ be $p$ and $q$.
We prove the result for the special case where $\chi(\gamma)$, 
$\chi(p)$ and $\chi(q)$ all contain two elements; 
the other cases are dealt with similarly.
Fig.~\ref{fig:splitup}a
\begin{figure}[tbp]
        \centerline{
         \begin{tabular}{cccc}
           \resizebox{!}{3cm}{\input{axiomfig3a.pstex_t}} 
           & \resizebox{!}{3.3cm}{\input{axiomfig3b.pstex_t}}
           & \resizebox{!}{3.3cm}{\input{axiomfig3c.pstex_t}}
           & \resizebox{!}{3.3cm}{\input{axiomfig3d.pstex_t}} \\              
           a & b & c & d
         \end{tabular} }
        \caption{The construction of a cross-cut with a given character}
        \protect\label{fig:splitup}
\end{figure}
shows the sub-case where $\chi(p)$ and $\chi(q)$ are nondisjoint; 
fig.~\ref{fig:splitup}b shows the sub-case where $\chi(p)$ and 
$\chi(q)$ 
are disjoint. 

\vspace{0.25cm}

\noindent
The sub-case of fig.~\ref{fig:splitup}a is trivial: the 
axiom~\ref{ax:shadow} with $a_{1}$ substituted for $x$ and $a_{i}$ 
%
% changed a_{j} to a_{i}. chack that this corresponds to fig7a
% (iep 15/3/98)
%
for $y$ immediately guarantees the existence of $u, v \in A$ 
partitioning $a_{1}$, and hence separated by a cross-cut $\gamma_{2}$; 
moreover the connectivity conditions on $u$ and $v$ mean that 
$\gamma_{1}$ and $\gamma_{2}$ have the same endpoints, so that 
$\chi(\gamma_{1}) = \chi(\gamma_{2})$.

\vspace{0.25cm}

\noindent
The sub-case of fig.~\ref{fig:splitup}b requires a little more work.  
However, two applications of axiom~\ref{ax:shadow} guarantee the 
existence in $A$ of the regions $a_{i}', a_{k}'$ shown in 
fig.~\ref{fig:splitup}c.  Axiom~\ref{ax:split} then guarantees that 
the region labelled $a_{1}'$ in fig.~\ref{fig:splitup}c can be split 
into two regions as shown in fig.~\ref{fig:splitup}d.  Summing 
together appropriate subdivisions of $a_{1}$ produces $c_{1}, c_{2} 
\in A$ separated by an arc $\gamma_{2}$ satisfying $\chi(\gamma_{1}) 
= \chi(\gamma_{2})$.  }
%
The rest of this section is devoted to showing that we can relax the 
conditions of claim~\ref{claim:4.1}.  First, we establish some results 
enabling us to decompose elements of $A$ in various ways.
%
\begin{claim}
  Let $a \in A$.  Then there exists $n \geq 0$ and Jordan regions 
  $b_{1}, \ldots, b_{n} \in A$ such that $a = b_{1} \oplus \ldots 
  \oplus b_{n}$.
\label{claim:4.2}
\end{claim}
(When $n = 0$, the right-hand side of this equation is taken to 
denote $0 \in S$).

\vspace{0.25cm}

\noindent 
\proof{
We may as well assume that $a$ has one component and $a \neq 1$, 
since extending the 
result to the other cases is trivial.  We proceed by induction on the 
number $k$ of components of $-a$.  If $k = 1$, $a$ is itself a Jordan 
region by lemma \ref{lma:0:jordan} and the result is certainly true.  
If $k > 1$, let $c, d$ be distinct components of $-a$.  By 
lemma~\ref{lma:0:complexcon} (setting $r = a$ and 
$s = 0$), $a+c$ and $a+d$ are connected.  By 
axiom~\ref{ax:split}, substituting $a$ for $x$, $c$ for $y$ and $d$ 
for $z$, we are guaranteed the existence of connected regions $u,v \in 
A$, partitioning $a$ such that $u+c$, $u+d$, $v+c$ and $v+d$ are all 
connected.  Hence, both $-u$ and $-v$ have fewer than $k$ components.  
By inductive hypothesis, $u$ and $v$ can be partitioned into finitely 
many Jordan regions in $A$.  The result follows immediately.  
}
%
\begin{claim}
  Let $n \geq 1$ and let $a_{1}, \ldots, a_{n} \in A$.  There exists a 
  Jordan partition $c_{1}, \ldots, c_{N} \in A$ such that, for all $i$ 
  ($1 \leq i \leq n$), $a_i$ can be expressed as the sum of zero or more 
  $c_{i}$.
\label{claim:4.3}
\end{claim}
\proof{Immediate given claim~\ref{claim:4.2}.}
%
\begin{claim}
  Let $n > 1$ and let $a_{1}, \ldots, a_{n} \in A$ be a partition with 
  $a_{1}$ a Jordan region.  There exists a Jordan partition $a_{1}, 
  c_{2}, \ldots, c_{N} \in A$ radial about $a_{1}$, such that, for all 
  $i$ ($2 \leq i \leq n$), $a_{i}$ can be expressed as the sum of 
  various $c_{j}$.
\label{claim:4.4}
\end{claim}
\proof{
By claim~\ref{claim:4.3}, we can find a Jordan partition 
$a_1, b_2, \ldots, b_M$ such that, for all $i$ ($2 \leq i \leq n$) 
$a_i$ can be expressed as the sum of various $b_j$.  We now show that 
the $b_j$ can be decomposed if necessary to form the required 
elements $c_{2}, \ldots, c_{N}$.

\vspace{0.25cm}

\noindent Suppose that $b_i$ is a neighbour of $a_1$ such that 
$-(a_1+b_i)$ is not connected.  Then let $d \neq e$ be two components 
of $-(a_1+b_i)$.  By lemma~\ref{lma:0:complexcon}, letting $r$ be 
$b_i$, $s$ be $a_1$ and, $t$ be successively $d$ and $e$, we know 
that both $b_i +d$ and $b_i + e$ are connected.  In 
axiom~\ref{ax:split}, substitute $b_i$ for $x$, $d$ for $y$ and $e$ 
for $z$.  Then there exist connected regions $u,v \in A$ partitioning 
$b_i$ such that $u+d$, $u+e$, $v+d$ and $v+e$ are all connected.  It 
follows that $u$ and $v$ are Jordan regions such that $d$ and $e$ 
belong to the same component of $-(a_1 + u)$ and also to the same 
component of $-(a_1 +v)$.  Hence both $-(a_1 + u)$ and $-(a_1 +v)$ 
have fewer components than $-(a_1 + b_i)$.  By replacing $b_i$ with 
$u$ and $v$ and proceeding as before, we eventually reach a Jordan 
partition radial about $a_1$.}
%
\begin{claim}
  In claim~\ref{claim:4.4}, the $c_2, \ldots, c_N$ can be chosen so 
  that $a_1$ has at least three neighbours.
\label{claim:4.5}
\end{claim}
\proof{Immediate given claim~\ref{claim:4.4} and  axiom~\ref{ax:split}.}
%
Now let us return to the task of relaxing the conditions of 
claim~\ref{claim:4.1}.
\begin{claim}
  Let $n > 1$ and let $a_{1}, \ldots, a_{n} \in A$ be a partition such 
  that $a_{1}$ is a Jordan region.  Let $b_{1}, b_{2} \in S$ be Jordan 
  regions with $a_{1} = b_{1} \oplus b_{2}$.  Then there exist 
  $c_{1},c_{2} \in A$ such that $a_{1}, \ldots, a_{n}, c_{1},c_{2} 
  \sim a_{1}, \ldots, a_{n}, b_{1}, b_{2}$.
\label{claim:4.6}
\end{claim}
\proof{Immediate given claims~\ref{claim:4.1} and~\ref{claim:4.5}.}
\begin{claim}
  Let $n>1$ and let $a_{1}, \ldots, a_{n} \in A$ be a partition such 
  that $a_{1}$ is a Jordan region.  Let $b \in S$ be such that $b \leq 
  a_1$.  Then there exists $c \in A$ such that $a_{1}, \ldots, a_{n}, 
  c \sim a_{1}, \ldots, a_{n}, b$.
\label{claim:4.7}
\end{claim}
\proof{
By claim ~\ref{claim:4.2}, we can find a Jordan partition 
$b_1, \ldots, b_m$ of $a_1$ such that $b$ can be expressed as the
sum of various $b_j$. It suffices to show that there are 
$c_1, \ldots, c_m \in A$ such that
\[
   a_{1}, \ldots, a_{n}, b_1, \ldots, b_m \sim
   a_{1}, \ldots, a_{n}, c_1, \ldots, c_m \ 
\]
We proceed by induction on $m$. If $m = 1$, then $b_1 = a_1$ and
we are done. If $m > 1$,
by lemma~\ref{lma:jordansubselect}, we can renumber the $b_i$ if
necessary so that $b_1$ and $b'_2= b_2 + \ldots + b_m$ are Jordan 
regions
satisfying $a_1 = b_1 \oplus b'_2$. By claim~\ref{claim:4.6}, there
exist $c_1, c_2' \in A$ such that
$a_{1}, \ldots, a_{n}, b_1,b'_2 \sim a_{1}, \ldots, a_{n}, c_1,c'_2$.
Let $\nu$ be a homeomorphism of the closed plane onto itself
mapping $a_i$ to itself, $b_1$ to $c_1$
and $b'_2$ to $c'_2$. It follows from lemma~\ref{lma:0:homo1}
that $\nu$ can be chosen
so that $\nu(b_i) \in S$ for all $i$ ($2 \leq i \leq m$). But then
the $\nu(b_i)$ form a Jordan partition of $c'_2$ in the partition
$c'_2, c_1, a_2, \ldots, a_n$. By inductive hypothesis, there exist
$c_2, \ldots, c_m \in A$ such that
\[
  c'_2, c_1, a_{2}, \ldots, a_{n}, \nu(b_2), \ldots, \nu(b_m) \sim
  c'_2, c_1, a_{2}, \ldots, a_{n}, c_2, \ldots, c_m \ .
\]
The result then follows immediately.
}
%
\begin{claim}
  Let $n>1$ and let $a_{1}, \ldots, a_{n} \in A$ be a Jordan 
  partition.  Let $b \in S$.  Then there exists $c \in A$ such that 
  $a_{1}, \ldots, a_{n}, c \sim a_{1}, \ldots, a_{n}, b$.
\label{claim:4.8}
\end{claim}
\proof{
We let $b = b.a_1 + \ldots + b.a_n$ By considering these terms 
separately, we use claim~\ref{claim:4.7} and an induction similar to 
that used in the proof of claim~\ref{claim:4.7}.  The details are 
routine.
}
\begin{claim}
  Let $n \geq 0$ and let $a_1, \ldots, a_n \in A$.  Let $b \in S$.  
  Then there exists $c \in A$ such that $a_1, \ldots, a_n, b \sim a_1, 
  \ldots, a_n, c$.
\label{claim:4.9}
\end{claim}
\proof{Immediate given claims~\ref{claim:4.3} and~\ref{claim:4.8}.}
%
Thus, we have established that $A$ forms a 
topologically homogeneous subset of $S$
in the sense made precise by claim~\ref{claim:4.9}.

\vspace{0.25cm}

\noindent
{\bf Stage 5: } We now have all the important elements for our proof.
\begin{claim}
  $\fA \preceq \fS \ .$
\label{claim:5.1}
\end{claim}
\proof{
By claim~\ref{claim:3.5}, $\fA \subseteq \fS$.  Let $n \geq 0$ and let 
$\phi(x_1, \ldots, x_n)$ be any formula of the form $\exists y 
\psi(x_1, \ldots, x_n, y)$.  According to the Tarski-Vaught lemma,
we can show that for any $a_1, \ldots, a_n \in A$ such that $\fS 
\models \phi[a_1, \ldots, a_n]$, there exists $c \in A$ such that $\fS 
\models \psi[a_1, \ldots, a_n,c]$, then $\fA \preceq \fS \ .$

\vspace{0.25cm}

\noindent
Let $a_1, \ldots, a_n$ and $\phi$ be as described.  Then there exists 
$b \in S$ such that $\fS \models \psi[a_1, \ldots, a_n,b]$.  By 
claim~\ref{claim:4.9}, there exists $c \in A$ such that $a_1, \ldots, 
a_n,b \sim a_1, \ldots, a_n,c$.  By lemma~\ref{lma:0:homotype}, $\fS 
\models \psi[a_1, \ldots, a_n,c]$.  
}
%
By the construction of $A$, $\fA \models \Phi$.
By claim~\ref{claim:5.1}, $\fS \models \Phi$. This completes the
proof of theorem~\ref{theo:complete}.
\boxterm
Finally, we have the result we want.
\begin{corollary}
Let $T_{\$}$ denote the set of sentences which are \$-theorems.
Then $T_{\$} = {\rm Th}(\fS) = {\rm Th}(\fR)$.
\label{coro:0}
\end{corollary}
\proof{Immediate by theorems~\ref{theo:sound}, \ref{theo:complete} and lemma~\ref{lma:iso:4}.}
%
\section{Conclusions}
This paper has presented a calculus for mereotopological reasoning in
which spatial regions are treated as primitive entities. We defined a
language $\cL$ with a one-place predicate $c(x)$, the function-symbols $+$,
$ \ . \ $ and $-$ and the constants $0$ and $1$. We provided an
interpretation \fR~for $\cL$ in which regions are identified with
polygonal regular sets of the real plane. Under this
interpretation, the predicate $c(x)$ is read as ``$x$ is connected''
(in the usual sense) and the Boolean function-symbols and constants
are given their obvious meanings in terms of
the appropriate regular Boolean algebra.
We proved the soundness and completeness of our calculus with respect
to an isomorphic model \fS~and therefore with respect to \fR~as well.  

Thus, although our calculus takes regions to be primary, it is
guaranteed an interpretation in terms of a model of the plane in which
regions are identified with polygonal, regular subsets of $\R^2$.
That is: the theorems of the calculus are precisely those formulae
made true by this model. Hence, our mereotopological calculus really
can claim to be a calculus of spatial regions. For there is good
reason to suppose that the polygonal ontology assumed here constitutes
an adequate model of 2-dimensional space for most practical purposes. (In
particular, this ontology is the one employed by nearly all computer
systems specialized for plane spatial representation such as
geographic information systems.)  In this respect, we claim, our
calculus is superior to other mereotopological calculi that have been
proposed in the literature.

Throughout this paper, we have restricted ourselves to a spatial
ontology featuring regular open polygons as its only elements, and the
question naturally arises as to whether this ontology could be
liberalized. In Pratt and Lemon~\cite{PrattLemon97b}, it was shown
that the domain of regular open polygons in the open plane could be
replaced by the domain of regular {\em definable} sets in the open
plane without change to the resulting theory.  Other natural
liberalizations of the polygonal ontology, however, do not support the
same mereotopological facts as $\fS$. We have already seen that
allowing arbitrary regular open sets into the domain of quantification
is one such liberalization.  Moreover, the authors have recently shown
that replacing half-planes with arbitrary Jordan regions in the
construction of $\fS$ also results in a model not elementarily
equivalent to $\fS$. We at present lack a general characterization of
the possible liberalizations of our polygonal ontology which result in
elementarily equivalent models.  Of greater practical interest is the
situation with well-behaved Boolean subealgebras of ${\rm
RO}(\R^3)$. At present, we know of know satisfactory treatment of the
three-dimensional case.

\section*{Acknowledgements}
With thanks to the referees, the Leverhulme Trust (grant number
F/120/AQ), the British Council's British-German Academic Research
Collaboration Programme (project 720), and  the European
Commission TMR Programme (contract number ERBFMBICT972035). The authors
also wish especially to acknowledge the help of Jeff Paris and Peter
Aczel.

\newpage

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% Bibliography
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\bibliographystyle{plain}
\bibliography{space}

%\tableofcontents  
\end{document}



