text:
\section{The early-type star population of NGC\,6231}

\begin{figure}[!t]
\plotfiddle{OBhisto_shaded.ps}{9cm}{0}{80}{80}{-245}{-185}
\caption{Distribution of the early-type star population within the XMM-Newton f.o.v.\ among the different spectral types and luminosity classes. The shaded regions correspond to detected X-ray emitters.}
\end{figure}

NGC\,6231 is a young  open cluster regarded as the nucleus of the Sco OB1 association \citep{PHC91}. Located at a distance of about 1.7 kpc, it contains a few hundred early-type stars and offers an excellent sample of different spectral types and luminosity classes. Hence NGC\,6231 has been chosen as the target of an XMM-Newton observing campaign in the framework of the guaranteed time of the Optical Monitor consortium. The XMM-Newton field of view (f.o.v.) was centered on the colliding wind binary (CWB) HD\,152248 in the core of the cluster \citep{SRG01, SSG04}. Within the 15 arcmin radius of the f.o.v., 110 early-type stars are reported in the literature, among which 15 O-type objects, either single or multiple, and a Wolf-Rayet system (WR\,79). About one half of the O-type objects are spectroscopic binaries for which we have detected the signature of both components using high resolution high S/N ratio spectra. Among the presumably single O-type stars, another half shows, on time-scales of a few days, small RV shifts of a peak-to-peak amplitude of about 15 to 30 km\,s$^{-1}$. These could not be associated to a possible multiplicity yet and we will therefore consider them as single in the following. Figure 1 presents the distribution of the early-type star population of the cluster among the different spectral types and luminosity classes.

\section{X-ray observations of NGC\,6231}

The XMM-Newton campaign consisted of six 30-ksec exposures spread over five days, for a total nominal duration  of about 180 ksec. Despite some background flares, this data set  forms one of the deepest X-ray views towards a young open cluster yet performed. Figure 2 presents a combined image of the three EPIC instruments and demonstrates that the field in the X-ray domain is, indeed, very crowded.

Based on the {\it edetectchain} of the Science Analysis System (SAS) software, we detected 610 X-ray sources in the f.o.v. An optical counterpart within a cross-correlation radius of 3 arcsec could be identified for about 520 of these objects ($\approx85$\%). Most of them seem to belong to the cluster. The estimation of the detection limit is a more tricky issue, the sensitivity of XMM-Newton being clearly not uniform throughout the f.o.v. For NGC\,6231 early-type stars displaying a typical temperature of 0.7\,keV, we estimate this limit to be about 3 to 8 10$^{-15}$\,erg \,s$^{-1}$\,cm$^{-2}$ depending on the position on the detectors. At the distance of the cluster, this yields luminosity limits ranging from 1.0 to 2.5\,10$^{30}$\,erg\,s$^{-1}$. More details on the estimation of the detection limit and on the factors influencing it will be given in \citet{Sana05}.

About 40 X-ray sources are associated with early-type stars and Fig.1 presents their repartition among the early-type population of the cluster. All the O-type stars, both singles and binaries, are detected in the X-ray domain, as are all the supergiants and most of the giants in the f.o.v.  On the contrary, only a small fraction ($\sim$30\%) of the B-type main-sequence stars are detected. We have obtained high resolution snapshot spectra of most of the B-type X-ray emitters and, except in one case, we were not able to detect evidence of binarity. Their RVs are further in good agreement with the mean velocity of the cluster. We can therefore reasonably consider them as singles. About one fourth of the B-type emitters are foreground objects while two other objects are known $\beta$\,Cep stars belonging to the cluster.

\begin{figure}[!t]
\plottwo{imgtot_col.eps}{lxlbol4sacaco.ps}
\caption{{\bf Left:} Combined three-colour X-ray image of NGC\,6231: red [0.5--1.0\,keV]; green [1.0-2.5\,keV]; blue [2.5-10.0\,keV]. This image appears in colour in the electronic version of the paper. {\bf Right:} $L_\mathrm{X}$ vs.\ $L_\mathrm{bol}$ diagram for the early-type stars of NGC\,6231 detected by XMM-Newton. Both axis are expressed in terms of $\log$(erg\,s$^{-1}$). The unabsorbed X-ray luminosities are restricted to the 0.5-10.0\,keV energy band. Solid lines indicate the \citeauthor{BSC97}\ relations for O- and B-type stars in the 0.1-2.0\,keV band. The dashed line gives an estimation of our detection limit for early-type stars. O and B stars are respectively indicated by filled and open symbols. Triangles are for binaries, squares for stars displaying small RV shifts and circles for presumably single stars. The asterisks indicate foreground objects.}
\end{figure}

\section{$L_\mathrm{X} / L_\mathrm{bol}$ relationship}

Among the 40 early-type X-ray emitters, we selected 31 of them that are bright and isolated enough. We extracted their X-ray spectra using the merged event-list of the 6 pointings. We then  estimated their X-ray fluxes by adjusting up to three-temperature optically thin thermal plasma models (\texttt{mekal} models). For this, we adopted individual ISM absorbing columns to reflect the differential reddening across the field \citep*{SBL98}. Most of these X-ray spectra are well described by \texttt{mekal} models with temperatures below 1\,keV. We then computed the unabsorbed X-ray fluxes and, adopting a distance modulus of 11.07 for NGC\,6231, we obtained the X-ray luminosities. Finally, based on the photometry of \citet{SBL98}, we computed the bolometric luminosity of the selected objects.

Figure 2 presents the  $L_\mathrm{X} / L_\mathrm{bol}$ diagram for the early-type stars of NGC\,6231. There is a clear separation between the behaviours of the  O- and  B-stars with a cut-off limit at $L_\mathrm{bol}\approx10^{38}$\,erg\,s$^{-1}$, as previously proposed by \citet {BSC97}. Though the dispersion is quite large, there is no obvious separation between single and binary O-type stars in our sample, except for the CWB HD\,152248 ($\log\left(L_\mathrm{X}\right)\approx33 $). Most of the detected B-stars are far more X-ray luminous than what is expected from the \citeauthor{BSC97}\ relation. However a direct comparison is difficult because of the different energy bands considered. In Fig. 2, the \citeauthor{BSC97}\  relations (obtained in the 0.1-2.0\,keV band) are only given as indications. The non-detection of a large fraction of the B-type star population is more puzzling, indicating that most of them have an X-ray luminosity below about 10$^{30}$\,erg\,s$^{-1}$.  This might be explained by a largely spread B-star emission, in which case we only observed the upper part of the distribution. However, if the dispersion was approximately uniform, we would expect to observe more stars slightly above the detection limit, in the region of the plot between about $\log(L_\mathrm{bol})=36$ and 38. This could suggest a bimodal distribution of the B-type stars in the $L_\mathrm{X} / L_\mathrm{bol}$ diagram. This point clearly deserves more attention in a near future.

\section{X-ray variability}

This last section briefly investigates the variability of the detected X-ray sources. Our XMM-Newton campaign actually consisted of six 30-ksec exposures spread over 5 days. The first aim was to monitor the X-ray emission from the five massive binaries  with a period shorter than 6 days in the f.o.v. These data however provide a good opportunity to probe the variability of various types of X-ray sources on a time-scale of a few days.

We thus perform a $\chi^2$ variability test. We adopted the null hypothesis of a constant count rate, in the 0.5-10.0\,keV energy band, for each of the six pointings and we required a 90\% confidence level in each EPIC instrument to reject that hypothesis. About 40 \% of all the sources and 33\% of the early-type X-ray emitters present a clear variability, while 25\% do not show any sign of variability in any of the instruments. Requiring a 99\% confidence level does not affect this pattern much since 25\% of the sources are  still reported as variable. This fraction is much larger than previously thought, clearly indicating that variability is a common phenomenon among stellar X-ray emitters.

Finally, one half of the short period O-type binaries present definite variability while another fourth display some sign of variability in at least one instrument. The emission from the WR system remains approximately constant throughout the six pointings, but we actually covered only 5 days out of its 9-day period. O-star X-ray variability does not seem to be exclusively related to binarity and could therefore not be uniquely explained by a wind-wind interaction scenario.

\section{Conclusions}

Using the XMM-Newton X-ray observatory, we performed one of the deepest X-ray investigations towards a young open cluster. Of an effective duration of at least 170\,ksec, our campaign reveals a very crowded field with 610 detected sources, among which 42 early-type stars.
We obtained the $L_\mathrm{X} / L_\mathrm{bol}$ relation for the early-type emitters of the cluster. We confirm the clear dichotomy between the behaviours of the  O- and B-type stars. No systematic X-ray overluminosity could be assigned to early-type binaries. Most of the B-type stars of the cluster are  more X-ray luminous than expected from the \citeauthor{BSC97}\ relation.
We finally investigated the variability of the X-ray sources and showed that variability affects a large fraction of the detected sources.

\acknowledgments{
This work was based on observations collected with XMM-Newton, an ESA Science Mission with instruments and contributions directly funded by ESA Member States and the USA (NASA). HS is a Research Fellow FNRS (Belgium); EG and GR are Research Associates FNRS (Belgium). HS is grateful to the FNRS (Belgium), to the ``Patrimoine de l'Universit\'e de Li\`ege'' and to the meeting SOC for contributing to his participation at this workshop. This research is also supported in part by contract P5/36 ``P\^ole d'Attraction Interuniversitaire'' (Belgian Federal Science Policy Office) and through the PRODEX XMM-OM and INTEGRAL projects. The SIMBAD database has been consulted for the bibliography.  }


text:
\section{Introduction}

In J\'onsson and Tarski's seminal \cite{1951}, the authors produced the very general definition of a \emph{Boolean algebra with operators} by building upon the foundation provided by the class of Boolean algebras. This factorisation of concerns into, firstly, the Boolean order structure, and later, any additional operations is still conspicuous when one examines the subsequently obtained duality between Boolean algebras with operators and descriptive general frames that has proved to be so important in modal logic \cite[Chapter 5: Algebras and General Frames]{blackburn_rijke_venema_2001}. And a similar remark can be made for the discrete duality that exists between, on the one hand, complete and atomic Boolean algebras with completely additive operators, and on the other hand, Kripke frames.

Whilst the Boolean framework is applicable to many famous classes of structures modelling relations---relation algebras and cylindric algebras are the foremost examples---it is not applicable to algebras modelling partial functions. This is for the simple reason that collections of partial functions cannot be relied upon to be closed under unions, only under unions of `compatible' functions. Though the theory of Boolean algebras with operators has been greatly generalised, weakening the ordered component all the way down to posets \cite{gehrke1994bounded, GEHRKE2001345, 10.2307/27588391}, it is not, in fact, a surfeit of order structure that is the culprit here. Indeed a moment's reflection reveals that the inclusion order is not in general enough to reveal whether two functions agree on any shared domain they may have.

There is growing interest in dualities for algebras modelling partial functions. More specifically, there are by now a number of duality theorems, proven by researchers working on inverse semigroups, having on one side: algebras modelling partial \emph{injective} functions and on the other: certain categories/groupoids or generalisations thereof \cite{lawson_2010, lawson2012non, kudryavtseva2017perspective}.\begin{NoHyper}\footnote{There are also categorical equivalences, for example \cite{doi:10.1080/00927870902887096}, but they are not our target in this work.}\end{NoHyper} Recently, a similar result has been obtained for a specific signature of not-necessarily-injective partial functions \cite{2009.07895}.

Can such results be organised into a general framework in the spirit of Boolean algebras with operators? In this paper we investigate algebras of partial functions in a signature that could be a candidate to be the equivalent of the Boolean signature in this framework. The signature is: \emph{relative complement} and \emph{domain restriction}. We have chosen the signature so as to provide us with two things:
\begin{itemize}
\item
a well-behaved order structure,
\item
compatibility information.
\end{itemize}
We show that the abstract class of isomorphs of such algebras of partial functions is axiomatised by a finite number of equations (\Cref{axiomatisation}). One might term this abstract class the class of `compatibility algebras'. Our signature is relatively unusual in that it does not include the composition operation on partial functions.
But we envisage a future theory of `compatibility algebras with operators', in which familiar operators on partial functions, such as \emph{composition}, \emph{range}, and \emph{converse} may be treated.

For the case of discrete dualities, one can make the following observation. First note that the duality between complete and atomic Boolean algebras and sets is a restricted case of a more general \emph{adjunction} between atomic Boolean algebras and sets. Then recall that  the atomic Boolean algebras are precisely the completely representable Boolean algebras. (\emph{Any} meets that exist become intersections, \emph{any} joins become unions.) Hence the adjunction can be viewed in more semantic terms as linking those algebras that are completely representable as fields of sets with the category of sets.

With this observation in mind, we prepare the ground for a discrete duality for `compatibility algebras with operators' by identifying the completely representable algebras of our signature (\Cref{complete_axiomatisation}). It turns out that in this case, again all that is needed is to add the condition `atomic' to the conditions for representability. Such an outcome is not as automatic as it may seem, for there exist situations, for relations and for functions, where complete representability is characterised by more complex properties \cite{journals/jsyml/HirschH97a, complete}.

In the sequel to this paper, \emph{Difference--restriction algebras of partial functions with operators: discrete duality and completion} \cite{diff-rest2}, we carry out one of these planned continuations of the project. There, we present an adjunction (restricting to a duality) for the category of completely representable algebras and complete homomorphisms, then extend to an adjunction/duality for completely representable algebras equipped with compatibility preserving completely additive operators.

\subsubsection*{Structure of paper} In \Cref{preliminaries}, we define formally the class of representable algebras that we wish to axiomatise, list a finite number of valid equations for these algebras, and begin to deduce some consequences of these equations. In \Cref{sec:domains}, we deduce further consequences, relating specifically to the semantic notion of domain containment. In \Cref{sec:filters}, we deduce some properties of filters.

 In \Cref{sec:rep}, we use a representation based on prime filters to prove that our equations axiomatise both the algebras representable as partial functions (\Cref{axiomatisation}) and also the algebras representable as \emph{injective} partial functions (\Cref{cor:rep}).

  In \Cref{sec:complete}, we define formally the completely representable algebras and show that they are precisely the atomic representable algebras in both the partial function (\Cref{complete_axiomatisation}) and injective partial function (\Cref{complete_corollary}) cases.

\section{Basic definitions and properties}\label{preliminaries}

In this section, we start with the necessary definitions relating to algebras of partial functions, present the set of equations that will eventually become our first axiomatisation, and derive various consequences of these equations.

Given an algebra $\algebra{A}$, when we write $a \in \algebra{A}$ or say that $a$ is an element of $\algebra{A}$, we mean that $a$ is an element of the domain of $\algebra{A}$. Similarly for the notation $S \subseteq \algebra{A}$ or saying that $S$ is a subset of $\algebra{A}$. We follow the convention that algebras are always nonempty. If $S$ is a subset of the domain of a map $\theta$ then $\theta[S]$ denotes the set $\{\theta(s) \mid s \in S\}$.

We begin by making precise what is meant by partial functions and
algebras of partial functions.
\begin{definition}
  Let $X$ and $Y$ be sets. A \defn{partial function} from $X$ to $Y$
  is a subset $f$ of $X \times Y$ validating
\begin{equation*
  (x, y) \in f \text{ and } (x, z) \in f \implies y = z.
\end{equation*}
If $X = Y$ then $f$ is called simply a partial function on $X$.
Given a partial function $f$ from $X$ to $Y$, its \defn{domain} is
the set
\[\dom(f) \coloneqq \{x \in X \mid \exists \ y \in Y \colon (x, y) \in f\}.\]
\end{definition}

\begin{definition
An
  \defn{algebra of partial functions} of the signature $\{-, \rest\}$
  is a universal algebra $\algebra A = (A, -, \rest)$ where the
  elements of the universe $A$ are partial functions from some
  (common) set $X$ to some (common) set $Y$ and the interpretations of
  the symbols are given as follows:
\begin{itemize}

\item
The binary operation $-$ is \defn{relative complement}:
\[f - g \coloneqq \{(x, y) \in X \times Y \mid (x, y) \in f \text{ and
  } (x, y) \not\in g\}.\]

\item
The binary operation $\rest$ is \defn{domain restriction}.\begin{NoHyper}\footnote{This operation has historically been called \emph{restrictive multiplication}, where \emph{multiplication} is the historical term for \emph{composition}. But we do not wish to emphasise this operation as a form of composition.}\end{NoHyper} It is the restriction of the second argument to the domain of the first; that is:
\[ f \rest g \coloneqq \{(x, y) \in X \times Y \mid x \in \dom(f)
  \text{ and } (x, y) \in g\}\text{.}\]
\end{itemize}
\end{definition}
Note that in algebras of partial functions of the signature $\{-,
\rest\}$, the set-theoretic intersection of two elements $f$ and $g$ can be
expressed as $f - (f - g)$. We use the symbol~$\cdot$ for this derived
operation.

We also observe that, without loss of generality, we may assume
$X = Y$ (a common stipulation for algebras of partial functions). Indeed, if $\cA$ is a $\{-, \rest\}$-algebra of partial functions from $X$
to $Y$, then it is also a $\{-, \rest\}$-algebra of partial functions from $X \cup Y$ to $X \cup Y$. In this
case, this non-uniquely-determined single set is called `the' \defn{base}. However, certain properties
may not be preserved by changing the base. For instance, while a
partial function is injective as a function on~$X$ if and only if it
is injective as a function on~$X'$, this is not the case for
surjectivity.

\begin{definition}
  An algebra $\algebra A$ of the signature $\{ -, \rest\}$ is
  \defn{representable} (by partial functions) if it is isomorphic to an
  algebra of partial functions. An isomorphism from $\algebra A$ to an
  algebra of partial functions is a \defn{representation} of $\algebra
  A$.
\end{definition}

Just as for algebras of partial functions, for any $\{-, \rest\}$-algebra
$\cA$, we will consider the derived operation $\bmeet$ defined by
\begin{equation*}
  \label{complement}\tag{I}
  a \bmeet b := a - (a - b).
\end{equation*}

Algebras of partial functions of many other signatures have been investigated, and the corresponding representation classes axiomatised, often (but not always) finitely, and often (but not always) with equations. We will not enumerate all these results here, but for a treatment of some of the most expressive signatures to have been considered, see \cite{hirsch}. For a relatively comprehensive guide to this literature, see \cite[\S 3.2]{phdthesis}. Focusing on signatures that, like ours, do not contain composition, \cite{BERENDSEN2010141} gives a finite equational axiomatisation for the more expressive signature $\{-, \pref\}$, where $\pref$ is the operation known as \emph{preferential union} or alternatively as \emph{override}. In \cite{JACKSON2021106532}, a finite equational axiomatisation is given for the signature---incomparable with ours---of preferential union and \emph{update}.

In \Cref{sec:rep} we shall see (\Cref{axiomatisation}) that the
class of $\{-, \rest\}$-algebras that is representable by partial
functions is the variety axiomatised by the following set of
equations.
\begin{enumerate}[label = (Ax.\arabic*), leftmargin = *]
\item \label{schein1} $a - (b - a) = a$
\item \label{commutative}
$a \bmeet b = b \bmeet a$
\item \label{schein3} $(a - b) - c = (a - c) - b$
\item \label{eq:8} $(a \rest c)\bmeet(b \rest c) = (a \rest b) \rest
  c$
\item \label{lifting}$ (a \bmeet b) \rest a = a \bmeet b$
\end{enumerate}

Algebras of the signature $\{-\}$ validating axioms \ref{schein1} -- \ref{schein3} are called \defn{subtraction algebras} \cite{abbott1969sets}. It is known that these equations axiomatise the $\{-\}$-algebras representable as an algebra of sets equipped with relative complement (see, for example, \cite[Theorem~1 + Example~(2)]{schein1992difference}). Hence \ref{schein1} -- \ref{schein3} are sound for $\{ -,
  \rest\}$-algebras
  of partial functions and therefore for all representable $\{ -,
  \rest\}$-algebras. We also know immediately that any (isomorphism invariant) property of sets with~$-$ is a consequence of \ref{schein1} -- \ref{schein3}.
 One particular consequence that will be often used in the rest of the paper without further mention is that the derived operation $\bmeet$ provides the structure of a semilattice with bottom $0 \coloneqq a - a$ (independent of choice of $a$). Similarly, we will also use the fact that $0$ acts as a right identity for $-$ without further remark. Three further properties that we will find useful are the following.
 \begin{align}
 \label{disjoint_0} b \bmeet (a - b) &= 0\\
     \label{eq:9} a - (a\bmeet b) & = a-b\\
    \label{eq:10} a\bmeet (b-c) &= (a\bmeet b)-c
    \end{align}

In the remainder of this section, we start by verifying that  axioms \ref{eq:8} and \ref{lifting} are also sound for representable $\{ -,
  \rest\}$-algebras,
and we derive some algebraic consequences of \ref{schein1} -- \ref{lifting} that will be useful in
the sequel.
\begin{lemma}\label{axioms}
  Axioms~\ref{eq:8} and \ref{lifting} are sound for all $\{ -,
  \rest\}$-algebras
  of partial functions and therefore for all representable $\{ -,
  \rest\}$-algebras.
\end{lemma}
\begin{proof}

  For~\ref{eq:8}, we observe that $(x,y) \in (a \rest c) \bmeet (b
  \rest c)$ exactly when $x$ belongs both to the domain of $a$ and to
  that of $b$, and $(x, y) \in c$. But having $x \in \dom(b)$ amounts
  to having $(x,z) \in b$ for some $z$, and thus we may conclude that
  \[\dom(a) \cap \dom(b) = \dom(a \rest b).\]
  This leads to the desired equality.

  Finally, for~\ref{lifting}, suppose $(x, y) \in (a \bmeet b) \rest
  a$. Then $(x, y) \in a$ and $x$ is in the domain of~$a \bmeet b$. By
  the later fact, there is some $z$ with $(x, z)$ in both $a$ and
  $b$. But since $a$ is a function $z$ must equal $y$. Hence $(x, y)
  \in a \bmeet b$. Conversely, if $(x, y) \in a \bmeet b$, then
  clearly $x \in \dom(a \bmeet b)$ and $(x, y) \in a$, so that $(x, y)
  \in (a \bmeet b) \rest a$.
\end{proof}
We observe that axioms \ref{schein1} -- \ref{eq:8} are valid not
only for functions, but for arbitrary binary relations. However, the
validity of \ref{lifting} relies on $a$ being a function.

\begin{proposition}

  In an algebra of the signature $\{-, \rest\}$ validating axioms
  \ref{schein1} -- \ref{lifting}, the following hold.
  \begin{align}
    \label{restricts}b \rest a &\leq a\\
    \label{eq:12} a \rest (b \rest c) & = (a \rest b) \rest c \\
    \label{eq:4} (a \rest b) \rest (a \bmeet b) & = a \bmeet b\\
    \label{eq:14} a \rest (b \bmeet c)& = (a \rest b) \bmeet c \\
    \label{eq:13} (a \rest b) - c & = a \rest (b - c)\\
    \label{left}(a \leq b, \ c \leq d)\limplies a \rest c &\leq b \rest d

  \end{align}
\end{proposition}
\begin{proof

  First we observe that the following equality holds:
  \begin{equation}
    \label{eq:18}
    (a \rest  (b \rest c))\bmeet (b \rest  (b \rest c))\bmeet (c \rest
    (b \rest c)) = (a \rest c) \bmeet (b \rest c).
  \end{equation}
  Indeed, by successively using axiom \ref{eq:8}, we can rewrite the
  left-hand side as
  \[((a \rest b) \rest (b \rest c))\bmeet (c \rest (b \rest c)) = ((a
    \rest b)\rest c) \rest (b \rest c) = ((a \rest c)\bmeet (b \rest
    c)) \rest (b \rest c),\]
  and by~\ref{lifting}, this is precisely $(a \rest c) \bmeet (b \rest
  c)$. We will also use that $\rest$ is idempotent, which is a
  consequence of \ref{lifting} and idempotency of the $\bmeet$ operation.
  \begin{description}
  \item[\eqref{restricts}:] This inequality translates into the
    equality $a \bmeet (b \rest a) = b \rest a$. Taking $a = c$
    in~\eqref{eq:18}, we have:
    \begin{align*}
      a \bmeet (b \rest a)
      & = (a\rest a) \bmeet (b \rest a) = (a \rest  (b \rest a))\bmeet
        (b \rest  (b \rest a))\bmeet (a \rest(b \rest a))
      \\ & = (b \rest  (b \rest a))\bmeet (a \rest(b \rest a)) \just
           {\ref{eq:8}} = (b \rest a) \rest (b \rest a) = (b \rest
           a).
    \end{align*}
  \item[\eqref{eq:12}:] By axiom~\ref{eq:8}, $(a \rest b) \rest c$
    equals the left-hand side of~\eqref{eq:18}. We prove that so does
    $a \rest (b \rest c)$:
    \[(a \rest (b \rest c)) \bmeet (b \rest (b \rest c)) \bmeet (c
      \rest (b \rest c)) \just {\ref{eq:8}} = (a \rest (b \rest c))
      \bmeet ((b \rest c) \rest (b \rest c)) \just{\eqref{restricts}}=
      a \rest (b \rest c).\]
  \item[\eqref{eq:4}:] We first observe that $b \rest (a \rest b) = a
    \rest b$. Indeed, we may compute:
    \begin{align}\label{eq:2.11}
      b \rest (a \rest b)
      & \just{\eqref{eq:12}} = (b \rest a)\rest b \just{\ref{eq:8}}
        = (b\rest b)\bmeet (a \rest b) \just {\eqref{restricts}}=
        a\rest b.
    \end{align}
    Then we can compute:
    \begin{align*}
    (a \rest b) \rest
    (a \bmeet b) &\just{\ref{eq:8}}=(a \rest (a \bmeet b))\bmeet(b \rest (a \bmeet b)) \\&\just{\ref{lifting}}= (a \rest ((a \bmeet b) \rest a)) \bmeet (b \rest ((a \bmeet b) \rest b)) \\&\just{\eqref{eq:2.11}}= ((a\bmeet b) \rest a) \bmeet ((a\bmeet b) \rest
    b)
   \\ &\just{\ref{lifting}}=a \bmeet b.
    \end{align*}
  \item[\eqref{eq:14}:] This follows from:
    \begin{align*}
      a \rest (b \bmeet c)
      & \just{\ref{lifting}} = a \rest ((b \bmeet c) \rest b)
        \just {\eqref{eq:12}} = (a \rest (b\bmeet c)) \rest b
      \\ & \just {\ref{eq:8}} = (a \rest b) \bmeet ((b \bmeet c) \rest b)
           \just {\ref{lifting}} = (a \rest b) \bmeet (b \bmeet c) \just
           {\eqref{restricts}} = (a \rest b) \bmeet c.
    \end{align*}
  \item[\eqref{eq:13}:] We have

 \begin{align*}
 (a \rest b) - c &\just{\hspace{2pt}\eqref{restricts}\hspace{2pt}} = (b \bmeet (a \rest b)) - c
\just{\eqref{complement}} = (b - (b - (a \rest b))) - c\\
&\just{\ref{schein3}} = (b - c) - (b - (a \rest b))
 = (b - c) - ((b - c) - (a \rest b))\\
&\just{\hspace{5.7pt}\eqref{complement}\hspace{5.7pt}} = (a \rest b) \bmeet (b - c)\just {\eqref{eq:14}} = a \rest (b \bmeet (b - c)) = a \rest (b - c),
 \end{align*}
 where the unmarked equalities follow from evident properties of sets with relative complement.
  \item[\eqref{left}:] Let $a\leq b$ and $c \leq d$. The desired
    inequality is a consequence of combining the inequalities $a\rest
    c \leq b \rest c$ and $b \rest c \leq b \rest d$. While the former
    is a trivial consequence of~\ref{eq:8} and the fact that $a\rest
    b = a$ implied by~\ref{lifting}, the latter may be derived as
    follows:
    \begin{align*}
      (b \rest c)\bmeet (b \rest d)
      & \just{\ref{lifting}} = (b \rest (c\rest d))\bmeet (b \rest
        d) \just{\eqref{eq:12}} = ((b \rest c)\rest d)\bmeet (b \rest
        d)
      \\ & \just{\ref{eq:8}} = (b \rest(b \rest
           c))\rest d \just{\ref{lifting}, \eqref{eq:12}} = b
           \rest (c\rest d) \just{\ref{lifting}} = b \rest c.\qedhere
    \end{align*}

  \end{description}
\end{proof}

Since, by property~\eqref{eq:12}, the operation $\rest$ is
associative, from hereon we may write $a \rest b \rest c$ instead of
$(a \rest b) \rest c$ or $a \rest (b \rest c)$.

For any poset $\cS$ and $a \in \cS$, the notation $a^\downarrow$
denotes the set $\{b \in \cS \mid b \leq a\}$. It is known that in any subtraction algebra $\cS$, for any $a \in \cS$, the set $a^\downarrow$, with least element
  $0$, greatest element $a$, meet given by $\bmeet$ and
  complementation given by $\compl{b} \coloneqq a - b$ is a Boolean
  algebra \cite{schein1992difference}. We note the following corollary.

\begin{corollary}\label{c:3}
  If $h: \cS \to \cT$ is a homomorphism of subtraction algebras then, for every $a \in \cS$,
  the map $h$ induces a homomorphism of Boolean algebras $h_a:
  a^\downarrow \to h(a)^\downarrow$.
\end{corollary}

  We can also prove a sort of converse to each $a^\downarrow$ of a subtraction algebra being a Boolean algebra.

\begin{proposition}\label{p:1}
Suppose that $(\cS, \cdot)$ is a meet-semilattice with
  bottom~$0$, such that for every $a \in \cS$, $(a^{\downarrow},
  \cdot, 0, a, \overline{(\_)}^a)$ is a Boolean algebra. Then setting
  $a-b := \overline{(a \cdot b)}^a$ defines a
  subtraction algebra structure on $\cS$ (on which \eqref{complement} becomes a valid equation).
\end{proposition}
\begin{proof}
First we argue that  $\bmeet$ is the operation obtained from the term $a - (a - b)$. Now $(a -b)$ is by definition in $a^\downarrow$, so $a - (a -b) = \overline{(a \cdot (a-b))}^a = \overline{(a-b)}^a$, which is the complement of the complement of $a \bmeet b$ in $a^\downarrow$, that is, equals $a \bmeet b$. As a consequence, the validity of \ref{commutative}, which is formally a statement about $-$, is immediate.

For the validity of \ref{schein1}, the term $a - (b - a)$ is by definition $\overline{a \bmeet\overline{(b\bmeet a)}^b}^a$. We calculate $a \bmeet\overline{(b\bmeet a)}^b$. Now $\overline{(b\bmeet a)}^b$ is by definition less than or equal to $b$, so $a \bmeet\overline{(b\bmeet a)}^b = a \bmeet b\bmeet\overline{(b\bmeet a)}^b$. But $\overline{(b\bmeet a)}^b$ is the complement of $a \bmeet b$ in $b^\downarrow$, so $a \bmeet b\bmeet \overline{(b\bmeet a)}^b = 0$. Hence $a - (b - a) = \overline{0}^a = a$.

For the validity of \ref{schein3}, we start from the term $(a-b) - c$. We may assume $b$ and $c$ are in $a^\downarrow$ since $a-b = \overline{a \bmeet b}^a = \overline{a \bmeet a \bmeet b}^a = a - (a \bmeet b)$ and $(a-b) - c = \overline{(a-b) \bmeet c}^a = \overline{(a-b) \bmeet a \bmeet c}^a = (a-b) - (a \bmeet c)$. We write simply $\overline{\phantom c}$ for the complement in $a^\downarrow$, and $+$ for the join. Then $(a - b) - c = \overline b - c = \overline{\overline b \bmeet c}^{\overline b}$. In any Boolean algebra, the complement operation on the induced Boolean algebra $d^\downarrow$ is given by $e \mapsto  d \bmeet \overline e$. So as $\overline b$ is an element of the Boolean algebra $a^\downarrow$, the complement on $\overline{b}^\downarrow$ is given by $d \mapsto \overline b \bmeet \overline d$. Hence $\overline{\overline b \bmeet c}^{\overline b} = \overline b \bmeet (b + \overline c) = \overline b \bmeet \overline c$. It is now clear, by commutativity of $\bmeet$ and symmetry, that this is equal to $(a-c) - b$.
\end{proof}

\section{The algebra of domains}\label{sec:domains}

Throughout this section, let $\algebra A$ be an
algebra of the signature $\{ -, \rest\}$ validating axioms
\ref{schein1} -- \ref{lifting}. Although we do not have the \emph{domain operation} in our
signature, the signature is expressive enough
that it can express the `domain containment' relation. In this section, we will begin to investigate this implicit domain information. Later we will
see that the domain containment relation can be extended to the set of filters
of~$\cA$ (\Cref{l:6}).

\begin{definition}
  Define the relation $\preceq_\cA$ on $\algebra A$ by $a \preceq_\cA
  b \iff a \leq b \rest a$.
\end{definition}
We often drop the subscript $\algebra A$. Notice that, by~\eqref{restricts}, we have $a \preceq b$ if and
only if $a = b \rest a$.  When $\cA$ is an algebra of partial
functions it is not hard to see that, for every $f, g \in \cA$, we
have $f \preceq g$ exactly when $\dom(f) \subseteq \dom(g)$.

\begin{lemma}\label{l:3}
  The following statements hold:
  \begin{enumerate}[label = (\alph*)]
  \item\label{item:5} $\preceq$ is a preorder on $\cA$ that contains
    $\leq$;
  \item\label{item:7} for every $a \in \cA$, if $a \preceq 0$, then $a = 0$.
  \end{enumerate}

\end{lemma}
\begin{proof}
  The fact that $\preceq$ is reflexive, that is, that $a = a \rest a$
  for every~$a \in \cA$, follows from axiom \ref{lifting}. To prove
  that $\preceq$ is transitive, let $a,b, c \in \cA$ be such that $a
  \preceq b$ and $b \preceq c$. Then we have
  \begin{align*}
    c \rest a \just{a \preceq b} = c \rest b \rest a \just{b \preceq
    c} = b \rest a \just {a \preceq b} = a,
  \end{align*}
  and thus $a \preceq c$.
  %
  To see that $\preceq$ contains $\leq$ let $a, b \in \cA$ be such
  that $a \leq b$. Since, by~\eqref{left}, the operation $\rest$ is
  order preserving, we have $a = a \rest a \leq b \rest a$, and hence $a
  \preceq b$. This proves~\ref{item:5}. For~\ref{item:7}, we observe
  that $a \preceq 0$ means $a \leq 0\rest a$. But,
  by~\ref{lifting}, we have $0 \rest a = 0$, and thus $a = 0$.
\end{proof}

Observe that every homomorphism of $\{-, \rest\}$-algebras is
$\preceq$-preserving, since $\preceq$ is defined by an equation.

We denote by $\sim_\cA$ the equivalence relation induced by
$\preceq_\cA$, and for a given $a \in \cA$ we use $[a]$ to denote the
equivalence class of~$a$. The canonical projection $\cA
\twoheadrightarrow \cA/{\sim_\cA}$ is denoted by~$\pi_\cA$. As with $\preceq$, if $\cA$
is clear from context, we denote $\sim_\cA$ and
$\pi_\cA$ by $\sim$ and $\pi$, respectively.  Given a
subset $S \subseteq \cA$, we may use $S/{\sim}$ to denote the forward
image $\pi[S]$ of~$S$ under~$\pi$.

\begin{lemma}\label{l:2}
  The poset $\algebra A / {\sim}$ of $\sim$-equivalence classes is a
  meet-semilattice with
  \begin{equation}
    [a] \wedge [b] = [a \rest b].\label{eq:2}
  \end{equation}
  In particular, we have $a^\downarrow/{\sim} = [a]^{\downarrow}$.
\end{lemma}
\begin{proof}
  The fact that $[a \rest b]$ is a lower bound of $[a]$ is a
  consequence of having $a \rest a = a$ by~\ref{lifting}. In turn, $[a
  \rest b]$ is a lower bound of $[b]$ thanks to~\eqref{restricts} and
  the fact that $\leq$ is contained in $\preceq$, by \Cref{l:3}.
  Suppose that $[c] \preceq [a], [b]$, that is, $c = a \rest c = b
  \rest c$. Then we may compute
  \[a \rest b \rest c = a \rest c = c,\]
  hence $[c] \preceq [a \rest b]$ and we have~\eqref{eq:2}.

  For the second assertion, by \Cref{l:3} it is clear that
  $a^\downarrow/{\sim} \subseteq [a]^{\downarrow}$. Conversely, let
  $[b] \preceq [a]$. By~\eqref{eq:2}, we have $[b \rest a] = [a]
  \wedge [b] = [b]$, and by~\eqref{restricts} we have $b \rest a \leq
  a$. Thus $[b] \in a^\downarrow/{\sim}$.
\end{proof}

\begin{lemma}\label{l:5}
  The relations $\leq$ and $\preceq$ coincide on each downset
  $a^{\downarrow}$, for $a \in \cA$. In particular, $[a]^\downarrow$
  is a Boolean algebra isomorphic to $a^{\downarrow}$.  Explicitly,
  for every $[b] \preceq [a]$, the element $b \rest a$ is the unique element of
  $a^\downarrow$ that is $\sim$-equivalent to~$b$.
\end{lemma}
\begin{proof}
  By \Cref{l:3}, we already know that $\preceq$ contains
  $\leq$. Conversely, let $x, y \in a^\downarrow$ be such that $x
  \preceq y$, that is, $y \rest x = x$. Using~\ref{lifting},
  we have $x = x \rest a$ and $y = y \rest a$. Therefore, $x\bmeet y =
  (y \rest a)\bmeet (x \rest a)$, and by~\ref{eq:8} it follows that
  $x \bmeet y = (y \rest x) \rest a$. Using the hypothesis that $x
  \preceq y$ and $x \rest a = x$, we may conclude that $x \leq y$ as
  intended.

   Thus $a^\downarrow$ is order isomorphic to $a^\downarrow / {\sim}$, which by the second part of \Cref{l:2} equals $[a]^\downarrow$. For the last assertion, we saw in the proof of \Cref{l:2} that $b \rest a$ is in $a^\downarrow$ and $\sim$-equivalent to $b$, thus we now know it is the unique such element of $a^\downarrow$.
\end{proof}
\begin{corollary} \label{c:2}
If $a \leq b$ and $b \preceq a$, then $a = b$. Hence, $a
  < b$ implies $a \prec b$, where $\prec$ denotes the strict relation
  derived from $\preceq$ (that is, $a \prec b$ if and only if $a \preceq
  b$ and $a \not\sim b$).
\end{corollary}
\begin{proof}
  Pick two elements $a, b$ validating $a \leq b$ and $b \preceq a$. By
  \Cref{l:3}, we know $a$ and $b$ are $\sim$-equivalent, and moreover they are
  both in the downset~$b^\downarrow$. Thus, by \Cref{l:5}, they must be equal.
\end{proof}
\begin{corollary}\label{c:1}
  The poset $\cA/{\sim}$ admits a subtraction algebra structure, where the
  operation $-$ is given by
  \[[a]-[b] = [a- (b \rest a)].\]
\end{corollary}
\begin{proof}
  By \Cref{l:5} we know that, for every $a \in \cA$, the set $[a]^\downarrow$
  is a Boolean algebra isomorphic to $a^\downarrow$ via the assignment
  $[b] \mapsto b \rest a$. So by \Cref{p:1}, $\cA/{\sim}$ is a subtraction algebra with $[a] - [b]$ equal to  the complement of $[a]\wedge[b] = [b \rest a]$ in
  $[a]^\downarrow$. This is indeed $[a-(b \rest a)]$, as $b \rest a \in a^\downarrow$ by~\eqref{restricts}.
\end{proof}

\section{Filters}\label{sec:filters}

We continue to let $\cA$ denote an algebra of the signature $\{-, \rest\}$
validating axioms~\ref{schein1} -- \ref{lifting}. Since $\cA$ admits
a semilattice structure, the notion of a \emph{filter of $\cA$} is
well defined.

\begin{definition}
  A subset $F$ of a meet-semilattice $\cS$ is a \defn{filter} if
  \begin{enumerate}[(i)]
  \item $F$ is nonempty,
  \item $F$ is upward closed,
  \item $a, b \in F \implies a \wedge b \in F$.
  \end{enumerate}
  We use $\filt \cS$ to denote the set of all filters of $\cS$. Notice
  that $\filt \cS$ is a poset ordered by inclusion, with top element
  $\cS$, the full filter.
\end{definition}

We now concentrate on $\filt \cA$. First observe that
there is a natural order-reversing embedding of posets
\[\iota: (\cA, \leq) \hookrightarrow (\filt\cA,
  \subseteq),\qquad a \mapsto a^\uparrow.\]
The preorder $\preceq$ may be extended to $\filt{\cA}$ as follows:
given $F, G \in \filt\cA$ we set
\[F \ppreceq G \iff G \rest F \subseteq F,\]
where for any subsets $S, T \subseteq \cA$, the notation $S \rest T$ denotes the set $\{s
\rest t \mid s \in S, \ t \in T\}$. Then $a \preceq b \iff a^\uparrow \ppreceq b^\uparrow$ for all $a, b \in \cA$, as we now check. Indeed, given  $a \preceq b$
   and using~\eqref{left}, we have $b^\uparrow \rest
  a^\uparrow \subseteq (b \rest a)^\uparrow = a^\uparrow$, and hence,
  $a^\uparrow \ppreceq b^\uparrow$. Conversely, if $a^\uparrow \ppreceq b^\uparrow$, that is $b^\uparrow \rest a^\uparrow \subseteq a^\uparrow$, then in particular $b \rest a \in a^\uparrow$. That is to say, $b \rest a \geq a$, which is the definition of $a \preceq b$.
\begin{lemma}\label{l:6}
  The following statements hold:
  \begin{enumerate}[label = (\alph*)]
  \item\label{item:8} $\ppreceq$ is a preorder on $\filt\cA$ that
    contains $\supseteq$;
  \item\label{item:9} for every $F \in \filt\cA$, if $F \ppreceq \cA$, then $F = \cA$;
  \end{enumerate}
\end{lemma}
\begin{proof}
  For \ref{item:8}, let $F, G, H \in \filt\cA$. Given $a,b \in F$, since $F$ is a
  filter, we have $a \bmeet b \in F$. On the other hand,
  by~\eqref{left}, we have $a \rest b \geq (a\bmeet b) \rest (a \bmeet b) =
  a\bmeet b$. Thus $F$ is closed under~$\rest$, and so $\ppreceq$ is
  reflexive. Now suppose that $F \ppreceq G$ and $G \ppreceq
  H$. Since $G$ is nonempty, by~\eqref{restricts} we have $H \rest F
  \subseteq H \rest (G \rest F)^\uparrow$. But, by~\eqref{left}, this $H \rest (G \rest F)^\uparrow$
  is contained in $(H \rest G \rest F)^\uparrow$, and using that $F
  \ppreceq G$ and $G \ppreceq H$ we may conclude that $(H \rest G \rest F)^\uparrow$ is in turn
  contained in~$F$. Therefore $\ppreceq$ is transitive, and
  $\ppreceq$ is a preorder. The fact that $\ppreceq$ contains
  $\supseteq$ is a trivial consequence of its reflexivity.

  For proving~\ref{item:9}, it suffices to observe that $\cA \subseteq
  (\cA \rest F)^\uparrow$. In fact, it is the case that $G \subseteq
  (G \rest F)^\uparrow$ whenever $G$ is a filter extending
  $F$. Indeed if $a \in G$ and $b \in F$ (nonemptiness of~$F$ yields
  the existence of such an element), then $(a\bmeet b) \rest b$
  belongs to $G \rest F$. By~\ref{lifting}, we have $(a\bmeet b) \rest
  b = a \bmeet b$, and thus, $a \in (G \rest F)^\uparrow$.
\end{proof}

We denote by $\approx$ the equivalence relation induced by $\ppreceq$,
and by
\[\rho: \filt\cA \to \filt\cA/{\approx}\]
the canonical projection. The $\approx$-equivalence class of a filter
$F \in \filt \cA$ is denoted~$\dbracket F$, and for a subset $S
\subseteq \cA$ we may use $S/{\approx}$ to denote $\rho[S]$.

\begin{lemma}\label{l:7}
  For every $F, G \in \filt \cA$, the subset $(G \rest F)^\uparrow
  \subseteq \cA$ is a filter. Moreover, the poset $\filt\cA/{\approx}$
  is a meet-semilattice with
    \begin{equation}
      \dbracket F \wedge \dbracket G = \dbracket{(G \rest
        F)^\uparrow}.\label{eq:16}
  \end{equation}
  In particular, we have $F^\Uparrow/{\approx} = \dbracket
  F^\downarrow$, where $F^\Uparrow$ is the upset of $F$ with respect to filter
  inclusion.
\end{lemma}
\begin{proof}
  First we show that $(G \rest F)^\uparrow$ is a filter.
\begin{enumerate}[(i)]
\item As $F$ and $G$ are nonempty, $G \rest F$, and therefore $(G
  \rest F)^\uparrow$ is nonempty.
\item The set $(G \rest F)^\uparrow$ is upward closed by definition.
\item Suppose $x, y \in (G \rest F)^\uparrow$. So there are $a, b \in
  G$ and $c,d \in F$ with $x \geq a \rest c$ and $y \geq b \rest
  d$. As $F$ and $G$ are filters, we know $a \bmeet b \in G$ and $c
  \bmeet d \in F$. By \eqref{left}, we find that $(a \bmeet b) \rest
  (c \bmeet d) \leq (a \rest c) \bmeet (b \rest d)$. It follows that
  the element $(a \bmeet b) \rest (c \bmeet d)$ of $G \rest F$ is
  smaller than or equal to $x \bmeet y$. Hence $x \bmeet y \in (G
  \rest F)^\uparrow$.
\end{enumerate}
Now for proving that $(G \rest F)^\uparrow$ is a lower bound of $F$
and of $G$ it suffices to prove, respectively, that $F \rest G \rest
F$ and $G \rest G \rest F$ are contained in $(G \rest
F)^\uparrow$. Using~\ref{eq:8}, we know that $F \rest G \rest F = G
\rest F \rest F$. Thus, reflexivity of $\ppreceq$ yields both
inclusions. To see that $(G \rest F)^\uparrow$ is the greatest
lower bound of $F$ and $G$, we let $H \subseteq \cA$ be another filter
containing both $F \rest H$ and $G \rest H$ (that is, $H \ppreceq F,
G$). Then
\[G \rest F \rest H \subseteq G \rest H \subseteq H,\]
and thus by \eqref{left}, we have $(G \rest F)^\uparrow \rest H \subseteq H^\uparrow = H$. That is, $H \ppreceq (G \rest F)^\uparrow$, thereby
proving~\eqref{eq:16}.

Finally, by \Cref{l:6}, we have $F^\Uparrow/{\approx} \subseteq
\dbracket F ^\downarrow$. Conversely, let $\dbracket G \ppreceq
\dbracket F$. By~\eqref{eq:16}, we have $\dbracket{(G \rest
  F)^\uparrow} = \dbracket F \wedge \dbracket G =\dbracket G$, and
since $G$ is nonempty, by~\eqref{restricts}, $(G \rest F)^\uparrow
\supseteq F$. Thus, $\dbracket G \in F^\Uparrow/{\approx}$.
\end{proof}

The fact that $\ppreceq$ can be viewed naturally as an extension of $\preceq$ already suggests that
$\preceq$ and $\ppreceq$ are tightly related, and \Cref{l:7} shows
that $\ppreceq$ induces on $\filt \cA/{\approx}$ a semilattice
structure generalising the semilattice structure induced on $\cA/{\sim}$ by
$\preceq$. Next we see that $\ppreceq$ actually admits a description
in terms of the projection~$\pi$.
\begin{proposition}\label{p:3}
  For every filter $F \subseteq \cA$, the subset $\pi[F]^{\uparrow}
  \subseteq \cA/{\sim}$ is a filter of $\cA/{\sim}$, and conversely, every filter
  of $\cA/{\sim}$ is of this form. Moreover, for every $F, G \in
  \filt\cA$, we have
  \begin{equation}
    \label{eq:15}
    F \ppreceq G \iff \pi[G]^\uparrow \subseteq \pi[F]^\uparrow.
  \end{equation}
  In particular, the quotients
  \[\rho: \filt\cA \twoheadrightarrow \filt\cA/{\approx}\qquad \text{
      and }\qquad \pi[\_]^\uparrow: \filt\cA \twoheadrightarrow
    \filt{\cA/{\sim}}\] are isomorphic.
\end{proposition}
\begin{proof}
  First we show that $\pi[F]^\uparrow = (F / {\sim})^\uparrow$ is a
  filter.
  \begin{enumerate}[(i)]
  \item As $F$ is nonempty, $F / {\sim}$, and therefore $(F /
    {\sim})^\uparrow$, is nonempty.
\item The set $(F / {\sim})^\uparrow$ is upward closed by definition.

\item Suppose $[a], [b] \in (F /{\sim})^\uparrow$, say $[a_0] \preceq
  [a]$ and $[b_0] \preceq [a]$ for $a_0, b_0 \in F$. Then as~$F$ is a
  filter, we have $a_0 \bmeet b_0 \in F$. Using~\eqref{eq:4} and
  \Cref{l:2}, we have
  \[[a_0 \bmeet b_0] \preceq [a_0 \rest b_0] = [a_0] \wedge [b_0],\]
  and thus $[a_0] \wedge [b_0]$ belongs to $(F/{\sim})^{\uparrow}$,
  yielding that so does $[a] \wedge [b]$, as desired.
\end{enumerate}
Conversely, let $G \subseteq \cA/{\sim}$ be a filter. Define the relation $\equiv$ on $\pi^{-1}(G)$ by $a \equiv b \iff \exists d \in \pi^{-1}(G) : d \rest a = d \rest b$. Then $\equiv$ is clearly reflexive and symmetric. It is also transitive, because given $d_1, d_2 \in \pi^{-1}(G)$ such that $d_1 \rest a = d_1 \rest b$ and $d_2 \rest b = d_2 \rest c$, we have $d_1 \rest d_2 \in \pi^{-1}(G)$ and $d_1 \rest d_2 \rest a = d_1 \rest d_2 \rest c$ (proven using the law $d_1 \rest d_2 \rest x = d_2 \rest d_1 \rest x$, which is an evident consequence of \ref{eq:8}). Take any equivalence class $E$ of $(\pi^{-1}(G), \equiv)$---as $\pi^{-1}(G)$ is nonempty, there exists at least one choice. We claim that $E$ is a filter. It is nonempty by definition and upward closed because $\pi^{-1}(G)$ is upward closed (as $\pi$ is order preserving), and $a \leq b \in \pi^{-1}(G)$ implies $a \rest a = a = a \rest b$. If $a, b \in E$, then taking $d \in \pi^{-1}(G)$ such that $d \rest a = d \rest b$, we know $\pi(d \rest a) \in G$, so $d \rest a \in \pi^{-1}(G)$. Then as $d \rest (d \rest a) = d \rest a$ and $a \in E$, we have $d \rest a \in E$. Then since $d \rest a = d \rest b \leq a, b$,  the upward-closed set $E$ is closed under meets. Hence $E$ is a filter. Then, given $[d] \in G$, if we choose some $a \in E$ we have $d \rest a \in E$ and $\pi(d \rest a) \preceq [d]$, so $[d] \in \pi[E]^\uparrow$. Hence
$\pi[E]^\uparrow = G$.

Finally, we prove~\eqref{eq:15}. First assume that $F \ppreceq G$. Take an arbitrary $a \in G$. As $F$ is nonempty, we can choose some $b \in F$. As $F \ppreceq G$, we have $a \rest b \in G \rest F \subseteq F$. So $[a \rest b] \in \pi[F]$. Since $[a \rest b] \preceq [a]$, we obtain $[a] \in \pi[F]^\uparrow$. As $a \in G$ was arbitrary, we deduce $\pi[G] \subseteq \pi[F]^\uparrow$. Thus $\pi[G]^\uparrow \subseteq \pi[F]^\uparrow$.

 Conversely, suppose we
have $\pi[G]^\uparrow \subseteq \pi[F]^\uparrow$, and pick any $a \in
G$ and $b\in F$, so that $a \rest b \in G \rest F$. Since $[a]$ and
$[b]$ both belong to $\pi[F]^\uparrow$, so does $[a] \wedge [b] = [a
\rest b]$. Hence there exists $c \in F$ such that $c \preceq a
\rest b$.
 In turn, by reflexivity of ${\ppreceq}$, the element $c \rest b$ also
belongs to $F$, and furthermore we have $c \rest b \preceq c\preceq a \rest b$. Thus
$c \rest b \preceq a \rest b$ in $b^\downarrow$, and by \Cref{l:5}
this implies $c \rest b \leq a \rest b$, which yields $a \rest b \in
F$ as required.
\end{proof}

\begin{lemma}\label{l:8}
  The relations $\supseteq$ and $\ppreceq$ coincide on each upset
  $H^\Uparrow \subseteq \filt\cA$
\end{lemma}
\begin{proof}
  Let  $F, G \in H^\Uparrow$ and chose some $a \in H$, so $a \in F \cap  G$.
We already know that $\ppreceq$ contains
  $\supseteq$ (\Cref{l:6}). Conversely, suppose that $F \ppreceq G$ and let $b \in
  G$. We argue that $b$ also belongs to $F$, thereby showing the
  inclusion $F \supseteq G$. Since $G$ is a filter, $a\bmeet b \in G$,
  and thus $[a \bmeet b] \in \pi[G] \subseteq \pi[F]^\uparrow$
  (see \Cref{p:3}). Therefore there exists $c \in F$ such that $c
  \preceq a \bmeet b$. By~\eqref{eq:14}, this implies $a \bmeet c
  \preceq a \bmeet b$. Since this inequality lives in $a^\downarrow$, it follows,
  by \Cref{l:5},  that $a \bmeet c \leq a\bmeet b$. Finally,
  since $a, c \in F$, and $F$ is a filter, we may conclude that $b \in
  F$.

\end{proof}
\section{Representability}\label{sec:rep}

In this section, we finally show that equations \ref{schein1} -- \ref{lifting} axiomatise the representable $\{-, \rest\}$-algebras, by describing a generic representation, by partial functions, of any such algebra.

Throughout this section, we let $\algebra S$ be an arbitrary subtraction algebra.
Recall that a filter $F \subseteq \cS$ is \defn{maximal} if it is
proper (not the whole of $\cS$) and is maximal amongst all proper
filters of $\cS$, with respect to inclusion. We use $\mf \cS$ to denote
the set of all maximal filters of~$\cS$.

We noted in \Cref{preliminaries} that for every $a \in \cS$ we have a Boolean
algebra $a^\downarrow$. This allows us to relate maximal filters of $\cS$
with those of $a^\downarrow$.

\begin{proposition}\label{l:4}
  For every $a \in \cS$, there is a bijection between
  ultrafilters of the Boolean algebra $a^{\downarrow}$ and maximal
  filters of $\cS$ containing $a$.

 More precisely, if $\mu \subseteq \cS$ is a maximal filter containing $a$, then
  $\mu \cap a^\downarrow \subseteq a^\downarrow$ is an ultrafilter, if
  $\nu \subseteq a^\downarrow$ is an ultrafilter, then $\nu^\uparrow
  \subseteq \cS$ (with the upward closure taken in $\cS$) is a
  maximal filter, and these constructions are mutually inverse.
\end{proposition}
\begin{proof}
  Suppose $\mu \subseteq \cS$ is a maximal filter, and let $a \in
  \mu$. It is easy to verify that $\mu \cap a^\downarrow$ is a proper
  filter of $a^\downarrow$.  It is also easy to verify that any filter
  $F$ of $a^\downarrow$ yields a filter $F^\uparrow$ of $\cS$ and that $(\mu \cap
  a^\downarrow)^\uparrow \subseteq \mu$. Hence
  any filter $F$ of $a^\downarrow$ properly extending $\mu \cap
  a^\downarrow$ satisfies $\mu \subsetneq F^\uparrow = \cS$, and hence $F =
  a^\downarrow$ (since $F$ is upward closed). That is, $\mu \cap
  a^\downarrow$ is an ultrafilter of~$a^\downarrow$.

  Conversely, let $\nu \subseteq a^{\downarrow}$ be an ultrafilter. It
  is straightforward to check that $\nu^\uparrow$ is a proper filter
  of~$\cS$, so we only need to show it is maximal. Let $F \subseteq
  \cS$ be a filter properly containing $\nu^\uparrow$ and let $b$
  belong to $F - \nu^\uparrow$.  We know both $a \bmeet b$ and $a - b$
  are in $a^\downarrow$ and are complements in this Boolean
  algebra. Hence either $a \bmeet b$ or $a - b$ is in the ultrafilter
  $\nu$, and hence in $\nu^\uparrow$. But $\nu^\uparrow$ is an upset
  that does not contain $b$, so it cannot contain $a\bmeet b$, and
  thus we have $a-b \in \nu^\uparrow \subseteq
  F$. Using~\eqref{disjoint_0}, this yields $b \bmeet (a-b) = 0 \in
  F$, so $F = \algebra A$. Hence $\nu^\uparrow$ is a maximal filter.

  Finally, we check that the two constructions are inverse to each
  other. If $\mu \subseteq \cS$ is a maximal filter and $a \in \mu$,
  then we have an inclusion of maximal filters $(\mu \cap
  a^\downarrow)^\uparrow \subseteq \mu$ and thus an equality. On the
  other hand, if $\nu \subseteq a^\downarrow$ is an ultrafilter, it is
  clear that $\nu = \nu^\uparrow \cap a^\downarrow$---this is
  the case for any upward-closed subset $\nu$ of $a^\downarrow$.
\end{proof}

\begin{corollary}\label{max_condition}
  Let $F \subseteq \cS$ be a filter. Then the following are
  equivalent.
  \begin{enumerate}[label = (\alph*)]
  \item\label{equivalent_one} $F$ is maximal.
  \item\label{equivalent_two} For all $a \in F$ and $b \in \algebra
    S$, precisely one of $a \bmeet b$ and $a - b$ belongs to $F$.
  \item\label{equivalent_three} For some $a \in F$, for all $b \in
    \algebra S$, precisely one of $a \bmeet b$ and $a - b$ belongs to
    $F$.
  \end{enumerate}
\end{corollary}
\begin{proof}
  Since $F$ is nonempty, it is clear that \ref{equivalent_two} implies
  \ref{equivalent_three}, while \ref{equivalent_one} implying
  \ref{equivalent_two} is an immediate consequence
  of~\Cref{l:4}. Suppose $a \in F$ witnesses the truth of
  \ref{equivalent_three}. Then by this hypothesis, $\nu \coloneqq F \cap
  a^\downarrow$ is an ultrafilter of $a^\downarrow$. Therefore, by
  \Cref{l:4}, $\nu^\uparrow$ is a maximal filter of $\cS$, and clearly $\nu^\uparrow \subseteq F$. Since $F$ is proper (because so is $\nu$), we conclude that $F
  = \nu^\uparrow$, and hence $F$ is maximal.
\end{proof}

\begin{corollary}\label{extension}
  Let $F \subseteq \cS$ be a proper filter. Then there exists a
  maximal filter $\mu$ with $F \subseteq \mu$.
\end{corollary}
\begin{proof}
  Take an element $a \in F$. It is straightforward to check that $F
  \cap a^\downarrow$ is a filter of the Boolean algebra
  $a^\downarrow$. Let $\nu$ be an ultrafilter of $a^\downarrow$ that
  extends $F \cap a^\downarrow$. Then, by \Cref{l:4}, the set $\nu^\uparrow$
  is the required $\mu$.
\end{proof}

In the results below, $\cA$ is an arbitrary $\{-,\rest\}$-algebra $\cA$ validating
axioms \ref{schein1} -- \ref{lifting}. So in particular, by \Cref{c:1}, we can view $\cA/{\sim}$ as a subtraction algebra, to which the previous results apply.

\begin{lemma}\label{filter_down}
  Let $\mu$ be a maximal filter of $\algebra A$.  Then the filter $(\mu /
  {\sim})^\uparrow$ is a maximal filter of $\algebra A / {\sim}$.
\end{lemma}

\begin{proof} To see that $(\mu/{\sim})^\uparrow$ is proper, it
  suffices to notice that $0$ is the bottom of $\cA$ and $[0] = \{0\}$
  (see \Cref{l:3}) is the bottom of $\cA/{\sim}$. Thus, should we have $[0] \in
  (\mu/{\sim})^\uparrow$ we would also have $0 \in \mu$ contradicting
  that $\mu$ is itself proper.

  Let us now show that $(\mu/{\sim})^\uparrow$ is maximal amongst
  proper filters. Let $a \in \mu$, so that $[a] \in \mu/{\sim}$. We
  argue that for all $[b] \in \algebra A/{\sim}$ either $[a] \wedge
  [b] \in \mu/{\sim}$ or $[a] - [b] \in \mu/{\sim}$, so that condition
  \ref{equivalent_three} of \Cref{max_condition} holds for
  $(\mu/{\sim})^\uparrow$. By \Cref{l:2} and \Cref{c:1}, respectively,
  we have $[a] \wedge [b] = [b \rest a]$ and $[a] - [b] = [a - (b
  \rest a)]$. Therefore, it suffices to show that one of $b \rest a$
  and $a - (b \rest a)$ belongs to $\mu$. But since $b \rest a \le a$
  by~\eqref{restricts}, and $\mu$ is a maximal filter, by
  \Cref{max_condition} this is indeed the case.
\end{proof}

\begin{lemma}\label{filter_up}
  Let $\mu \subseteq \cA$ be a maximal filter, and let $F \subseteq
  \cA$ be any filter. If the filter $(\mu \rest F)^\uparrow$ is proper, then it
  is maximal. Moreover, $(\mu \rest F)^\uparrow$ is maximal if and only if $\mu \ppreceq F$
  (and if and only if  $\mu \approx (\mu \rest
  F)^\uparrow$).
\end{lemma}

\begin{proof} Let $\mu \in \mf \cA$ and $F \in \filt \cA$ be such that
  $(\mu \rest F)^\uparrow$ is proper. Since the operations $\bmeet$
  and $-$ are both order-preserving in the first coordinate, by
  \Cref{max_condition}, to prove that $(\mu \rest F)^\uparrow$ is
  maximal, it suffices to show that for every $b \in \mu$ and $a \in
  F$ and every $c \in \cA$, one of the elements $(b \rest a)\bmeet c$ and
  $(b \rest a)-c$ belongs to $(\mu \rest F)^\uparrow$. Set $x := (a
  \bmeet c) \rest b$. Since $x \leq b$ and $b \in \mu$, by
  \Cref{max_condition} we know that either $x \in \mu$ or
   $b-x \in \mu$. In the first case we have $x \rest a \in (\mu \rest F)^\uparrow$ and we calculate
   \[x \rest a = (a \bmeet c) \rest b \rest a \just{\ref{eq:8}}= b \rest (a \bmeet c) \rest a \just{\ref{lifting}}= b \rest (a \bmeet c) \just{\eqref{eq:14}}= (b \rest a) \bmeet c.\]
   In the second case we show that
\[  (b-x)\rest a =(b \rest a)-c.\]
Since both sides of this inequality are bounded above by~$a$,
by~\Cref{l:5} it suffices to show that
\[
  (b-x)\rest a \sim(b \rest a)-c.\]
We calculate:
\begin{align*}
  [(b-x) \rest a]
  & = [(b-((a \cdot c)\rest b)) \rest a] \just {\Cref{l:2}} = [b-((a \cdot c)\rest b)] \wedge [a]
  \\ & \hspace{-18pt}\just {\Cref{c:1}} = ([b]-[a \cdot c]) \wedge [a] \just {\eqref{eq:10}} = [b] \wedge ([a]-[a \cdot c])
  \\ &  \hspace{-18pt}\just {\Cref{c:1}} = [b] \wedge [a - (a \cdot c \rest a)] \just
       {\ref{lifting}} = [b] \wedge [a - a \cdot c]
  \\ & \hspace{-5pt}\just {\eqref{eq:9}} = [b] \wedge [a - c]\just {\Cref{l:2}} =
       [b\rest(a-c)] \just {\eqref{eq:13}} = [(b \rest a) - c].
\end{align*}

To show $(\mu \rest F)^\uparrow$ is maximal if and only if $\mu \ppreceq F$, we first assume that $(\mu \rest F)^\uparrow$
is maximal. We want to show that $(F \rest \mu)^\uparrow = \mu$. As $\mu \subseteq (F \rest \mu)^\uparrow$ and $\mu$ is maximal, it suffices to show that the filter $(F \rest \mu)^\uparrow$ is proper. Suppose not: then there is $a \in F$ and $b \in \mu$ such that $a \rest b = 0$. By \Cref{l:2}, we obtain $0 \sim a \rest b \sim b \rest a$. So by \Cref{l:3}\ref{item:7}, we have $0 = b \rest a \in \mu \rest F$, contradicting properness of $(\mu \rest F)^\uparrow$

Conversely, we have $\mu
\ppreceq F$ if and only if $F \rest \mu \subseteq \mu$, which implies $\mu \rest F \rest \mu
\subseteq \mu$. So if $0$ belonged to $\mu \rest F$, it would also
belong to $\mu$, contradicting the properness of $\mu$. (The law $0 \rest a = 0$ follows from \Cref{l:3}\ref{item:7}.) Thus $(\mu \rest
F)^\uparrow$ is proper, and since it contains $\mu$, maximal.

Finally, we note that, by \Cref{l:7}, we have $\mu \ppreceq F$ if and only if  $\mu \approx (\mu \rest
F)^\uparrow$.
\end{proof}

\begin{proposition}\label{representation}

  Let $\cA$ be an algebra of the signature $\{-, \rest\}$ validating axioms
  \ref{schein1} -- \ref{lifting}, and let $\theta$ be the map
  given by
  \begin{equation*}
    a^\theta \coloneqq \{(\xi, \mu)\in \mf \cA \times \mf \cA \mid \xi
    \approx \mu \ \text{ and } \ a \in \mu \}.
  \end{equation*}
  Then $\theta$ is a representation of the $\{ -, \rest\}$-algebra
  $\algebra A$ by partial functions.
\end{proposition}
\begin{proof}
  The fact that each $a^\theta$ is a partial function on $\mf \cA$ is
  an immediate consequence of \Cref{l:8}, since (maximal) filters containing $a$ belong to the upset $(a^\uparrow)^\Uparrow \subseteq \filt\cA$.

  %
  For showing that $\theta$ represents both operations correctly, we
  pick two $\approx$-equivalent maximal filters $\xi, \mu \in \mf
  \cA$.

  For $-$ we have the following:
  \begin{align*}
    (\xi, \mu) \in a^\theta - b^\theta
    & \iff a \in \mu \ \text{ and }\ b \notin \mu
    \\  & \iff a-b \in \mu \qquad\qquad\qquad \text{(by \Cref{max_condition})}
    \\  & \iff (\xi, \mu) \in (a-b)^\theta.
  \end{align*}

  For $\rest$ suppose $(\xi, \mu) \in (a \rest b)^\theta$. Then $a
  \rest b \in \mu$, so $b \in \mu$, by \eqref{restricts}. Hence $(\xi,
  \mu) \in b^\theta$. To show that $(\xi, \mu) \in a^\theta \rest
  b^\theta$, it remains to show that $\xi$ is in the domain of the partial function
  $a^\theta$. That is, we must find a maximal filter $\nu$ with $a \in
  \nu$ and $\nu \approx \xi$. We claim that $(\mu \rest
  \{a\})^\uparrow$ is the required $\nu$. We noted that $b \in \mu$;
  hence $b \rest a \in \mu \rest \{a\}$, and hence $(\mu \rest
  \{a\})^\uparrow$ contains $a$, by \eqref{restricts}. By
  \Cref{filter_up} and using the hypothesis that $\xi \approx \mu$, we
  only need to show that $(\mu \rest \{a\})^\uparrow$ (equal to $(\mu \rest a^\uparrow)^\uparrow$) is proper. That
  is, we want to show that for every $c \in \mu$, we have $c \rest a \neq 0$. Suppose
  otherwise, and let $c \in \mu$ satisfy $c \rest a = 0$.
  Then we would have $(a \rest b) \bmeet c \in \mu$. But
  \[(a \rest b) \bmeet c \just{\eqref{eq:14}}= (a \rest c) \bmeet b \just{\Cref{l:2}}\sim (c \rest a) \bmeet b =0,\]
    which by \Cref{l:3}\ref{item:7} yields $(a \rest b) \bmeet c = 0$, contradicting the properness of $\mu$.

  Conversely, suppose $(\xi, \mu) \in a^\theta \rest b^\theta$. So we
  know $b \in \mu$ and that there exists a maximal filter $\nu$
  containing $a$ such that $\xi \approx \nu$. In particular, since
  $\mu \approx \xi \approx \nu$, $[a] \wedge [b] = [a \rest b] \in
  (\mu/{\sim})^{\uparrow}$.
  %
  Since $\mu$ is maximal, by \Cref{max_condition} it contains exactly
  one of the elements $a \rest b$ and $b-(a \rest b)$.

  Plainly it cannot be $b - (a \rest b)$, else both $[b - (a \rest
  b)]$ and $[a \rest b]$ would be in $(\mu/{\sim})^\uparrow$, yielding
  $[0] \in (\mu/{\sim})^\uparrow$, by \Cref{c:1}
  and~\eqref{disjoint_0}. We conclude that $a \rest b \in \mu$. Hence
  $(\xi, \mu) \in (a \rest b)^\theta$.

  Finally, we show that $\theta$ is injective. Since $\theta$ is a
  homomorphism, we have $a^\theta = b^\theta$ if and only if
  $(a-b)^\theta = \emptyset = (b-a)^\theta$. In turn, by
  \Cref{extension} this holds exactly when $a-b = 0 = b-a$, which implies $a = b$.

\end{proof}

\begin{theorem}\label{axiomatisation}
The class of $\{ -, \rest\}$-algebras representable by partial functions is a variety, axiomatised by the finite set of equations \ref{schein1} -- \ref{lifting}.
\end{theorem}

\begin{proof}
  As we saw in \Cref{preliminaries} all representable algebras validate the
  axioms. By \Cref{representation}, every $\{ -,
  \rest\}$-algebra validating the axioms is representable.
\end{proof}

We finish this section with an alternative representation of any representable $\{-,
\rest\}$-algebra, using only
\emph{injective} partial functions. This representation is built from the representation exhibited
in \Cref{representation}.

\begin{corollary}
  Let $\cA$ be an algebra of the signature $\{-, \rest\}$ validating  axioms
  \ref{schein1} -- \ref{lifting}, and let $\eta$ be the map given
  by
  \begin{equation*}
    a^\eta \coloneqq \{(\dbracket \mu, \mu)\in (\mf \cA/{\approx})
    \times \mf \cA \mid  a \in \mu \}.
  \end{equation*}
  Then $\eta$ is a representation of~$\algebra A$ by injective partial
  functions.
\end{corollary}
\begin{proof}
  This is a simple consequence of \Cref{representation} together with
  the observation that, for all maximal filters $\xi, \mu \subseteq
  \cA$ and $a \in \cA$, we have
  \[(\xi, \mu)\in a^\theta \iff (\dbracket \xi, \mu) \in a^\eta. \qedhere\]
\end{proof}

\begin{corollary}\label{cor:rep}
  The class of $\{ -, \rest\}$-algebras representable by injective
  partial functions is a variety, axiomatised by the finite set of
  equations \ref{schein1} -- \ref{lifting}.
\end{corollary}

\section{Complete representability}\label{sec:complete}

In this section we discuss complete representations of $\{-, \rest\}$-algebras and investigate the axiomatisability of the class of completely representable algebras.

The next two definitions apply to any function from a poset $\cP$ to a poset $\cQ$. So in particular, these definitions apply to
representations of Boolean algebras as fields of sets as well as to
representations of $\{ -, \rest\}$-algebras by partial
functions, where a representation of a Boolean algebra is viewed as an embedding into a full powerset algebra, and a representation of a $\{ -, \rest\}$-algebra is viewed as an embedding into the algebra of all partial functions on the base. Since it is mainly these two cases we will be concerned with in this section, we will
represent meets and joins in~$\cP$ by~$\meet$ and~$\join$ respectively and meets and joins in~$\cQ$
by~$\bigcap$ and~$\bigcup$ respectively, using subscripts if it is necessary to be more precise about which poset we are in.

\begin{definition}\label{def:meet}
  A function $h: \cP \to \cQ$ is \defn{meet complete} if, for every
  nonempty subset~$S$ of~$\algebra{P}$, if $\meet S$ exists, then so
  does $\bigcap h[S]$ and
  \[h(\meet S) = \bigcap h[S]\text{.}\]
\end{definition}

\begin{definition}\label{def:join}
  A function $h: \cP \to \cQ$ is \defn{join complete} if, for every
  subset~$S$ of~$\algebra{P}$, if $\join S$ exists, then so does
  $\bigcup h[S]$ and
  \[h(\join S) = \bigcup h[S].\]
\end{definition}

Note that $S$ is required to be nonempty in \Cref{def:meet}, but not
in \Cref{def:join}. A Boolean algebra can be represented using a meet-complete representation if and only if it can be represented using a join-complete representation, for the simple
reason that any meet-complete homomorphism \emph{is} join-complete,
and vice versa. So in this case we may simply describe such a
homomorphism using the adjective \defn{complete}.\begin{NoHyper}\footnote{In the case
  of representations of Boolean algebras as fields of sets, other
  adjectives have been used. Dana Scott suggested \emph{strong}, which
  was subsequently used by Roger Lyndon; John Harding uses
  \emph{regular}.}\end{NoHyper} The signature $\{ -, \rest\}$ is expressive enough
that the same remarks apply to it, as we will now see.

We now start to follow a part of \cite{complete} very closely---the end
of Section 2 and beginning of Section 3 there. The upcoming several
proofs (up to \Cref{atomistic}) are trivial adaptations of the proofs found in that paper, but
it is worth including them here, since they are all rather short. Note that although, in view of the subject of this paper, we choose to state some of these results in terms of representations of $\{-, \rest\}$-algebras by partial functions, the $\rest$ operation plays no role---the results hold more generally for representations of $\{-\}$-algebras by sets.

\begin{lemma}\label{l:15}
  Let $\algebra{A}$ and $\cB$ be subtraction algebras and $h: \cA
  \to \cB$ a homomorphism. For each $a\in \cA$, let $h_a: a^\downarrow
  \to h(a)^\downarrow$ denote the homomorphism of Boolean algebras
  induced by~$h$ (recall \Cref{c:3}). If $h$ is meet complete or
  join complete, then $h_a$ is complete.
\end{lemma}

\begin{proof}
  Suppose $h$ is meet complete. If $S$ is a nonempty subset of
  $a^\downarrow$, then all lower bounds for $S$ in $\algebra{A}$ are
  also in $a^\downarrow$. Hence if $\meet_{a^\downarrow} S$ exists
  then it equals $\meet_{\algebra{A}} S$, and so $\bigcap_{\algebra B} h[S]$ exists and equals $h(\meet_{a^\downarrow} S)$. This equality also tells us that $\bigcap_{\algebra B} h[S] \in h(a)^\downarrow$. Hence
  $h(\meet_{a^\downarrow} S) = \bigcap_{\algebra B} h[S] = \bigcap_{h(a)^\downarrow} h[S]$. So ~$h_a$ is
  complete.

  Suppose that $h$ is join complete, $S \subseteq a^\downarrow$, and
  $\join_{a^\downarrow} S$ exists. If $c \in \algebra{A}$ and $c$ is
  an upper bound for $S$, then $c \geq c \bmeet a \geq
  \join_{a^\downarrow} S$. Hence $\join_{a^\downarrow} S =
  \join_{\algebra{A}} S$, giving the existence of $\bigcup_{\algebra B} h[S]$ and
  the equality $h(\join_{a^\downarrow} S) = h(\join_{\algebra{A}} S) =
  \bigcup_{\algebra B} h[S]$. This equality also tells us that $\bigcup_{\algebra B} h[S] \in h(a)^\downarrow$. Hence $h(\join_{a^\downarrow} S) =\bigcup_{\algebra B} h[S] = \bigcup_{h(a)^\downarrow} h[S]$. So $h_a$ is complete.
\end{proof}

\begin{corollary}\label{lemma:Boolean}
  Let $\algebra{A}$ be an algebra of the signature $\{ -, \rest\}$. Any
  representation $\theta$ of $\algebra{A}$ by partial functions
  restricts to a representation of $a^\downarrow$ as a field of sets
  over $\theta(a)$, which is complete if $\theta$ is meet complete or
  join complete.
\end{corollary}

\begin{corollary}\label{cor:1}
  Let $\algebra{A}$ and $\cB$ be subtraction algebras and $h: \cA
  \to \cB$ be a homomorphism. If $h$ is meet complete, then it is join
  complete.
\end{corollary}
\begin{proof}
  Suppose that $h$ is meet complete. Let $S$ be a subset of
  $\algebra{A}$ and suppose that $\join_{\algebra{A}} S$ exists. Let
  $a = \join_{\algebra{A}} S$. Then $h_a$ is complete and so
  \[h(\join_{\algebra{A}} S) = h(\join_{a^\downarrow} S) = \bigcup_{h(a)^\downarrow}
    h[S]= \bigcup_{\algebra B}
    h[S]\text{.}\qedhere\]
\end{proof}

\begin{corollary}\label{cor:2}
  Let $\algebra{A}$ and $\cB$ be subtraction algebras and $h: \cA
  \to \cB$ be a homomorphism. If $h$ is join complete, then it is meet
  complete.
\end{corollary}
\begin{proof}
  Suppose that $h$ is join complete. Let $S$ be a nonempty subset of
  $\algebra{A}$ and suppose that $\meet_{\algebra{A}} S$ exists. As
  $S$ is nonempty, we can find $s \in S$. We let $S \bmeet s$ denote the set $\{s' \bmeet s \mid s' \in S\}$. Then $h_s$ is complete and
  \[h(\meet_{\algebra{A}} S) = h(\meet_{\algebra{A}} (S \bmeet s))
    = h(\meet_{s^\downarrow} (S \bmeet s)) = \bigcap_{h(s)^\downarrow} h[S \bmeet
    s] =\bigcap_{\algebra B} h[S \bmeet
    s] = \bigcap_{\algebra B} h[S]\text{.}\qedhere\]
\end{proof}

We have established that there is but one notion of complete homomorphism for representable $\{ -, \rest\}$-algebras. Hence there is but one notion of
complete representation for $\{ -, \rest\}$-algebras. If a $\{ -, \rest\}$-algebra has a complete representation we say it is \defn{completely representable}.

We now move
on and consider the property of being atomic, both for algebras and
for representations. We will see that the completely representable
algebras are precisely the algebras that are representable and atomic.

\begin{definition}
Let $\algebra{P}$ be a poset with a least element, $0$. An \defn{atom} of $\algebra{P}$ is a minimal nonzero element of $\algebra{P}$. We write $\At(\algebra{P})$ for the set of atoms of $\algebra P$. We say that $\algebra{P}$ is \defn{atomic} if every nonzero element is greater than or equal to an atom.
\end{definition}

We note that representations of $\{ -, \rest\}$-algebras necessarily
represent the partial order by set inclusion: this may be seen as a
consequence of \Cref{lemma:Boolean}. The following definition is
meaningful for any notion of representation where this is the case.

\begin{definition}
Let $\algebra{P}$ be a poset with a least element and let $\theta$ be a representation of $\algebra{P}$. Then $\theta$ is \defn{atomic} if $x \in \theta(a)$ for some $a \in \algebra{P}$ implies $x \in \theta(b)$ for some atom $b$ of $\algebra{P}$.
\end{definition}

We will need the following theorem.

\begin{theorem}[Hirsch and Hodkinson \cite{journals/jsyml/HirschH97a}]\label{thm:hirsch-hodkinson} Let $\algebra{B}$ be a Boolean algebra. A representation of $\algebra{B}$ as a field of sets is atomic if and only if it is complete.
\end{theorem}

\begin{proposition}\label{prop:at-com}
Let $\algebra{A}$ be an algebra of the signature $\{ -, \rest\}$ and $\theta$ be a representation of $\algebra{A}$ by partial functions. Then $\theta$ is atomic if and only if it is complete.
\end{proposition}

\begin{proof}
Suppose that $\theta$ is atomic, $S$ is a nonempty subset of $\algebra{A}$ and $\meet S$ exists. It is always true that $\theta(\meet S) \subseteq \bigcap \theta[S]$, regardless of whether or not $\theta$ is atomic. For the reverse inclusion, we have
\[\begin{array}{cll}
 & (x, y) \in \bigcap \theta[S]
\\ \implies & (x, y) \in \theta(s) & \text{for all }s \in S
\\ \implies & (x, y) \in \theta(a) & \text{for some atom }a\text{ such that }(\forall s \in S)\text{ } a \leq s
\\ \implies & (x, y) \in \theta(a) & \text{for some atom }a\text{ such that } a \leq \meet S
\\ \implies &  (x, y) \in \theta(\meet S)\text{.}
\end{array}\]
The third line follows from the second because, choosing an $s_0 \in S$ we have $(x, y) \in \theta(s_0)$, hence some atom $a$  with $(x, y) \in \theta(a)$, and thus $(x, y) \in \theta(a \bmeet s)$ for any $s \in S$. So for all $s \in S$, the element $a \bmeet s$ is nonzero, so equals $a$, by atomicity of $a$, giving $a \leq s$.

Conversely, suppose that $\theta$ is complete. Let $(x, y)$ be a pair contained in $\theta(a)$ for some $a \in \algebra{A}$. By \Cref{lemma:Boolean}, the map $\theta$ restricts to a complete representation of $a^\downarrow$ as a field of sets. Hence, by \Cref{thm:hirsch-hodkinson}, $(x, y) \in \theta(b)$ for some atom $b$ of the Boolean algebra $a^\downarrow$. Since an atom of $a^\downarrow$ is clearly an atom of $\algebra{A}$, the representation $\theta$ is atomic.
\end{proof}

\begin{corollary}\label{cor:atomic}
Let $\algebra{A}$ be an algebra of the signature $\{ -, \rest\}$. If $\algebra{A}$ is completely representable by partial functions then $\algebra{A}$ is atomic.
\end{corollary}

\begin{proof}
Let $a$ be a nonzero element of $\algebra{A}$. Let $\theta$ be any complete representation of $\algebra{A}$. Then $\emptyset = \theta(0) \neq \theta(a)$, so there exists $(x, y) \in \theta(a)$. By \Cref{prop:at-com}, the map $\theta$ is atomic, so $(x, y) \in \theta(b)$ for some atom $b$ in $\algebra{A}$. Then $(x, y) \in \theta(a \bmeet b)$, so $a \bmeet b > 0$, from which we may conclude that the atom $b$ satisfies $b \leq a$.
\end{proof}

For Boolean algebras, the algebra being atomic is necessary and sufficient for complete representability \cite{Abian01051971}. On the other hand, there exist scenarios in which being atomic is necessary but \emph{not} sufficient for complete representability, for example for the signature of composition, intersection, and antidomain, for representation by partial functions (\cite[Proposition 4.6]{complete}). Do we have sufficiency in our case? The answer is yes. But before we prove this we need a couple more lemmas.

\begin{definition}
A poset $\algebra{P}$ is \defn{atomistic} if its atoms are join dense in $\algebra{P}$. That is to say that every element of $\algebra{P}$ is the join of the atoms less than or equal to it.
\end{definition}

Clearly any atomistic poset is atomic. For $\{ -, \rest\}$-algebras representable by partial functions, the converse is also true.

\begin{lemma}\label{atomistic}
Let $\algebra{A}$ be a subtraction algebra. If $\algebra{A}$ is atomic, then it is atomistic.
\end{lemma}

\begin{proof}
  Suppose $\algebra{A}$ is atomic and let $a \in \algebra{A}$. We know the algebra $a^\downarrow$ is a Boolean algebra and
  clearly it is atomic. It is well-known that atomic Boolean algebras
  are atomistic. So we have
\[
a = \join_{a^\downarrow} \At(a^\downarrow)   = \join_{\algebra{A}}  \At(a^\downarrow) = \join_{\algebra{A}} \{ x \in \At(\algebra{A}) \mid x \leq a \}\text{.}
\]
The second equality holds because any upper bound $c \in \algebra{A}$ for $\At(a^\downarrow)$ is above an upper bound in $a^\downarrow$, for example $c \bmeet a$. Hence the least upper bound in $a^\downarrow$ is least in $\algebra{A}$ also.
\end{proof}

The last lemma concerns properties of the atoms of representable $\{-, \rest\}$-algebras.

\begin{lemma}\label{l:atom_preserved}
  Let $\algebra{A}$ be a representable algebra of the signature $\{ -,
  \rest\}$. Then
  \begin{enumerate}[label=(\alph*)]
  \item\label{item:1} if $x \in \At(\cA)$, then $[x] \in \At
    (\cA/{\sim})$;
  \item\label{item:2} for every $a \in \cA$ and $x \in \At(\cA)$,
    either $x \rest a = 0$ or $x \rest a$ is an atom. And moreover, $x
    \rest a$ is an atom if and only if $x \preceq a$  (and if and only if  $x \sim x \rest a$).
  \end{enumerate}
\end{lemma}
\begin{proof}\leavevmode
  \begin{enumerate}[label = (\alph*)]
  \item Let $a \in \cA$ be such that $[a] \prec [x]$. Then $a \rest x
    < x$. (We cannot have $a \rest x = x$, else, by \Cref{l:2}, $[x]
    \preceq [a]$.)  But then as $x$ is an atom, $a \rest x = 0$. Hence
    $[a] = [a \rest x] = [0]$. As $[a]$ was an arbitrary element below
    $[x]$, we conclude that $[x]$ is an atom.

  \item Suppose $x \rest a \neq 0$ and let $b \in \cA$ be such that $0
    \leq b < x \rest a$. By \Cref{c:2}, we have $0 \preceq b \prec x
    \rest a$ and, by~\Cref{l:2}, $x \rest a \preceq x$. But by
    part~\ref{item:1}, $[x]$ is an atom, and thus, $0 \sim b$ and $x
    \rest a \sim x$. This yields $b = 0$, and so, $x \rest a$ is an
    atom, and $x \preceq a$. Finally, by~\Cref{l:2} we have $x \preceq a$ if and only if  $x \sim x \rest a$. \qedhere
\end{enumerate}

\end{proof}

\begin{proposition}\label{complete_representation}
  Let $\algebra A$ be an atomic and representable $\{ -,
  \rest\}$-algebra. Let $\theta$ be the map given by
  \begin{equation*}
    a^\theta \coloneqq \{(x,y) \in \At(\algebra A) \times \At(\algebra
    A) \mid  \ x \sim y \ \text{ and }\ y \leq a\}.
  \end{equation*}
  Then $\theta$ is a complete representation of $\algebra A$ by
  partial functions.
\end{proposition}

\begin{proof}
  First we show that the relation $a^\theta$ is a partial
  function. That is, we argue that if $x \sim y \sim z$ for atoms $x,
  y, z$, with $y, z \le a$,  then $y = z$. But this is a consequence
  of Lemma~\ref{l:5}.

  Next we show that $\theta$ represents each operation correctly. We
  pick $a, b \in \algebra A$ and two
  $\sim$-equivalent atoms $x,y \in \At(\cA)$ .

  Showing that $(a-b)^\theta = a^\theta - b^\theta$ amounts to
  showing that
  \[y \leq a-b \iff (y \leq a\ \text{ and } \ y\not\leq b).\]
  By~\eqref{eq:10}, if $y \leq a-b$ then $y \leq a$. Suppose that
  we also have $y \leq b$. Then, $y \leq b\cdot (a-b)$ which,
  by~\eqref{disjoint_0}, yields $y = 0$, a contradiction. This shows
  the forward implication. Conversely, since $y \in
  \At(a^{\downarrow})$ and $a - b$ and $a \bmeet b$ are complements in the
  Boolean algebra $a^\downarrow$, it follows that $y \leq a - b$
  (because we are assuming $y \not\leq b$). Thus, we conclude that
  $\theta$ represents $-$ correctly.

  For $\rest$, first suppose that $(x,y) \in (a \rest
  b)^\theta$. Clearly, $(x,y) \in b^\theta$. We show that $(x, y \rest
  a) \in a^\theta$, and thus $x \in \dom (a^\theta)$, yielding $(x, y)
  \in a^\theta \rest b^\theta$. By \Cref{l:2}, we have $a \rest b
  \preceq a$, and since, by Lemma~\ref{l:3}, $\preceq$ includes $\leq$,
  we have $y \preceq a \rest b$. Thus, $y \preceq a$ and, again
  by~\Cref{l:2}, we have $y \sim y \rest a$. Since $x\sim y$ by
  hypothesis, we conclude $(x, y \rest a) \in a^\theta$ as claimed.

  Conversely, suppose $(x,y) \in a^\theta \rest b^\theta$, that is, $x
  \in \dom(a^\theta)$ and $y \leq b$. Since $y$ is an atom of the
  Boolean algebra $b^\downarrow$, we have $y \le a \rest b$ or $y \le
  b-(a \rest b)$. We suppose that $y \le b-(a \rest b)$ and we let $z
  \in \At(a^\downarrow)$ be $\sim$-equivalent to~$x$. Using that $\le$ is included in $\preceq$, we have $y \preceq b- (a \rest b)$ and $z
  \preceq a$. Since $x \sim y \sim z$, it follows by~\Cref{l:2} that
  $x \preceq a \rest (b-(a \rest b))$. Finally, using \Cref{c:1}
  and~\eqref{disjoint_0}, we conclude that $[x] = 0$, hence by \Cref{l:3}\ref{item:7} that $x = 0$, which is a
  contradiction. Therefore, we have $y \le (a \rest b)$ as intended.

  Next, we note that $\theta$ is injective. If $a^\theta = b^\theta$
  then $a$ and $b$ are greater than or equal to the same set of
  atoms. Since $\algebra A$ is atomistic (\Cref{atomistic}), $a$ and
  $b$ are each the supremum of this set of atoms, hence are equal.

  Finally, we show that $\theta$ turns any suprema that exist into
  unions. Suppose an element $a \in \algebra A$ is the supremum of
  some $S \subseteq \algebra A$, and let $b$ be an atom. Clearly if $b
  \leq s$ for some $s \in S$ then $b \leq a$. Conversely, suppose for
  all $s \in S$ we have $b \not\leq s$. Then as $b$ is an atom, for
  each $s$ we have $s \bmeet b = 0$. So in the Boolean algebra
  $a^\downarrow$ we have $s = s \bmeet ((a - b) + a \bmeet b) = s \bmeet (a -
  b) + s \bmeet a \bmeet b = s \bmeet (a - b) + 0 = s \bmeet (a -b)$. So $s
  \leq a - b$, and that holds for each $s \in S$. Hence $a - b$ is an
  upper bound for $S$, so $a = \join S \leq a - b$. Since $b$ is nonzero, it follows that $b
  \not\leq a$. We have shown that $b \leq \join S \iff b \leq s$ for
  some $s \in S$. Hence $(\join S)^\theta = \bigcup_{s \in S}
  s^\theta$. We conclude that $\theta$ is a complete representation.
\end{proof}

\begin{theorem}\label{complete_axiomatisation}
The class of $\{ -, \rest\}$-algebras that are completely representable by partial functions is axiomatised by the finite set of equations \ref{schein1} -- \ref{lifting} together with the $\forall\exists\forall$ first-order formula stating that the algebra is atomic.
\end{theorem}

\begin{proof}
By definition, the completely representable algebras are representable, and by \Cref{cor:atomic} they are atomic. \Cref{complete_representation} tells us the converse---that any representable and atomic algebra is completely representable. Hence the completely representable algebras are precisely those that are both representable and atomic. By \Cref{axiomatisation}, equations \ref{schein1} -- \ref{lifting} axiomatise representability. So with the addition of the formula stating the algebra is atomic, an axiomatisation of the completely representable algebras is obtained.
\end{proof}

As before, we can use the representation of \Cref{complete_representation} to
get a complete representation by \emph{injective} partial functions.
\begin{corollary}
  Let $\algebra A$ be an atomic and representable $\{ -,
  \rest\}$-algebra. Let $\eta$ be the map given by
  \begin{equation*}
    a^\eta \coloneqq \{([x],x) \in (\At(\algebra A)/{\sim}) \times \At(\algebra
    A) \mid  x \leq a\}.
  \end{equation*}
  Then $\eta$ is a complete representation of $\algebra A$ by
  injective partial functions.
\end{corollary}
\begin{proof}
  This follows from \Cref{complete_representation} together with the
  observation that for every $x, y \in \At(\cA)$ and $a\in \cA$, we
  have
  \[([y],x) \in a^\eta \iff (y, x) \in a^\theta. \qedhere\]
\end{proof}

\begin{corollary}\label{complete_corollary}
The class of $\{ -, \rest\}$-algebras that are completely representable by injective partial functions is axiomatised by the finite set of equations \ref{schein1} -- \ref{lifting} together with the $\forall\exists\forall$ first-order formula stating that the algebra is atomic.
\end{corollary}

The axiomatisation of \Cref{complete_axiomatisation} and \Cref{complete_corollary} uses the minimum possible degree of quantifier alternation, for it is not possible to axiomatise these classes using any $\exists\forall\exists$ first-order theory, finite or otherwise.

\begin{proposition}
The class of $\{ -, \rest\}$-algebras that are completely representable by partial functions and the class of $\{ -, \rest\}$-algebras that are completely representable by injective partial functions are not axiomatisable by any $\exists\forall\exists$ first-order theory.
\end{proposition}

\begin{proof}
Any Boolean algebra $(B, 0, 1, \bmeet, \compl{\phantom{c}})$  can be interpreted as an algebra of the signature $\{ -, \rest\}$ by setting $a - b \coloneqq a \bmeet \compl{b}$ and $a \rest b \coloneqq a \bmeet b$. There exist Boolean algebras $\algebra B$ and $\algebra B'$ with $\algebra B$ atomic and $\algebra B'$ not, such that $\algebra B$ and $\algebra B'$ satisfy the same $\exists\forall\exists$ first-order theory---see \cite[Proposition 3.7]{complete} for a proof of this fact. But $\algebra B'$, interpreted as an algebra of the signature $\{ -, \rest\}$, cannot be completely representable by partial functions, as it is not atomic. On the other hand, $\algebra B$ is representable by partial functions by the following argument. By Stone's representation theorem we may assume that $\algebra{B}$ is a field of sets. Then the set of all identity functions on elements of $\algebra{B}$ forms a representation of $\algebra{B}$ by partial functions. Since $\algebra B$ is also atomic, by \Cref{complete_axiomatisation}/\Cref{complete_corollary} it is \emph{completely} representable by (injective) partial functions. Hence $\algebra B$ and $\algebra B'$ witness that any $\exists\forall\exists$ first-order theory cannot have all and only the completely representable algebras as its models.
\end{proof}

\bibliographystyle{amsplain}

redpajama_set_name: RedPajamaArXiv