2021 2098

# Theory of Constructive Semigroups with Apartness –
Foundations, Development and Practice

Melanija Mitrović
Faculty of Mechanical Engineering
University of Niš
A. Medvedeva 14 Address for correspondence: Faculty of Mechanical Engineering,
A. Medvedeva 14, 18000 Niš, Serbia.

Received March 2021; accepted January 2022. 18000 Niš  Serbia
<EMAIL_ADDRESS>Mahouton Norbert Hounkonnou1
Int. Chair in Mathematical Physics and Applications
(ICMPA-UNESCO Chair)
University of Abomey-Calavi
072 B.P. 50 Cotonou  Republic of Benin  Africa
<EMAIL_ADDRESS>
(with copy to<EMAIL_ADDRESS> Marian Alexandru Baroni1
“Dunarea de Jos” University of Galati  Romania
<EMAIL_ADDRESS>
###### Abstract

This paper has several purposes. We present through a critical review the
results from already published papers on the constructive semigroup theory,
and contribute to its further development by giving solutions to open
problems. We also draw attention to its possible applications in other
(constructive) mathematics disciplines, in computer science, social sciences,
economics, etc. Another important goal of this paper is to provide a clear,
understandable picture of constructive semigroups with apartness in Bishop’s
style both to (classical) algebraists and the ones who apply algebraic
knowledge.

###### keywords:

Semigroup with apartness, set with apartness, co-quasiorder, co-equivalence,
co-congruence.

††volume: 184††issue: 3

Theory of Constructive Semigroups with Apartness …

“Semigroups aren’t a barren, sterile flower on the tree of algebra, they are a
natural algebraic approach to some of the most fundamental concepts of algebra
(and mathematics in general), this is why they have been in existence for more
then half a century, and this is why they are here to stay.”
Boris M. Schein, [57]

##  1 Introduction

A general answer to the question what constructive mathematics is could be
formulated as follows: it is mathematics which can be implemented on a
computer. There are two main ways of developing mathematics constructively.
The first one uses classical traditional logic within a strict algorithmic
framework. The second way is to replace classical logic with _intuitionistic
logic_.

Throughout this paper _constructive mathematics_ is understood as mathematics
performed in the context of intuitionistic logic, that is, without the law of
excluded middle (LEM). There are two main characteristics for a constructivist
trend. The notion of _truth_ is not taken as primitive, and _existence_ means
constructibility. From the classical mathematics (CLASS) point of view,
mathematics consists of a preexisting mathematical truth. From a constructive
viewpoint, the judgement $\varphi$ _is true_ means that _there is a proof of_
$\varphi$. “What constitutes a proof is a social construct, an agreement among
people as to what is a valid argument. The rules of logic codify a set of
principles of reasoning that may be used in a valid proof. Constructive
(intuitionistic) logic codifies the principles of mathematical reasoning as it
is actually practiced,” [26]. In constructive mathematics, the _status of
existence statement_ is much stronger than in CLASS. The classical
interpretation is that an object exists if its non-existence is contradictory.
In constructive mathematics when the existence of an object is proved, the
proof also demonstrates how to find it. Thus, following further [26], the
_constructive logic_ can be described as logic of people matter, as distinct
from the classical logic, which may be described as the logic of the mind of
God. One of the main features of constructive mathematics is that the concepts
that are equivalent in the presence of LEM, need not be equivalent any more.
For example, we distinguish nonempty and inhabited sets, several types of
inequalities, two complements of a given set, etc.

There is no doubt about deep connections between constructive mathematics and
computer science. Moreover, “if programming is understood not as the writing
of instructions for this or that computing machine but as the design of
methods of computation that is the computer’s duty to execute, then it no
longer seems possible to distinguish the discipline of programming from
constructive mathematics”, [36].

Constructive mathematics is not a unique notion. Various forms of
constructivism have been developed over time. The principal trends include the
following varieties: INT \- Brouwer’s intuitionistic mathematics, RUSS \- the
constructive recursive mathematics of the Russian school of Markov, BISH \-
Bishop’s constructive mathematics. Every form has intuitionistic logic at its
core. Different schools have different additional principles or axioms given
by the particular approach to constructivism. For example, the notion of an
_algorithm_ or a _finite routine_ is taken as primitive in INT and BISH, while
RUSS operates with a fixed programming language and an algorithm is a sequence
of symbols in that language. We have to emphasize that Errett Bishop - style
constructive mathematics, BISH, forms the framework for our work. BISH enables
one to interpret the results both in classical mathematics and in other
varieties of constructivism. BISH originated in 1967 with the publication of
the book _Foundations of Constructive Mathematics_ , [4], and with its second,
much revised edition in 1985, [5]. There has been a steady stream of
publications contributing to Bishop’s programme since 1967. A ten-year long
systematic research of computable topology, using apartness as the fundamental
notion, resulted in the first book, [13], on topology within BISH framework.
Modern algebra, as is noticed

in [11], “contrary to Bishop’s expectations, also proved amenable to natural,
thoroughgoing, constructive treatment”.

Working within the classical theory of semigroups several years ago we, [39],
decided to change the classical background with the intuitionistic one. This
meant, among other things, that the perfect safety of the classical theory
with developed notions, notations and methodologies was left behind. Instead,
we embarked on an adventure into exploring an algebraically new area (even
without clearly stated notions and notations) of _constructive semigroups with
apartness_. What we had “in hand” at that moment was the experience and
knowledge coming from the classical semigroup theory, other constructive
mathematics disciplines such as, for example, constructive analysis, and,
especially, from constructive topology, as well as constructive theories of
groups and rings with tight apartness and computer science. For classical
algebraists who, like us, wonder “on the odd day” what constructive algebra is
all about, and who want to find out what it feels like doing it, they will
understand soon that _constructive algebra_ is more complicated than classical
algebra in various ways: algebraic structures as a rule do not carry a
decidable equality relation (this difficulty is partly met by the introduction
of a strong inequality relation, the so-called apartness relation); there is
(sometime) the awkward abundance of all kinds of substructures, and hence of
quotient structures, [61].

As highlighted by Romano DA _et al_ , [41], _the theory of semigroup with
apartness_ is a new approach to semigroup theory and not a new class of
semigroups. It presents a semigroup facet of some relatively well established
direction of constructive mathematics which, to the best of our knowledge, has
not yet been considered within the semigroup community. This paper has several
purposes: to present through a critical review results from our already
published papers, [17], [18], [41], on the constructive point of view on
semigroup theory, to contribute to its further development giving solutions to
the problems posted (in the open, or, somehow hidden way) within the scope of
those papers, and to lay the foundation for further works.

The order theory provides one of the most basic tools of semigroup theory
within CLASS. In particular, the structure of semigroups is usually most
clearly revealed through the analysis of the behaviour of their appropriate
orders. The most basic concept leads to the _quasiorders_ , reflexive and
transitive relations with the fundamental concepts being introduced whenever
possible in their natural properties. Going through [17], [18], [41], we can
conclude that one of the main objectives of those papers is to develop an
appropriate constructive order theory for semigroups with apartness. We
outline some of the basic concepts of semigroups with apartness, as special
subsets on the one hand, and orders on the other. The strongly irreflexive and
co-transitive relations are building blocks of the constructive order theory
we develop. With a primitive notion of ’set with apartness’ our main intention
was to connect all relations defined on such a set. This is done by requiring
them to be a part (subset) of an apartness. Such a relation is clearly
strongly irreflexive. If, in addition, it is co-transitive, then it is called
_co-quasiorder_.

In algebra within CLASS, the formulation of homomorphic images (together with
substructures and direct products) is one of the principal tools used to
manipulate algebraic structures. In the study of homomorphic images of an
algebraic structure, a lot of help comes from the notion of a quotient
structure, which captures all homomorphic images, at least up to isomorphism.
On the other hand, the homomorphism is the concept which goes hand in hand
with congruences. The relationship between quotients, homomorphisms and
congruences is described by the celebrated _isomorphism theorems_ , which are
a general and important foundational part of abstract and universal algebras.
The quotient structures are not part of BISH. The quotient structure does not,
in general, have a natural apartness relation. So, _the Quotient Structure
Problem_ (QSP) is one of the very first problem which has to be considered for
any structure with apartness. The solutions of QSP problem for sets and
semigroups with apartness were given in [17]. Some examples of special cases
can be found in [52] and [53]. _Co-equivalences_ , symmetric co-quasiorders,
and equivalences which can be associated to them play the main roles. As an
example that a single concept of classical mathematics may split into two or
more distinct concepts when working constructively we have logical $\neg Y$
and apartness $\sim Y$ complement of a given subset $Y$ of a set or semigroup
with apartness. The key for the solution of the QSP for a set and semigroup
with apartness is given by the next theorem (Theorem 2.3, [17]).

###### Theorem 1.1

If $\kappa$ is a co-equivalence on $S$, then the relation ${\sim}\kappa$ is an
equivalence on $S$, and $\kappa$ defines apartness on $S/\,\sim\kappa$.

Theorem 1.1 is the key ingredient to formulate and prove the apartness
isomorphism theorem for a set with apartness (see [17], Theorem 2.5). Based on
these results, the apartness isomorphism theorem for a semigroup with
apartness ([17], Theorem 3.4) is formulated and proved as well. The just
mentioned results are significantly improved in [41], where, among other
things, it is proved that the two complements, logical and apartness, coincide
for a co-quasiorder $\tau$ defined on a set or semigroup with apartness, i.e.
we have $\sim\tau=\neg\tau$ (see Proposition 2.3, Theorem 2.4 from [41]).

###### Remark 1

In [40], an overview to the development of isomorphism theorems in certain
algebraic structures - from classical to constructive - is given.

It is well known that within CLASS  a number of subsets of a semigroup enjoy
special properties relative to multiplication, for example, completely
isolated subset, convex subset, subsemigroup, ideal. On the other hand,
relations defined on a semigroup can be distinguished one from another
according to the behaviour of their related elements to multiplication. From
that point of view, _positive quasiorders_ are of special interest. Going
through literature with the theory of semigroups as the main topic, one can
see that there is almost no method of studying semigroups without a certain
type of positive quasiorders involved. It is often the case that results on
connections between positive quasiorders and subsets defined above showed them
fruitful as well. Partly inspired by classical results, in [18] we consider
_complement positive co-quasiorders_ , i.e. constructive counterparts of
positive quasiorders, and their connections with special subsets of semigroups
with apartness. Inspired by the existing notion from constructive analysis and
topology, we use the complements (both of them) for the classification of
subsets of a given set with apartness. _Strongly detachable subsets_ , i.e.
those subsets for which we can decide whether an element $x$ from that set
belongs to the subset in question or to its apartness complement, play a
significant role within the scope of [18]. In Lemma 3.2, we prove that for any
co-quasiorder $\tau$, defined on a set with apartness, its left and right
$\tau$-classes of any element are strongly detachable subsets. The main result
of this paper, Theorem 4.1, gives the description of a complement positive co-
quasiorder, defined on a semigroup with apartness, via the behaviour of its
left and right classes and their connections with special subsets.

Apart from the above issues, an addition problem is the so-called _constant
domain axiom_ : the folklore type of axiom in CLASS algebra

$\varphi\,\vee\,\forall x\,\psi(x)\ \leftrightarrow\ \forall
x\,(\varphi\,\vee\,\psi(x)),$

its constructive version

$\varphi\,\vee\,\forall_{x}\,\psi(x)\ \rightarrow\
\forall_{x}\,(\varphi\,\vee\,\psi(x))$

can be a source of problems when doing algebra constructively. We choose
intuitionistic logic of constant domains CD to be the background of [18].
Recall that intermediate logic, such as, for example CD, the logic that is
stronger than intuitionistic logic but weaker than classical one, can be
constructed by adding one or more axioms to intuitionistic logic. There is a
continuum of such logics. For more details see [1], [23].

The presence of apartness implies the appearance of different types of
substructures connected to it. We deal with strongly detachable subsets in
[18]. In [41] we mentioned two more: detachable and quasi-detachable subsets.
In Proposition 2.1 we show that a strongly detachable subset is detachable and
quasi-detachable. Even more, from [41] the apartness and logical complements
coincide for strongly detachable and quasi-detachable subsets.

Going through [18] and [41] it can be noticed that we can face several
problems arising from their scope. For example,

  * •

The relations between detachable, strongly detachable and quasi detachable
subsets are only partially described in [41], Proposition 2.1. A complete
description of their relationship remains an open problem.

  * •

Are the results of [18] valid in intuitionistic logic if we work with quasi-
detachable subsets instead of strongly detachable ones? Which of the presented
results or their form(s) are valid for the intuitionistic background, if any?

To conclude, the theory of semigroup with apartness, its background and
motivations, further development and its possible applications as well as the
critical answers to a number of questions including those mentioned above will
be the main topics throughout this paper.

The paper is organized in the following way. In our work on constructive
semigroups with apartness, as it is pointed out above, we have faced an
algebraically completely new area. The background and motivation coming from
the classical semigroup theory, other constructive mathematics disciplines and
computer science are the content of Section 2. Some results on classical
semigroups which can partly be seen as an inspiration for the constructive
ones are also discussed here. In Section 3, the main one, we are going to give
a critical review of some of the published results on sets and semigroups with
apartness as well as the solutions to some of the open problems on sets and
semigroups with apartness. One of the main results, Theorem 3.1, gives a
complete description of the relationships between distinguished subsets of a
set with apartness, which, in turn, justifies the constructive order theory we
develop with those subsets with the main role in that framework. By
Proposition 3.2, if any left/right-class of a co-quasiorder defined on a set
with apartness is a (strongly) detachable subset then the limited principle of
omniscience, LPO, holds. This shows that Theorem 4.1 (and Lemma 3.2 important
for its proof) set in [18] cannot be proved in BISH without the logic of
constant domains CD. Within intuitionistic logic, we can prove its weaker
version, Theorem 3.7, which is another important result of this section. As
for QSP, for sets and semigroups with apartness, we achieve a little progress
in that direction. Theorem 3.2, the key theorem for the QSP’s solution,
generalizes the similar ones from [17], [41]. In addition, as a generalization
of the first apartness isomorphism theorem, the new theorem, Theorem 3.4, the
second apartness isomorphism theorem for sets with apartness, is formulated
and proved. Finally, in Section 4, examples of some already existing
applications as well as future possible realizations of the ideas presented in
the previous section are given.

More background on constructive mathematics can be found in [3], [4], [13],
[61]. The standard reference for constructive algebra is [38]. For the
classical case see [39], [43]. Examples of applications of these theoretical
concepts can be found in [2], [12], [16], [25], [42].

##  2 Preliminaries: background, known results and motivation

Starting our work on constructive semigroups with apartness, as pointed out
above, we faced an algebraically completely new area. What we had in “hand” at
that moment were the experience and knowledge coming from the classical
semigroup theory, other constructive mathematics disciplines, and computer
science.

###  2.1 Algebra and semigroups within CLASS

“I was just going to say, when I was interrupted, that one of the many ways of
classifying minds is under the heads of arithmetical and algebraical
intellects. All economical and practical wisdom is an extension of the
following arithmetical formula: 2 + 2 = 4. Every philosophical proposition has
the more general character of the expression a + b = c. We are mere
operatives, empirics, and egotists until we learn to think in letters instead
of figures .”

Oliver Wendell Holmes: _The Autocrat of the Breakfast Table_

A very short account of abstract algebra and its development will be given
here. Over the course of the 19th century, algebra made a transition from a
subject concerned entirely with the solution of mostly polynomial equations to
a discipline that deals with general structures within mathematics. The term
abstract algebra as a name for this area appeared in the early 20th century.
“In studying abstract algebra, a so called axiomatic approach is taken; that
is, we take a collection of objects $S$ and assume some rules about their
structure. These rules are called axioms. Using the axioms for $S$, we wish to
derive other information about $S$ by using logical arguments. We require that
our axioms be consistent; that is, they should not contradict one another. We
also demand that there not be to many axioms. If a system of axioms is too
restrictive, there will be few examples of the algebraic structure,” [33].

An _algebraic structure_ can be, informally, described as a set of some
elements of objects with some (not necessarily, but often, binary) operations
for combining them. A _set_ is considered as a primitive notion which one does
not define. We will take the intuitive approach that a set is some given
collection of objects, called elements or members of the set. The cartesian
product of a set $S$ with itself, $S\times S$, is of special importance. A
subset $\rho$ of $S\times S$, or, equivalently, a property applicable to
elements of $S\times S$, is called a _binary relation on_ $S$. The ordered
pair $(S,\rho)$ is a particular _relational structure_. In general, there are
many properties (for example: reflexivity, symmetry, transitivity) that binary
relations may satisfy on a given set. As usual, for a relation $\rho$ on $S$,
$a\rho=\\{x\in S:(a,x)\in\rho\\}$, and $\rho a=\\{x\in S:(x,a)\in\rho\\}$ are
the left and the right $\rho$-class of the element $a\in S$ respectively. The
concept of an _equivalence_ , i.e. reflexive, symmetric and transitive
relation, is an extremely important one and plays a central role in
mathematics. If $\varepsilon$ is an equivalence on a set $S$, then
$S/\varepsilon=\\{x\varepsilon:x\in S\\}$ is called the _quotient set of_ $S$
_by_ $\varepsilon$. Classifying objects according to some property is a
frequent procedure in many fields. Grouping elements in “a company” so that
elements in each group are of the same prescribed property as performed by
equivalence relations, and the classification gives the corresponding quotient
sets. Thus, abstract algebra can show us how to identify objects with the same
properties properly - we have to switch to a quotient structure (technique
applicable, for example, to abstract data type theory).

Some fundamental concepts in abstract algebra are: set and operation(s)
defined on that set; certain algebraic laws that all elements of a structure
can respect, such as, for example, associativity, commutativity; some elements
with special behaviour in connection with operation(s): idempotent elements,
identity element, inverse elements, … Combining the above concepts gives some
of the most important structures in mathematics: groups, rings, semigroups, …
Centred around an algebraic structure are notions of: substructure,
homomorphism, isomorphism, congruence, quotient structure. A mapping between
two algebraic structures of the same type, that preserves the operation(s) or
is compatible with the operation(s) of the structures is called
_homomorphism_. Homomorphisms are essential to the study of any class of
algebraic objects. An equivalence relation $\rho$ on an algebraic structure
$S$ (such as a group, a ring, or a semigroup) that is compatible with the
structure is called a _congruence_. Within CLASS the quotient set $S/\rho$
becomes the structure of the same type in a natural way. The relationship
between quotients, homomorphisms and congruences is described by the
celebrated _isomorphism theorems_. Isomorphism theorems are a general and
important foundational part of abstract and universal algebra.

“Algebra is beautiful. It is so beautiful that many people forget that algebra
can be very useful as well,” [35]. Abstract algebra is the highest level of
abstraction. Understanding it means, among other things, that one can think
more clearly, more efficiently. With the development of computing in the last
several decades, applications that involve algebraic structures have become
increasingly important. To mention a few, lot of data structures form monoids
(semigroups with the identity element); algebraic properties are important for
parallel execution of programs - for example, combining a list of items with
some binary operators can be easily parallelized if that operator is
associative (commutativity is often required as well). Examples of
applications given above lead to _semigroups_. In fact, following [34], (free)
_semigroups_ are the first mathematical objects every human being has to deal
with - even before attending school.

####  2.1.1 More about the theory of semigroups

A _semigroup_ is an algebraic structure consisting of a set with an
associative binary operation defined on it. In the history of mathematics,
_the algebraic theory of semigroups_ is a relative newcomer, with the theory
proper developing only in the second half of the twentieth century.
Historically, it can be viewed as an algebraic abstraction of the properties
of the composition of transformations on a set. But, there is no doubt about
it, the main sources came from group and ring theories. However, semigroups
are not a direct generalization of group theory as well as ring theory. Let us
remember: congruences on groups are uniquely determined by their normal
subgroups, and, on the other hand, there is a bijection between congruences
and the ideals of rings. The study of congruences on semigroups is more
complicated - no such device is available. One must study congruences as such.
Thus, semigroups do not much resemble groups and rings. In fact, semigroups do
not much resemble any other algebraic structure. Nowadays, semigroup theory is
an enormously broad topic and has advanced on a very broad front. Following
[37], “a huge variety of structures studied by mathematicians are sets endowed
with associative binary operation.” Even more, it appears that “semigroup
theory provides a convenient general framework for unifying and clarifying a
number of topics in fields that are seen, at first sight, unrelated”, [34].

The capability and flexibility of semigroups from the point of view of
modeling and problem-solving in extremely diverse situations have been already
pointed out, and interesting new algebraic ideas arise with binary
applications and connections to other areas of mathematics and sciences. Let
us start our short journey through the applications of semigroups with the
connections to the algebra of relations. The theory of semigroups is one of
the main algebraic tools used in the theory of automata as well as the theory
of formal languages. According to some authors, the role of the theory of
semigroups for theoretical computer science is compared with the one which the
philosophy has with the respect to science in general. Some investigations on
transformation semigroups of synchronizing automata show up interesting
implications for various applications for robotics, or more precisely, robotic
manipulation. On the other hand, areas such as biology, biochemistry,
sociology also make use of semigroups. For example, semigroups can be used in
biology to describe certain aspects in the crossing of organisms, in genetics,
and in consideration of metabolisms. Following [7], [35], the sociology
includes the study of human interactive behaviour in group situations, in
particular in underlying structures of societies. The study of such relations
can be elegantly formulated in the language of semigroups. The book [8] is
written for social scientists with the main aim to help readers to apply
“interesting and powerful concepts” of semigroup theory to their own fields of
expertise. However, the list of applications given above does not purport to
mention all of the existing applications of semigroup theory. As it is pointed
out in [37], it is often the case that “most applications make minimal use of
the reach of the (classical) algebraic theory of semigroups.” There is need
for study of some more structures of semigroups which can find applications in
different areas, [45]. This can bring very pretty mathematics to illustrate
the interplay between certain scientific areas and semigroup-theoretic
techniques. This type of research can be a topic on its own for certain types
of papers.

In what follows some known results from the classical semigroup theory useful
for our development will be presented.

_A semigroup_ $(S,\cdot)$ is a set $S$ together with an associative binary
operation $\cdot$

  * (A)

$\enspace\quad(\forall a,b,c\in S)\ [(a\cdot b)\cdot c\,=\,a\cdot(b\cdot c)]$.

Where the nature of the multiplications is clear from the context, it is
written $S$ rather than $(S,\,\cdot)$. Frequently, $xy$ is written rather than
$x\,\cdot\,y$.

Various approaches have been developed over the years to construct frameworks
for understanding the structure of semigroups. The fundamental concepts of
semigroup theory elaborated by Suschekewitsch, Rees, Green, Clifford and other
pioneers include as one of the main tools, _Green’s quasiorders_ (and
equivalences generated by them), defined by the multiplication of semigroups
and in terms of special subsemigroups. The notion of an order plays an
important role throughout mathematics as well as in some adjacent disciplines
such as logic and computer science. Order theory provides one of the most
basic tools of semigroup theory as well. In particular, the structure of
semigroups is usually most clearly revealed through the analysis of the
behaviour of their appropriate orders. A pure order theory is concerned with a
single undefined binary relation $\rho$. This relation is assumed to have
certain properties (such as, for example, reflexivity, transitivity, symmetry,
antisymmetry), the most basic of which leads to the concept of _quasiorder_. A
quasiorder plays a central role throughout this short exposition with the
fundamental concepts being introduced whenever possible in their natural
properties.

Distinguishing subsets

A number of subsets of a semigroup enjoy special properties relative to the
multiplication. A subset $T$ of a semigroup $S$ is:

  * •

_completely isolated_ if $ab\in T$ implies $a\in T$ or $b\in T$ for any
$a,b\in S$,

  * •

_convex_ if $ab\in T$ implies both $a,b\in T$ for any $a,b\in S$,

  * •

_subsemigroup_ if for any $a,b\in T$ we have $ab\in T$,

  * •

_ideal_ if for any $a\in T$ and $s\in S$ we have $as,sa\in T$.

A subsemigroup $T$ of $S$ which is convex (resp. completely isolated) as a
subset is called a _convex_ (resp. _completely isolated_) _subsemigroup_. In
an analogous way, we define a complex (completely isolated) ideal of $S$. Some
of their existing properties are listed in the lemma below.

###### Lemma 2.1

Let $S$ be a semigroup. Then:

  * _(i)_

An ideal $I$ of $S$ is completely isolated if and only if $\neg I=S\setminus
I$ is either a subsemigroup of $S$ or is empty.

  * _(ii)_

An nonempty subset $F$ of $S$ is convex if and only if $\neg F=S\setminus F$
is either a completely isolated ideal or is empty.

Within CLASS  semigroups can historically be viewed as an algebraic
abstraction of the transformations on a set. Of great importance is the role
of the subsemigroups given above in describing the structure of transformation
semigroups. We refer the reader to [22], [58] for more details about
definitions, properties and applications of such subsemigroups.

Describing a semigroup and its structure is a formidable task. There are many
different techniques developed for that purpose. _Semilattice decomposition of
semigroups_ is one of the methods with general applications. For more
information on semilattice decomposition of semigroups see [39], [43]. It is
shown in [43] that this method leads to the study of completely isolated
ideals and convex subsemigroups.

Quasiorders

By definition, a binary relation $\rho$ of set $S$ is a subset of $S\times S$.
To describe the relation defined on a semigroup $S$, we have to say which
order pairs belong to $\rho$. In other words, for any $a\in S$, we have to
know the following subsets of $S$:

$a\rho\,=\,\\{x\in S\,\mid\,(a,x)\in\rho\\}$,

$\rho a\,=\,\\{x\in S\,\mid\,(x,a)\in\rho\\}$,

called the left and right $\rho$-class of an element $a$. That is how we
connect a study of binary relations defined on a given set with its subsets.

The relations defined on a semigroup $S$ are distinguished one from another
according to the behaviour of their related elements to the multiplication. A
relation $\rho$ defined on a semigroup $S$ is

  * •

_positive_ if $(a,ab),(a,ba)\in\rho$, for any $a,b\in S$,

  * •

_with common multiply property_ , or, also called for short, with _cm-
property_ if $(a,c),(b,c)\in\rho$ implies $(ab,c)\in\rho$, for any $a,b,c\in
S$.

  * •

_with compatibility property_ if $(x,y),(u,v)\in\rho$ implies $(xu,yv)\in\rho$
for any $x,y,u,v\in S$.

In the sequel, the positive quasiorders will also be considered. Recall that
the _division relation_ $|$ on a semigroup $S$, defined by

$a\,|\,b\ \stackrel{{\scriptstyle\rm def}}{{\Leftrightarrow}}\ (\exists x,y\in
S^{1})\ b=xay,$

for $a,b\in S$, is the smallest positive quasi-order defined on $S$. The
positive quasi-orders were introduced in [56]. In [60] their link to
semilattice decompositions of semigroups was established. In [44] their
possible applications in psychology were announced. Finally, close connections
between positive quasiorders and subsemigroups defined above were given in
[6]. Here we mention some of these results:

###### Theorem 2.1

Let $\rho$ be a quasiorder on $S$. The following conditions on a semigroup $S$
are equivalent:

  * _(i)_

$\rho$ is a positive quasiorder;

  * _(ii)_

$(\forall a,b\in S)\,(ab)\rho\subseteq a\rho\cap b\rho$;

  * _(iii)_

$(\forall a,b\in S)\,\rho a\cup\rho b\subseteq\rho(ab)$;

  * _(iv)_

$a\rho$ is an ideal for any $a\in S$;

  * _(v)_

$\rho a$ is a convex subset of $S$ for any $a\in S$.

###### Theorem 2.2

Let $\rho$ be a quasiorder on $S$. The following conditions on a semigroup $S$
are equivalent:

  * _(i)_

$\rho$ is a positive quasiorder with cm-property;

  * _(ii)_

$\rho a$ is a convex subsemigroup of $S$ for any $a\in S$;

  * _(iii)_

$(\forall a,b\in S)\,(ab)\rho=a\rho\cap b\rho$.

Finally, we can say that, from the point of view of the classical semigroup
theory, the interrelations between the following notions are of interest:

  * •

semilattice decomposition of semigroups,

  * •

completely isolated and convex subsemigroups and/or ideals,

  * •

positive quasiorders.

Isomorphism theorems for semigroups

Let us remember that congruences on groups are uniquely determined by their
normal subgroups, and, on the other hand, there is a bijection between
congruences and the ideals of rings. The study of congruences on semigroups is
more complicated - no such device is available. One must study congruences as
such. A _congruence_ $\rho$ on a semigroup $S$ is an equivalence, i.e.
symmetric quasiorder, with the _compatibility property_. Classically, the
quotient set $S/\rho$ is then provided with a semigroup structure.

###### Theorem 2.3

Let $S$ be a semigroup and $\rho$ a congruence on it.Then $S/\rho$ is a
semigroup with respect to the operation defined by $(x\rho)(y\rho)=(xy)\rho$,
and the mapping $\pi\,:\,S\,\rightarrow\,S/\rho$, $\pi(x)=x\rho$, $x\in S$, is
an _onto_ homomorphism.

Provided that the (_first_) _isomorphism theorem for semigroups_ follows.

###### Theorem 2.4

Let $f:S\rightarrow T$ be a homomorphism between semigroups $S$ and $T$. Then

  * _(i)_

$ker\,f=f\circ f^{-1}=\\{(x,y)\in S\times S\,:\,f(x)=f(y)\\}$ is a congruence
on $S$;

  * _(ii)_

the mapping $\theta\,:\,S/ker\,f\,\rightarrow\,T$ defined by
$\theta(x(ker\,f))=f(x)$ is an embedding such that $f=\theta\circ\pi$;

  * _(iii)_

if $f$ maps $S$ onto $T$, then $\theta$ is an isomorphism.

The theorem which follows is concerned with a more general situation.

###### Theorem 2.5

Let $\rho$ be a congruence on a semigroup $S$, and let $f:S\rightarrow T$ be a
homomorphism between semigroups $S$ and $T$ such that $\rho\subseteq ker\,f$.
Then there exists a homomorphism of semigroups $\theta:S/\rho\rightarrow T$,
such that $f=\theta\circ\pi$. If, in addition, $f$ is _onto_ , then $\theta$
is an isomorphism.

###  2.2 Constructive algebra

Constructive algebra is a relatively old discipline developed among others by
L. Kronecker, van der Waerden, A. Heyting. For more information on the history
see [38], [61]. One of the main topics in constructive algebra is constructive
algebraic structures with the relation of (tight) apartness $\\#$, the second
most important relation in constructive mathematics. The principal novelty in
treating basic algebraic structures constructively is that (tight) apartness
becomes a fundamental notion. (Consider the reals: we cannot assert that
$x^{-1}$ exists unless we know that $x$ is apart from zero, i.e. $|x|>0$ \-
constructively that is not the same thing as $x\neq 0$. Furthermore, in fields
$x^{-1}$ exists only if $x$ is apart from 0, [3]) The study of algebraic
structures in the presence of _tight_ apartness was started by Heyting, [27].
Heyting gave the theory a firm base in [29]. Roughly, the descriptive
definition of a structure with apartness includes two main parts:

  * •

the notion of a certain classical algebraic structure is straightforwardly
adopted;

  * •

a structure is equipped with an apartness with standard operations respecting
that apartness.

Quotient structures are not part of BISH. A quotient structure does not, in
general, have a natural apartness relation. So, _the Quotient Structure
Problem_ \- QSP is one of the very first problems which has to be considered
for any structure with apartness. Talking about the QSP for sets and
semigroups with apartness and its history - solution of the QSP for sets with
apartness is for the first time given in [17]. The QSP’s solutions for groups
with _tight_ apartness and commutative rings with _tight_ apartness presented
in [3], [19], [46], [48], [49], [54], [61] inspired us to give solutions of
QSP for _sets with apartness_ in 2013, [17], which, in turn, imply the
solution of QSP for semigroups with apartness as its consequence.

A lot of ideas, notions and notations come from, for example, the constructive
analysis, and, especially, from the constructive topology, as well as from
constructive theories of groups and rings with _tight_ apartness. Although the
area of constuctive semigroups with apartness is still in its infancy, we can
already conclude that, similarly to the clasical case, the semigroups with
apartness do not much resemble groups and rings. In fact, they do not much
resemble any other constructive algebraic structures with apartness.

###  2.3 Computer science

It is well known that formalization is a general method in science. Although
it was created as a technique in logic and mathematics, it has entered into
engineering as well. Formal engineering methods can be understood as
mathematically-based techniques for the functional specification, development
and verification in the engineering of software and hardware systems. Despite
some initial suspicion, it was proved that formal methods are powerful enough
to deal with real life systems. For example, it is shown that “software of the
size and complexity as we find in modern cars today can be formally specified
and verified by applying computer based tools for modeling and interactive
theorem proving,” [15].

Proof assistants are computer systems which give a user the possibility to do
mathematics on a computer: from (numerical and symbolical) computing aspects
to the aspects of defining and proving. The latter ones, doing proofs, are the
main focus. It is believed that, besides their great future within the area of
mathematics formalization, their applications within computer-aided modelling
and verification of the systems are and will be more important. One of the
most popular, with the intuitionistic background, is the proof assistant
computer system _Coq_.

Coq is used for formal proves of well known mathematical theorems, such as,
for example, the Fundamental Theorem of Algebra, FTA, [24]. For that purpose,
the _constructive algebraic hierarchy_ for Coq was developed, [25], consisting
of constructive basic algebraic structures (semigroups, monoids, groups,
rings, fields) with _tight_ apartness. In addition, all these structures are
limited to the commutative case. As it is noticed in [25] “that algebraic
hierarchy has been designed to prove FTA. This means that it is not rich as
one would like. For instance, we do not have noncommutative structure because
they did not occur in our work.” … So, a question which arises from this is:

> _What can be done in connection with noncommutative semigroups with
> apartness where apartness is only “ordinary” and not the tight one?_

We put noncommutative constructive semigroups with “ordinary” apartness in the
core of our study, proving first, of course, that such semigroups do exist,
[17]. As in [5], we made “every effort to follow classical development along
the lines suggested by familiar classical theories or in all together new
directions.”

The results of our several years long investigations, [17], [18], [41],
present a semigroup facet of some relatively well established directions of
constructive mathematics which, to the best of our knowledge, have not yet
been considered within the semigroup community. The initial step towards
grounding the theory done through our papers will be developed through the
scope of this paper. We are going to give a critical review of some of those
results as well as the solutions to some of the open problems arising from
those papers.

##  3 Main results: sets and semigoups with apartness

Before starting our constructive examination of sets and semigroups with
apartness, we should clarify its setting. By constructive mathematics we mean
Bishop-style mathematics, BISH. We adopt Fred Richman’s viewpoint, [47], where
constructive mathematics is simply mathematics carried out with intuitionistic
logic. The Bishop-style of constructive mathematics enables one to interpret
the results both in classical mathematics, CLASS, and other varieties of
constructivism. We regard classical mathematics as Bishop-style mathematics
plus the law of excluded middle, LEM. This logical principle can be regarded
as the main source of nonconstructivity. It was Brouwer, [14], who first
observed that LEM was extended without justification to statements about
infinite sets. Several consequences of LEM are not accepted in Bishop’s
constructivism. We will mention three such nonconstructive principles - the
ones which will be used latter.

  * •

The limited principle of omniscience, LPO: for each binary sequence
$\left(a_{n}\right)_{n\geq 1}$, either $a_{n}=0$ for all $n\in\mathbb{N}$, or
else there exists $n$ with $a_{n}=1$.

  * •

The lesser limited principle of omniscience, LLPO: if
$(a_{n})_{n\in\mathbb{N}}$ is a binary sequence containing at most one term
equal to 1, then either $a_{2n}=0$ for all $n\in\mathbb{N}$, or else
$a_{2n+1}=0$ for all $n\in\mathbb{N}$.

  * •

Markov’s principle, MP: For each binary sequence $\left(a_{n}\right)_{n\geq
1}$, if it is impossible that $a_{n}=0$ for all $n\in\mathbb{N}$, then there
exists $n$ with $a_{n}=1$.

###### Remark 2

LPO is equivalent to the decidability of equality on the real number line
$\mathbb{R}$.

$\forall_{x\in\mathbb{R}}\,(x=0\vee x\neq 0).$

A detailed constructive study of $\mathbb{R}$ can be found in [10].

Within constructive mathematics, a statement $P$, as in classical mathematics,
can be disproved by giving a counterexample. However, it is also possible to
give a _Brouwerian counterexample_ to show that the statement is
nonconstructive. A Brouwerian counterexample to a statement $P$ is a
constructive proof that $P$ implies some nonconstructive principle, such as,
for example, LEM, and its weaker versions LPO, LLPO, MP. It is not a
counterexample in the true sense of the word - it is just an indication that
$P$ does not admit a constructive proof. More details about nonconstructive
principles and various classical theorems that are not constructively valid
can be found in [31].

###  3.1 Set with apartness

The cornerstones for BISH include the notion of positive integers, sets and
functions. The set $\mathbb{N}$ of positive numbers is regarded as a basic
set, and it is assumed that the positive numbers have the usual algebraic and
order properties, including mathematical induction.

Contrary to the classical case, a set exists only when it is defined. To
define a set $S$, we have to give a property that enables us to construct
members of $S$, and to describe the equality $=$ between elements of $S$ –
which is a matter of convention, except that it must be an equivalence. A set
$(S,=)$ is an _inhabited_ set if we can construct an element of $S$. The
distinction between the notions of a nonempty set and an inhabited set is a
key in constructive set theories. The notion of equality of different sets is
not defined. The only way in which elements of two different sets can be
regarded as equal is by requiring them to be subsets of a third set. For this
reason, the operations of union and intersection are defined only for sets
which are given as subsets of a given set. There is another problem to face
when we consider families of sets that are closed under a suitable operation
of complementation. Following [5] “we do not wish to define complementation in
the terms of negation; but on the other hand, this seems to be the only method
available. The way out of this awkward position is to have a very flexible
notion based on the concept of _a set with apartness_.”

A property $P$, which is applicable to the elements of a set $S$, determines a
subset of $S$ denoted by $\\{x\in S:P(x)\\}$. Furthermore, we will be
interested only in properties $P(x)$ which are _extensional_ in the sense that
for all $x_{1},x_{2}\in S$ with $x_{1}=x_{2}$, $P(x_{1})$ and $P(x_{2})$ are
equivalent. Informally, it means that “it does not depend on the particular
description by which $x$ is given to us”, [13].

An inhabited subset of $S\times S$, or, equivalently, a property applicable to
elements of $S\times S$, is called a _binary relation_ on $S$. In general,
there are many properties that binary relations may satisfy on a given set.
For instance, reflexivity, symmetry, transitivity, irreflexivity, strong
irreflexivity, co-transitivity play a role under constructive rules.

In CLASS, equivalence is the natural generalization of equality. A theory with
equivalence involves equivalence and functions, and relations respecting this
equivalence. In constructive mathematics the same works without difficulty,
[55].

Many sets come with a binary relation called inequality satisfying certain
properties, and denoted by $\neq$, $\\#$ or $\not\backsimeq$. In general, more
computational information is required to distinguish elements of a set $S$,
than to show that elements are equal. Comparing with CLASS, the situation for
inequality is more complicated. There are different types of inequalities
(denial inequality, diversity, apartness, tight apartness - to mention a few),
some of them completely independent, which only in CLASS are equal to one
standard inequality. So, in CLASS the study of the equivalence relation
suffices, but in constructive mathematics, an inequality becomes a “basic
notion in intuitionistic axiomatics”. Apartness, as a positive version of
inequality, “is yet another fundamental notion developed in intuitionism which
shows up in computer science,” [32].

Let $(S,=)$ be an _inhabited_ set. By an _apartness_ on $S$ we mean a binary
relation $\\#$ on $S$ which satisfies the axioms of irreflexivity, symmetry
and cotransitivity:

  * (Ap1)

$\neg(x\\#x)$

  * (Ap2)

$x\\#y\ \Rightarrow\ y\\#x$,

  * (Ap3)

$x\\#z\ \Rightarrow\ \forall_{y}\,(x\\#y\,\vee\,y\\#z).$

If $x\\#y$, then $x$ and $y$ are different, or distinct. Roughly speaking,
$x=y$ means that we have a proof that $x$ equals $y$ while $x\\#y$ means that
we have a proof that $x$ and $y$ are different. Therefore, the negation of
$x=y$ does not necessarily imply that $x\\#y$ and vice versa: given $x$ and
$y$, we may have neither a proof that $x=y$ nor a proof that $x\\#y$.

The negation of apartness is an equivalence
$(\approx)\stackrel{{\scriptstyle\text{d}ef}}{{=}}(\neg\,\\#)\,$ called _weak
equality_ on $S$.

###### Remark 3

The statement that every equivalence relation is the negation of some
apartness relation is equivalent to the excluded middle. The statement that
the negation of an equivalence relation is always an apartness relation is
equivalent to the nonconstructive de Morgan law.

The apartness on a set $S$ is _tight_ if

  * (Ap4)

$\neg(x\\#y)\ \Rightarrow\ x=y$.

Apartness is tight just when $\approx$ and $=$ are the same, that is
$\neg(x\\#y)\ \Leftrightarrow\ x=y$.

In some books and papers, such as [61], the term “preapartness” is used for an
apartness relation, while “apartness” means tight apartness. The tight
apartness on the real numbers was introduced by L. E. J. Brouwer in the early
1920s. Brouwer introduced the notion of apartness as a positive intuitionistic
basic concept. A formal treatment of apartness relations began with A.
Heyting’s formalization of elementary intuitionistic geometry in [28]. The
intuitionistic axiomatization of apartness is given in [30].

By extensionality, we have

  * (Ap5)

$x\\#y\,\wedge\,y=z\ \Rightarrow\,x\\#z$,

the equivalent form of which is

  * (Ap5’)

$x\\#y\,\wedge\,x=x^{\prime}\,\wedge\,y=y^{\prime}\
\Rightarrow\,x^{\prime}\\#y^{\prime}$.

A _set with apartness_ $(S,=,\\#)$ is the starting point for our
considerations, and will be simply denoted by $S$. The existence of an
apartness relation on a structure often gives rise to an apartness relation on
another structure. For example, given two sets with apartness
$(S,=_{S},\\#_{S})$ and $(T,=_{T},\\#_{T})$, it is permissible to construct
the set of mappings between them. Following [13], _a mapping_ $f:S\rightarrow
T$ is an algorithm which produces an element $f(x)$ of $T$ when applied to an
element $x$ of $S$, which is extensional, that is

$\forall_{x,y\in S}\,(x=_{S}y\ \Rightarrow\ f(x)=_{T}f(y)).\mathbf{\ }$

A mapping $f:S\rightarrow T$ is:

\- _onto_ $S$ or _surjection_ : $\forall_{y\in T}\ \exists_{x\in S}\
(y=_{T}f(x))$;

\- _one-one_ or _injection_ : $\forall_{x,y\in S}\,(f(x)=_{T}f(y)\
\Rightarrow\ x=_{S}y)$;

\- _bijection_ between $S$ and $T$: it is a one-one and onto.

An important property applicable to mapping $f$ is that of strong
extensionality. Namely, a mapping $f:S\rightarrow T$ is a _strongly
extensional_ mapping, or, for short, an _se-mapping_ , if

$\forall_{x,y\in S}\,(f(x)\\#_{T}f(y)\ \Rightarrow\ x\\#_{S}y).$

(The strong extensionality of all mappings from $\mathbb{R}$ to $\mathbb{R}$
implies Markov principle, MP, see [13].)

Furthermore, $f$ is

\- _apartness injective_ , shortly _a-injective_ : $\forall_{x,y\in
S}\,(x\\#_{S}y\ \Rightarrow\ f(x)\\#_{T}f(y))$;

\- _apartness bijective_ : a-injective, se-bijective.

Given two sets with apartness $S$ and $T$ it is permissible to construct the
set of ordered pairs $(S\times T,=,\\#)$ of these sets defining apartness by

$(s,t)\,\\#\,(u,v)\enspace\stackrel{{\scriptstyle\rm
def}}{{\Leftrightarrow}}\enspace s\,\\#_{S}\,u\,\vee\,t\,\\#_{T}\,v.$

####  3.1.1 Distinguishing subsets

The presence of apartness implies the appearance of different types of
substructures connected to it. Inspired by the constructive topology with
apartness [13], we define the relation $\bowtie$ between an element $x\in S$
and a subset $Y$ of $S$ by

$x\bowtie Y\ \stackrel{{\scriptstyle\rm def}}{{\Leftrightarrow}}\
\forall_{y\in Y}(x\\#y).$

A subset $Y$ of $S$ has two natural complementary subsets: _the logical
complement_ of $Y$

${\neg Y}\stackrel{{\scriptstyle\rm def}}{{=}}\\{x\in S:x\notin Y\\},$

and _the apartness complement_ or, shortly, the _a-complement_ of $Y$

${\sim Y}\,\stackrel{{\scriptstyle\rm def}}{{=}}\,\\{x\in S\,:\,x\bowtie
Y\\}.$

Denote by $\widetilde{x}$ the a-complement of the singleton $\\{x\\}$. Then it
can be easily shown that $x\in\sim Y$ if and only if
$Y\subseteq\widetilde{x}.$

If the apartness is not tight we can find subsets $Y$ with ${\sim
Y}\subset{\neg Y}$ as in the following example.

###### Example 1

Let $S=\\{a,b,c\\}$ be a set with apartness defined by
$\\{(a,c),(c,a),(b,c),(c,b)\\}$ and let $Y=\\{a\\}$. Then the a-complement
$\sim\\!\,Y=\\{c\\}$ is a proper subset of its logical complement $\neg
Y=\\{b,c\\}$.

For a tight apartness, the two complements are constructive counterparts of
the classical complement. In general, we have ${\sim Y}\subseteq{\neg Y}.$
However, even for a tight apartness, the converse inclusion entails the Markov
principle, MP. This result illustrates a main feature of constructive
mathematics: classically equivalent notions could be no longer equivalent
constructively. For which type of subset of a set with apartness do we have
equality between its two complements? It turns out that the answer initiated a
development of _order theory_ for sets and semigroups with apartness

The complements are used for the classification of subsets of a given set. A
subset $Y$ of $S$ is

  * •

_a detachable_ subset in $S$ or, in short, a _d-subset_ in $S$ if

$\forall_{x\in S}\,(x\in Y\vee x\in{\neg}Y);$

  * •

_a strongly detachable_ subset of $S$, shortly _an sd-subset of_ $S$, if

$\forall_{x\in S}\,(x\in Y\vee x\in{\sim}Y),$

  * •

_a quasi-detachable_ subset of $S$, shortly _a qd-subset of_ $S$, if

$\forall_{x\in S}\,\forall_{y\in Y}\,(x\in Y\vee x\\#y).$

The relations between detachable, strongly detachable and quasi-detachable
subsets are partially described in [41], Proposition 2.1. A description of the
relationships between those subsets of set with apartness, which, in turn,
justifies the constructive order theory for sets and semigroups with apartness
we develop, is given in the next theorem which is one of the main results of
this paper.

###### Theorem 3.1

Let $Y$ be a subset of $S$. Then:

  * _(i)_

Any sd-subset is a qd-subset of $S$. The converse implication entails LPO .

  * _(ii)_

Any qd-subset $Y$ of $S$ satisfies ${\sim Y}={\neg Y}$.

  * _(iii)_

If any qd-subset is a d-subset, then LPO holds.

  * _(iv)_

If any d-subset is a qd-subset, then MP holds.

  * _(v)_

Any sd-subset is a d-subset of $S$. The converse implication entails MP.

  * _(vi)_

If any subset of a set with apartness $S$ is a qd-subset, then LPO holds.

###### Proof.

(i). Let $Y$ be an sd-subset of $S$. Then, applying the definition and logical
axiom we have

$\displaystyle\forall_{x\in S}\,(x\in Y\vee x\in{\sim}Y)\ $
$\displaystyle\Leftrightarrow\ $ $\displaystyle\forall_{x\in S}\,(x\in
Y\,\vee\,\forall_{y\in Y}(x\\#y))$ $\displaystyle\Rightarrow$
$\displaystyle\forall_{x\in S}\,\forall_{y\in Y}\,(x\in Y\vee x\\#y).$

In order to prove the second part of this statement, we consider the real
number set $\mathbb{R}$ with the usual (tight) apartness and the subset
$Y=\widetilde{0}.$ Then, for each real number $x$ and for each $y\in Y$ it
follows, from the co-transitivity of $\\#$, either $y\\#x$ or $x\\#0$, that
is, either $x\in Y$ or $x\\#y$. Consequently, $Y$ is a qd-subset of
$\mathbb{R}.$ On the other hand, if $Y$ is an sd-subset of $\mathbb{R},$ then
for each $x\in\mathbb{R}$, either $x\in Y$ or $x\in\sim Y.$ In the former
case, $x\\#0$ and in the latter $x=0$, hence LPO holds.

(ii). Let $Y$ be a qd-subset, and let $a\in\neg Y$. By assumption we have

$\forall_{x\in S}\,\forall_{y\in Y}\,(x\in Y\vee x\\#y),$

so substituting $a$ for $x$, we get $\forall_{y\in Y}\,(a\in Y\vee a\\#y)$,
and since, by assumption, $\neg(a\in Y)$, it follows that $a\\#y$ for all
$y\in Y$. Hence $a\in\sim Y$. See also [41].

(iii). Let $S$ be the real number set $\mathbb{R}$ with the usual apartness
$\\#$. As in the proof of (i), consider the qd-subset $\widetilde{0}$ of
$\mathbb{R}$. If $\widetilde{0}$ is a d-subset of $\mathbb{R}$, then
$x\in\widetilde{0}$ or $\neg(x\in\widetilde{0})$, for all real numbers $x$. In
the latter case $\neg(x\\#0)$, which is equivalent to $x=0.$ Thus we obtain
the property $\forall_{x\in\mathbb{R}}\;(x\\#0\vee x=0)$ which, in turn, is
equivalent to LPO.

(iv). Consider a real number $a$ with $\neg(a=0)$ and let $S$ be the set
$\\{0,a\\}$ endowed with the usual apartness of $\mathbb{R}$. For $Y=\\{0\\}$,
since $0\in Y$ and $a\in\neg Y,$ it follows that $Y$ is a d-subset of $S$. On
the other hand, if $Y$ is a qd-subset of $S$, then $a\\#0$. It follows that
for any real number with $\neg(a=0)$, $a\\#0$ which entails the Markov
Principle, MP.

(v). The first part follows immediately from (i), (ii) and the definition of
d-subsets. The converse follows from (i) and (iv).

(vi). Consider again $\mathbb{R}$ with the usual apartness and define
$Y=\\{0\\}.$ If $Y$ is a qd-subset of $\mathbb{R}$, then for all
$x\in\mathbb{R}$ we have $x=0$ or $x\\#0$, hence LPO holds. ∎

If the apartness is not tight, we can find subsets which are not qd-subsets,
let alone sd-subsets. To show this, let us consider the set $S=\\{a,b,c\\}$
with the apartness defined in Example 1 and define $Y=\\{a\\}.$ Then $Y$ is
not a qd-subset of $S$. If we work with a tight apartness, although vacuously
true in classical mathematics, the properties of detachability are not
automatically satisfied in BISH. The Brouwerian examples from Theorem 3.1
motivate the use of qd-subsets. Constructive mathematics brings to the light
some notions which are invisible to the classical eye (here, the three notions
of detachability).

####  3.1.2 Co-quasiorders

Let $(S\times S,=,\\#)$ be a set with apartness. An inhabited subset of
$S\times S$, or, equivalently, a property applicable to the elements of
$S\times S$, is called a _binary relation_ on $S$. Let $\alpha$ be a relation
on $S$. Then

$(a,b)\ \bowtie\ \alpha\ \Leftrightarrow\ \forall_{(x,y)\in\alpha}\
((a,b)\,\\#\,(x,y)),$

for any $(a,b)\in S\times S$. The apartness complement of $\alpha$ is the
relation

$\mathbf{\sim\alpha}\,=\,\\{(x,y)\in S\times S:(x,y)\bowtie\alpha\\}.$

In general, we have $\sim\alpha\subseteq\neg\alpha$, which is shown by the
following example.

###### Example 2

Let $S=\\{a,b,c\\}$ be a set with apartness defined by
$\\{(a,c),(c,a),(b,c),(c,b)\\}$. Let $\alpha=\\{(a,c),(c,a)\\}$ be a relation
on $S$. Its a-complement

$\sim\\!\,\alpha=\\{(a,a),(b,b),(c,c),(a,b),(b,a)\\}$

is a proper subset of its logical complement $\neg\alpha$.

The relation $\alpha$ defined on a set with apartness $S$ is

  * •

irreflexive if $\forall_{x\in S}\,\neg((x,x)\in\alpha)$;

  * •

strongly irreflexive if $(x,y)\in\alpha\ \Rightarrow\ x\\#y$;

  * •

co-transitive if $(x,y)\in\alpha\ \Rightarrow\ \forall_{z\in
S}\,((x,z)\in\alpha\,\vee\,(z,y)\in\alpha).$

It is easy to check that a strongly irreflexive relation is also irreflexive.
For a tight apartness, the two notions of irreflexivity are classically
equivalent but not so constructively. More precisely, if each irreflexive
relation were strongly irreflexive then MP would hold.

In the constructive order theory, the notion of co-transitivity, that is the
property that for every pair of related elements, any other element is related
to one of the original elements in the same order as the original pair is a
constructive counterpart to classical transitivity, [17].

###### Lemma 3.1

Let $\alpha$ be a relation on $S$. Then:

  1. _(i)_

$\alpha$ is strongly irreflexive if and only if $\sim\\!\,\alpha$ is
reflexive;

  2. _(ii)_

if $\alpha$ is reflexive then $\sim\\!\,\alpha$ is strongly irreflexive;

  3. _(iii)_

if $\alpha$ is symmetric then $\sim\\!\,\alpha$ is symmetric;

  4. _(iv)_

if $\alpha$ is co-transitive then $\sim\\!\,\alpha$ is transitive.

###### Proof.

(i). Let $\alpha$ be a strongly irreflexive relation on $S$. For each $a\in
S$, it can be easily proved that $(a,a)\\#(x,y)$ for all $(x,y)\in\alpha$.

Let $\sim\\!\,\alpha$ be reflexive, that is $(x,x)\in\sim\\!\,\alpha$, for any
$x\in S$. On the other hand, the definition of the a-complement implies
$(x,y)\\#(x,x)$ for any $(x,y)\in\alpha$. So, $x\\#x$ or $x\\#y$. Thus,
$x\\#y$, that is, $\alpha$ is strongly irreflexive.

(ii). Let $\alpha$ be reflexive. Let $(x,y)$ be an element of $\sim\alpha$.
Since $\alpha$ is reflexive, $(y,y)\in\alpha$ hence $(x,y)\\#(y,y)$ which
implies $x\\#y.$ Consequently, $\sim\alpha$ is strongly irreflexive.

(iii). If $\alpha$ is symmetric, then

$\displaystyle(x,y)\in\sim\\!\,\alpha\ $ $\displaystyle\Leftrightarrow$
$\displaystyle\ \forall_{(a,b)\in\alpha}\,((x,y)\\#(a,b))$
$\displaystyle\Rightarrow$ $\displaystyle\
\forall_{(b,a)\in\alpha}\,((x,y)\\#(b,a))$ $\displaystyle\Rightarrow$
$\displaystyle\ \forall_{(b,a)\in\alpha}\,(x\\#b\ \vee\ y\\#a)$
$\displaystyle\Rightarrow$ $\displaystyle\
\forall_{(a,b)\in\alpha}\,((y,x)\\#(a,b))$ $\displaystyle\Leftrightarrow$
$\displaystyle\ (y,x)\in\sim\\!\,\alpha.$

(iv). If $(x,y)\in\sim\alpha$ and $(y,z)\in\sim\alpha$, then, by the
definition of $\sim\alpha$, we have that $(x,y)\bowtie\alpha$ and
$(y,z)\bowtie\alpha$. For an element $(a,b)\in\alpha$, by co-transitivity of
$\alpha$, we have $(a,x)\in\alpha$ or $(x,y)\in\alpha$ or $(y,z)\in\alpha$ or
$(z,b)\in\alpha$. Thus $(a,x)\in\alpha$ or $(z,b)\in\alpha$, which implies
that $a\\#x$ or $b\\#z$, that is $(x,z)\\#(a,b)$. So, $(x,z)\bowtie\alpha$ and
$(x,z)\in\ \sim\alpha$. Therefore, $\sim\alpha$ is transitive. ∎

###### Remark 4

As it is shown in Lemma 3.1, it can be proved that the logical complement of
each co-transitive relation is transitive. However, if the logical complement
of any transitive relation were co-transitive, then LLPO would hold.

To prove this, let us consider the strict order $<$ on the real number line
and assume that its logical complement $\geq$ is cotransitive. Then, taking
into account that $x\geq x$, it follows that

$\forall x\in{\bf R}\;(x\geq 0\vee 0\geq x)$

which, in turn, is equivalent to LLPO. This Brouwerian example can be found in
books on constructive mathematics, see, for example, [13].

The apartness complement $\sim\alpha$ of a relation $\alpha$ of $S$ can be
transitive without assuming co-transitivity of $\alpha$. So, the converse
statement from Lemma 3.1(iv), in general, is not true.

###### Example 3

Let $(S,=,\\#)$ be a set with apartness defined in Example 2.

(1.) A strongly irreflexive (symmetric) relation $\alpha=\\{(a,c),(c,a)\\}$,
which is not co-transitive has the a-complement

$\sim\alpha=\\{(a,a),(b,b),(c,c),(a,b),(b,a)\\}$

which is transitive.

(2.) A strongly irreflexive (nonsymmetric) relation
$\alpha=\\{(a,c),(c,a),(b,c)\\}$, which is not co-transitive, has the
a-complement

$\sim\alpha=\\{(a,a),(b,b),(c,c),(a,b),(b,a)\\}$

which is transitive.

###### Remark 5

The Brouwerian example from Remark 4 also shows that, even for a tight
apartness, a relation whose co-transitivity cannot be proved constructively
might have a transitive a-complement. To prove this, we need only observe that
the a-complement of the relation $\geq$ is $<$.

A relation $\tau$ defined on a set with apartness $S$ is a

  * •

_weak co-quasiorder_ if it is irreflexive and co-transitive,

  * •

_co-quasiorder_ if it is strongly irreflexive and co-transitive.

###### Remark 6

“One might expect that the splitting of notions leads to an enormous
proliferation of results in the various parts of constructive mathematics when
compared with their classical counterparts. In particular, usually only very
few constructive versions of a classical notion are worth developing since
other variants do not lead to a mathematically satisfactory theory,” [61].

Even if the two classically (but not constructively) equivalent variants of a
co-quasiorder are constructive counterparts of a quasiorder in the case of (a
tight) apartness, the stronger variant, co-quasiorder, is, of course, the most
appropriate for a constructive development of the theory of semigroups with
apartness we develop, which will be evident in the continuation of this paper.
The weaker variant, that is, weak co-quasiorder, could be relevant in
analysis.

As in Example 2 the a-complement of a relation can be a proper subset of its
logical complement. If the relation in question is a co-quasiorder, then we
have the following important properties.

###### Proposition 3.1

Let $\tau$ be a co-quasiorder on $S$. Then:

  * _(i)_

$\tau$ is a qd-subset of $S\times S$;

  * _(ii)_

$\sim\\!\,\tau=\neg\,\tau$.

###### Proof.

(i). Let $(x,y)\in S\times S$. Then, for all $(a,b)\in\tau$,

$\displaystyle a\tau x\vee x\tau b$ $\displaystyle\ \Rightarrow\ $
$\displaystyle a\tau x\vee x\tau y\vee y\tau b$ $\displaystyle\ \Rightarrow\ $
$\displaystyle a\\#x\vee x\tau y\vee y\\#b$ $\displaystyle\ \Rightarrow\ $
$\displaystyle(a,b)\\#(x,y)\vee x\tau y,$

that is, $\tau$ is a qd-subset.

(ii). It follows from (i) and Theorem 3.1(ii). ∎

See also [41].

The co-quasiorder is one of the main building blocks for the order theory of
semigroups with apartness we develop.

In general, to describe the relation we have to determine which ordered pairs
belong to $\tau$, that is, we have to determine $a\tau$ and $\tau a$, the left
and the right $\tau$-class of each element $a$ from $S$. That is the way to
connect (in CLASS and in BISH as well) a relation defined on a given set with
certain subsets of the set. Starting from an sd-subset $T$ of $S$, we are able
to construct co-quasiorders as follows.

###### Lemma 3.2

Let $T$ be an sd-subset of a set with apartness $S$. Then, the relation $\tau$
on $S$, defined by

$(a,b)\in\tau\ \stackrel{{\scriptstyle\rm def}}{{\Leftrightarrow}}\ a\in\sim
T\,\wedge\,b\in T,$

is a co-quasiorder on $S$.

###### Proof.

Let $(a,b)\in\tau$, that is $a\in\sim T$ and $b\in T$, and let $x\in S$. By
the assumption, $T$ is an sd-subset, so we have $x\in T$ or $x\in\sim T$. If
$x\in T$, then, by the definition of $\tau$, we have $(a,x)\in\tau$.
Similarly, if $x\in\sim T$, then $(x,b)\in\tau$. Thus, co-transitivity of
$\tau$ is proved. By the definition of $\tau$, the strong irreflexivity
follows immediately. Thus, $\tau$ is a co-quasiorder on $S$. ∎

###### Example 4

Let $S=\\{a,b,c,d,e\\}$ be a set with the diagonal

$\triangle_{S}=\\{(a,a),(b,b),(c,c),(d,d),(e,e)\\}$

as the equality relation. If we denote by $K$ the set
$\triangle_{S}\cup\\{(a,b),(b,a)\\}$, then we can define an apartness $\\#\,$
on $S$ to be $(S\times S)\setminus K$. Thus, $(S,=,\\#\,)$ is a set with
apartness. The relation $\tau\subseteq S\times S$, defined by

$\tau=\\{(c,a),(c,b),(d,a),(d,b),(d,c),(e,a),(e,b),(e,c),(e,d)\\},$

is a co-quasiorder on $S$. (Left) $\tau$-classes of $S$ are:
$a\tau=b\tau=\emptyset$, $c\tau=\\{a,b\\}$, $d\tau=\\{a,b,c\\}$,
$e\tau=\\{a,b,c,d\\}$. It can be easily checked that all those $\tau$-classes
are sd-subsets of $S$.

Generally speaking, for a co-quasiorder defined on a set with apartness we can
not prove that its left and/or right classes are d-subsets or sd-subsets. More
precisely, we can prove the following result.

###### Proposition 3.2

Let $\tau$ be a co-quasiorder. Then:

  * _(i)_

if $a\tau$ is a d-subset of $S$ for any $a\in S$, then LPO holds;

  * _(ii)_

if $a\tau$ is an sd-subset of $S$ for any $a\in S$, then LPO holds.

###### Proof.

(i). Similar to the proof of Theorem 3.1(iii). It suffices to let $\tau$ be
the usual apartness on the real number set and $a=0.$

(ii). We can use the same example as above and apply Theorem 3.1(i). ∎

Having in mind what is just proved, we cannot expect to prove Lemma 3.2 from
[18], as stated in [18], with d-subsets or sd-subsets without the Constant
Domain Axiom, CDA.

####  3.1.3 Intuitionistic logic of constant domains CD as a background

Following [1], the intuitionistic logic of constant domains CD  arises from a
very natural Kripke-style semantics, which was proposed in [23] as a
philosophically plausible interpretation of intuitionistic logic. CD can be
formalized as intuitionistic logic extended with from the classical algebra
point of view pretty strong principle, the Constant Domain Axiom, CDA,

$\Vdash\forall_{x}\,(P\vee R(x))\,\rightarrow\ (P\vee\forall_{x}\,R(x)),$

where $x$ is not a free variable of $P$. The intermediate logic obtained in
this way, as it is pointed out in [1], further proves intuitionistically as
well as classically valid theorems, yet they often possess a strong
constructive flavour.

From a given co-quasiorder $\tau$, with CD as a logical background, we are
able to prove the connection of its classes with sd-subsets of $S$.

###### Lemma 3.3

Let $\tau$ be a co-quasiorder on a set $S$. Then $a\tau$ (respectively $\tau
a$) is an sd-subset of $S$, such that $a\bowtie a\tau$ (respectively
$a\bowtie\tau a$), for any $a\in S$. Moreover, if $(a,b)\in\tau$, then
$a\tau\cup\tau b=S$ is true for all $a,b\in S$.

###### Proof.

See [18]. ∎

Lemma 3.3, due to Proposition 3.2, cannot be proved outside CD as logical
background.

###### Remark 7

In intuitionistic logic of constant domain CD, the notions of sd-subset and
qd-subset coincide.

####  3.1.4 QSP for sets with apartness

The Quotient Structure Problem, QSP, is one of the very first problems which
has to be considered for any structure with apartness. The solutions of the
QSP problem for sets and semigroups with apartness was given in [17]. Those
results are improved in [41]. In what follows, we achieve a little progress in
that direction. Theorem 3.2, the key theorem for the QSP’s solution
generalizes the similar ones from [17], [41]. In addition, as a generalization
of the Theorem 3.3, the first apartness isomorphism theorem, the new Theorem
3.4, that we call the second apartness isomorphism theorem for sets with
apartness is formulated and proved.

The quotient structures are not part of BISH. A quotient structure does not
have, in general, a natural apartness relation. For most purposes, we overcome
this problem using a _co-equivalence_ –symmetric co-quasiorder–instead of an
equivalence. Existing properties of a co-equivalence guarantee its
a-complement is an equivalence as well as the quotient set of that equivalence
will inherit an apartness. The following notion will be necessary. For any two
relations $\alpha$ and $\beta$ on $S$ we can say that $\mathbf{\alpha}$
_defines an apartness on_ ${S/\beta}$ if we have

(Ap6) $x\beta\,\\#\,y\beta\ \stackrel{{\scriptstyle\rm
def}}{{\Leftrightarrow}}\ (x,y)\in\alpha$.

If in addition $\alpha$ is a co-quasiorder and $\beta$ is an equivalence, then
(Ap6) implies

(Ap6’) $((x,a)\in\beta\,\wedge\,(y,b)\in\beta)\ \Rightarrow\
((x,y)\in\alpha\,\Leftrightarrow\,(a,b)\in\alpha).$

Indeed, let $\alpha$ be a co-quasiorder and $\beta$ an equivalence on $S$ such
that $\mathbf{\alpha}$ _defines an apartness on_ ${S/\beta}$. Let
$(x,a),(y,b)\in\beta$, i.e. $a\in x\beta$ and $b\in y\beta$, which, by the
assumption, gives $a\beta=x\beta$ and $b\beta=y\beta$. If $(x,y)\in\alpha$,
then, by (Ap6), $x\beta\,\\#\,y\beta$, which, by (Ap5’), gives
$a\beta\,\\#\,b\beta$. By (Ap6) we have $(a,b)\in\alpha$. In a similar manner,
starting from $(a,b)\in\alpha$ we can conclude $(x,y)\in\alpha$.

The next theorem is the key for the solution of QSP for sets with apartness.
It generalizes the results from [17], [41].

###### Theorem 3.2

Let $S$ be a set with apartness. Then:

  * _(i)_

Let $\varepsilon$ be an equivalence, and $\kappa$ a co-equivalence on $S$.
Then, $\kappa$ defines an apartness on the factor set $S/\varepsilon$ if and
only if $\varepsilon\cap\kappa=\emptyset$.

  * _(ii)_

The quotient mapping $\pi:S\rightarrow S/\varepsilon$, defined by
$\pi(x)=x\varepsilon$, is an onto se-mapping.

###### Proof.

(i). Let $x,y\in S$ and assume that $(x,y)\in\varepsilon\cap\kappa$. Then
$(x,y)\in\varepsilon$ and $(y,y)\in\varepsilon$, which, by (Ap6’) and and
$(x,y)\in\kappa$, gives $(y,y)\in\kappa$, which is impossible. Thus,
$\varepsilon\cap\kappa=\emptyset$.

Let $(x,a),(y,b)\in\varepsilon$ and $(x,y)\in\kappa$. Then, by co-transitivity
of $\kappa$ and by assumption, we have

$\displaystyle(x,y)\in\kappa$ $\displaystyle\ \Rightarrow\ $
$\displaystyle(x,a)\in\kappa\vee(a,y)\in\kappa$ $\displaystyle\ \Rightarrow\ $
$\displaystyle(x,a)\in\kappa\vee(a,b)\in\kappa\vee(b,y)\in\kappa$
$\displaystyle\ \Rightarrow\ $ $\displaystyle(a,b)\in\kappa.$

(ii). Let $\pi(x)\\#\pi(y)$, that is $x\varepsilon\\#y\varepsilon$, which, by
(i), means that $(x,y)\in\kappa$. Then, by the strong irreflexivity of
$\kappa$, we have $x\\#y$. So $\pi$ is an se-mapping.

Let $a\varepsilon\in S/\varepsilon$ and $x\in a\varepsilon$. Then
$(a,x)\in\varepsilon$, i.e. $a\varepsilon=x\varepsilon$, which implies that
$a\varepsilon=x\varepsilon=\pi(x)$. Thus $\pi$ is an onto mapping. ∎

###### Corollary 3.1

If $\kappa$ is a co-equivalence on $S$, then the relation
${\sim}\kappa(={\neg}\kappa)$ is an equivalence on $S$, and $\kappa$ defines
an apartness on $S/\,\sim\kappa$.

###### Proof.

By Lemma 3.1, $\sim\kappa$ is an equivalence, by Proposition 3.1,
$(\sim\kappa)=(\neg\kappa)$, and, by Theorem 3.2, $\kappa$ defines an
apartness on $S/\sim\kappa$. ∎

Let $f:S\to T$ be an se-mapping between sets with apartness. Then the relation

$\mathrm{coker}\,f\stackrel{{\scriptstyle\rm def}}{{=}}\\{(x,y)\in S\times
S:f(x)\\#f(y)\\}$

defined on $S$ is called the _co-kernel_ of $f$. Now, _the first apartness
isomorphism theorem_ for sets with apartness follows.

###### Theorem 3.3

Let $f:S\to T$ be an se-mapping between sets with apartness. Then

  * _(i)_

the co-kernel of $f$ is a co-equivalence on $S$ which defines an apartness on
$S/\ker\,f$;

  * _(ii)_

the mapping $\theta:S/\ker\,f\to T$, defined by $\theta(x(\ker\,f))=f(x)$, is
a one-one, a-injective se-mapping such that $f=\theta\circ\pi$;

  * _(iii)_

if $f$ maps $S$ onto $T$, then $\theta$ is an apartness bijection.

###### Proof.

See [41]. ∎

Now, _the second apartness isomorphism theorem_ , a generalised version of
Theorem 3.3, for sets with apartness follows.

###### Theorem 3.4

Let $f:S\to T$ be a mapping between sets with apartness, and let $\kappa$ be a
co-equivalence on $S$ such that $\kappa\cap\mathrm{ker}\,f=\emptyset$. Then:

  * _(i)_

$\kappa$ defines apartness on factor set $S/\mathrm{ker}\,f$;

  * _(ii)_

the projection $\pi:S\to S/\mathrm{ker}\,f$ defined by
$\pi(x)=x(\mathrm{ker}\,f)$ is an onto se-mapping;

  * _(iii)_

the mapping $f$ induces a one-one mapping $\theta:S/\mathrm{ker}\,f\to T$
given by $\theta(x(\mathrm{ker}\,f))=f(x)$, and $f=\theta\circ\pi$;

  * _(iv)_

$\theta$ is an se-mapping if and only if $\mathrm{coker}\,f\subseteq\kappa$;

  * _(v)_

$\theta$ is a-injective if and only if $\kappa\subseteq\mathrm{coker}\,f$.

###### Proof.

(i). It follows from Theorem 3.2(i).

(ii). It follows from Theorem 3.2(ii).

(iii). This was shown in Theorem 3.3.

(iv). Let $\theta$ be an se-mapping. Let
$(x,y)\in\mathrm{\mathrm{\mathrm{coker}}}\,f$ for some $x,y\in S$. Then, by
definition of $\mathrm{coker}\,f$ and $\theta$, the assumption and (i), we
have

$\displaystyle f(x)\\#f(y)\ $ $\displaystyle\Leftrightarrow$ $\displaystyle\
\theta(x(\mathrm{ker}\,f))\\#\theta(y(\mathrm{ker}\,f))$
$\displaystyle\Rightarrow$ $\displaystyle\
x(\mathrm{ker}\,f)\\#y(\mathrm{ker}\,f)$ $\displaystyle\Leftrightarrow$
$\displaystyle\ (x,y)\in\kappa.$

Conversely, let $\mathrm{coker}\,f\subseteq\kappa$. By assumption, (i), (iii)
and the definitions of $\theta$ and $\mathrm{coker}\,f$, we have

$\displaystyle\theta(x(\mathrm{ker}\,f))\\#\theta(y(\mathrm{ker}\,f))\ $
$\displaystyle\Leftrightarrow$ $\displaystyle\ f(x)\\#f(y)$
$\displaystyle\Leftrightarrow$ $\displaystyle\ (x,y)\in\mathrm{coker}\,f$
$\displaystyle\Rightarrow$ $\displaystyle\ (x,y)\in\kappa$
$\displaystyle\Leftrightarrow$ $\displaystyle\
x(\mathrm{ker}\,f)\\#y(\mathrm{ker}\,f).$

(v). Let $\theta$ be a-injective, and let $(x,y)\in\kappa$. Then, by (iii), we
have

$\displaystyle x(\mathrm{ker}\,f)\\#y(\mathrm{ker}\,f)\ $
$\displaystyle\Rightarrow$ $\displaystyle\
\theta(x(\mathrm{ker}\,f))\\#\theta(y(\mathrm{ker}\,f))$
$\displaystyle\Leftrightarrow$ $\displaystyle\ f(x)\\#f(y)$
$\displaystyle\Leftrightarrow$ $\displaystyle\ (x,y)\in\mathrm{coker}\,f.$

Conversely, let $\kappa\subseteq\mathrm{coker}\,f$. Then

$\displaystyle x(\mathrm{ker}\,f)\\#y(\mathrm{ker}\,f)\ $
$\displaystyle\Leftrightarrow$ $\displaystyle\ (x,y)\in\kappa$
$\displaystyle\Rightarrow$ $\displaystyle\ (x,y)\in\mathrm{coker}\,f$
$\displaystyle\Leftrightarrow$ $\displaystyle\ f(x)\\#f(y)$
$\displaystyle\Leftrightarrow$ $\displaystyle\
\theta(x(\mathrm{ker}\,f))\\#\theta(y(\mathrm{ker}\,f)).$

∎

###### Corollary 3.2

Let $f:S\to T$ be a mapping between sets with apartness, and let $\kappa$ be a
co-equivalence on $S$ such that $\kappa\cap\mathrm{ker}\,f=\emptyset$. Then:

  * _(i)_

$f$ is an se-mapping if and only if $\mathrm{coker}\,f$ is strongly
irreflexive;

  * _(ii)_

if $\theta:S/\mathrm{ker}\,f\to T$, defined by
$\theta(x(\mathrm{ker}\,f))=f(x)$, is an se-mapping, then $f$ is an se-mapping
too.

###### Proof.

(i). Let $f$ be an se-mapping. Then, by Theorem 3.3, $\mathrm{coker}\,f$ is
strongly irreflexive. The converse is almost obvious.

(ii). If $\theta$ is an se-mapping then, by Theorem 3.4(iv), we have that
$\mathrm{coker}\,f\subseteq\kappa$. So, the strong irreflexivity of $\kappa$
implies the strong irreflexivity of $\mathrm{coker}\,f$, which, by (i),
implies $f$ is an se-mapping. ∎

###### Remark 8

The notion of co-quasiorder first appeared in [50]. However, let us mention
that the results reported from [50]: Theorem 0.4, Lemma 0.4.1, Lemma 0.4.2,
Theorem 0.5 and Corollary 0.5.1 (pages 10-11 in [51]) are not correct. Indeed,
the mentioned filled product is not associative in general. The notion of co-
equivalence, i.e. a symmetric co-quasiorder, first appeared in [9].

###  3.2 Semigroups with apartness

Given a set with apartness $(S,=,\\#)$, the tuple $(S,=,\\#,\,\cdot)$ is a
_semigroup with apartness_ if the binary operation $\cdot$ is associative

  * (A)

$\enspace\quad\forall_{a,b,c\in S}\ [(a\cdot b)\cdot c\,=\,a\cdot(b\cdot c)]$,

and strongly extensional

  * (S)

$\enspace\quad\forall_{a,b,x,y\in S}\ (a\cdot x\\#\,b\cdot
y\Rightarrow(a\\#\,b\,\vee\,x\\#\,y))$.

As usual, we are going to write $ab$ instead of $a\cdot b$. For example, for a
given set with apartness $A$ we can construct a semigroup with apartness
$S=A^{A}$ in the following way.

###### Theorem 3.5

Let $S$ be the set of all se-functions from $A$ to $A$ with the standard
equality $=$

$f=\,g\ \Leftrightarrow\ \forall_{x\in A}\,(f(x)=\,g(x))$

and apartness

$f\\#\,g\ \Leftrightarrow\ \exists_{x\in A}\,(f(x)\\#\,g(x)).$

Then $(S,=,\\#,\circ)$ is a semigroup with respect to the binary operation
$\circ$ of composition of functions.

###### Proof.

See [18]. ∎

Until the end of of this paper, we adopt the convention that _semigroup_ means
_semigroup with apartness_. Apartness from Theorem 3.5 does not have to be
tight, [17].

Let $S$ and $T$ be semigroups with apartness. A mapping $f:S\rightarrow T$ is
a homomorphism if

$\forall_{x,y\in S}\,(f(xy)=f(x)f(y)).$

A homomorphism $f$ is

  * •

an _se-embedding_ if it is one-one and strongly extensional;

  * •

an _apartness embedding_ if it is a-injective se-embedding;

  * •

an _apartness isomorphism_ if it is apartness bijection and se-homomorphism.

Within CLASS, the semigroups can be viewed, historically, as an algebraic
abstraction of the properties of the composition of transformations on a set.
Cayley’s theorem for semigroups (which can be seen as an extension of the
celebrated Cayley’s theorem on groups) stated that every semigroup can be
embedded in a semigroup of all self-maps on a set. As a consequence of the
Theorem 3.5, we can formulate _the constructive Cayley’s theorem for
semigroups with apartness_ as follows.

###### Theorem 3.6

Every semigroup with apartness se-embeds into the semigroup of all strongly
extensional self-maps on a set.

###### Proof.

See [18]. ∎

###### Remark 9

Following [47], the term “constructive theorem” refers to a theorem with
constructive proof. A classical theorem that is proven in a constructive
manner is a constructive theorem.

It is a pretty common point of view that classical theorem becomes more
enlightening when it is seen from the constructive viewpoint. On the other
hand, it can not be said that the theory of constructive semigroups with
apartness aims at revising the whole classical framework in nature.

####  3.2.1 Co-quasiorders defined on a semigroup

We are going to encounter sd-subsets or sd-subsemigroups which have some of
the properties mentioned in Section 2.1.1. A strongly detachable convex
(respectively completely isolated) subsemigroup of $S$ is called, in short, an
_sd-convex_ (respectively sd-completely isolated) subsemigroup of $S$.
Similarly, there are sd-convex and sd-completely isolated ideals of $S$.

###### Lemma 3.4

Let $S$ be a semigroup with apartness. The following conditions are true:

  * _(i)_

Let $T$ be an sd-convex subset of a semigroup with apartness $S$. If ${\sim}T$
is inhabited, then it is an ideal of $S$.

  * _(ii)_

If $I$ is an sd-completely isolated ideal of a semigroup with apartness $S$,
then ${\sim}I$ is a convex subsemigroup of $S$.

###### Proof.

(i). Let $x,y,\in{\sim}T$. Let $a\in{\sim}T$ and $x\in S$. By the assumption
we have that $ax\in T$ or $ax\in\sim T$. If $ax\in T$, then, as $T$ is convex,
we have $a\in T$, which is impossible. Similarly, one can prove that
$xa\in{\sim}T$. So, ${\sim}T$ is an ideal of $S$.

(ii). In a similar manner as in (i) we can prove that ${\sim}I$ is a
subsemigroup of $S$.

Let $xy\in{\sim}I$. By the assumption, we have $x\in I$ or $x\in\sim I$. If
$x\in I$, then, as $I$ is an ideal, we have $xy\in I$, which is impossible.
Thus $x\in\sim I$. Similarly, we can prove that $y\in{\sim}I$. So, ${\sim}I$
is convex. ∎

Let us start with an example of a co-quasiorder defined on a semigroup with
apartness $S$.

###### Example 5

Let $S$ be a semigroup given by

$\cdot$ | a | b | c | d | e
---|---|---|---|---|---
a | b | b | d | d | d
b | b | b | d | d | d
c | d | d | c | d | c
d | d | d | d | d | d
e | d | d | c | d | c

Let the equality on $S$ be the diagonal
$\triangle_{S}=\\{(a,a),(b,b),(c,c),(d,d),(e,e)\\}.$ If we denote by
$K=\triangle_{S}\cup\\{(a,b),(b,a)\\}$, then we can define an apartness $\\#$
on $S$ by $(S\times S)\setminus K$. The relation $\tau\subseteq S\times S$,
defined by

$\tau=\\{(c,a),(c,b),(d,a),(d,b),(d,c),(e,a),(e,b),(e,c),(e,d)\\},$

is a co-quasiorder on $S$.

Let $\tau$ be a co-quasiorder defined on a semigroup $S$ with apartness.
Following the classical results as much as possible, we can start with the
following definition.

A co-quasiorder $\tau$ on a semigroup $S$ is

  * •

_complement positive_ if $(a,ab),(a,ba)\in\sim\tau$ for any $a,b\in S$,

  * •

with _constructive common multiple property_ , or, in short, with
_constructive cm-property_ if
$(ab,c)\in\tau\Rightarrow(a,c)\in\tau\vee(b,c)\in\tau$ for all $a,b,c\in S$,

  * •

with _complement common multiple property_ , or, in short, with _complement
cm-property_ if $(a,c),(b,c)\in\sim\tau\Rightarrow(ab,c)\in\sim\tau$ for all
$a,b,c\in S$.

Recall, by the Proposition 3.1, $(\sim\tau)=(\neg\tau)$.

###### Example 6

The co-quasiorder $\alpha$ defined on the semigroup $S$ considered in Example
5 is not complement positive because we have $(e,ea)=(e,d)\in\alpha$.

###### Example 7

Let $S$ be the three element semilattice given by

$\cdot$ | a | b | c
---|---|---|---
a | a | c | c
b | c | b | c
c | c | c | c

Let the equality on $S$ be the diagonal
$\triangle_{S}=\\{(a,a),(b,b),(c,c)\\}$. We can define an apartness $\\#$ on
$S$ to be $(S\times S)\setminus\triangle_{S}$. Thus, $(S,=,\\#,\cdot)$ is a
semigroup with apartness. The relation $\tau\subseteq S\times S$, defined by

$\tau=\\{(a,b),(c,a),(c,b)\\},$

is a complement positive co-quasiorder on $S$.

On the other hand, from $(ab,a)=(c,a)\in\tau$ neither $(a,a)$ nor $(b,a)$ are
in $\tau$, so $\tau$ does not have the constructive cm-property. From
$(a,a)\bowtie\tau$ and $(b,a)\bowtie\tau$, we have $(ab,a)=(c,a)\in\tau$, and
$\tau$ does not have the complement cm-property as well.

The following lemma shows how some sd-subsets lead us to positive co-
quasiorders.

###### Lemma 3.5

Let $S$ be a semigroup with apartness $S$.

  * _(i)_

If $K$ is an sd-convex subset of $S$, then the relation $\tau$ defined by

$(a,b)\in\tau\stackrel{{\scriptstyle\rm def}}{{\Leftrightarrow}}a\in\sim
K\wedge b\in K$

is a complement positive co-quasiorder on $S$.

  * _(ii)_

If $J$ is an sd-ideal of $S$ such that $J\subset S$, then the relation $\tau$
defined by

$(a,b)\in\tau\stackrel{{\scriptstyle\rm def}}{{\Leftrightarrow}}a\in J\wedge
b\in\sim J$

is a complement positive co-quasiorder on $S$.

###### Proof.

(i). By Lemma 3.2, $\tau$ is a co-quasiorder on $S$. Let $(x,y)\in\tau$. By
the co-transitivity of $\tau$, we have
$(x,a)\in\tau\,\vee\,(a,ab)\in\tau\,\vee\,(ab,y)\in\tau$, for any $a,b\in S$.
If $(a,ab)\in\tau$, then, by the definition of $\tau$, we have $a\in\sim K$
and $ab\in K$, and, as $K$ is a convex subset, we have $a\in K$ and $b\in K$,
which is impossible. So, we have $(x,a)\in\tau\,\vee\,(ab,y)\in\tau$. By the
strong irreflexivity of $\tau$ we have $x\\#a\,\vee\,ab\\#y$, i.e.
$(x,y)\\#(a,ab)$. Thus, we have proved that $(a,ab)\bowtie\tau$ for any
$a,b\in S$. The proof of $(a,ba)\bowtie\tau$ is similar. Therefore, $\tau$ is
a complement positive co-quasiorder on $S$.

(ii). By Lemma 3.2, $\tau$ is a co-quasiorder on $S$. Let $(x,y)\in\tau$. By
the co-transitivity of $\tau$, we have
$(x,a)\in\tau\,\vee\,(a,ab)\in\tau\,\vee\,(ab,y)\in\tau,$ for any $a,b\in S$.
If $(a,ab)\in\tau$, then, by the definition of $\tau$, we have $a\in J$ and
$ab\in\sim J$, which, as $J$ is an ideal, further implies $ab\in J$, which is
a contradiction. The rest of the proof is similar to the arguments in the
proof of (i). ∎

By Proposition 3.2, if any left/right-class of a co-quasiorder defined on a
set with apartness is a (strongly) detachable subset, then LPO holds. This
shows that Theorem 4.1 on a complement positive co-quasiorder (and Lemma 3.2
important for its proof) from [18] cannot be proved outside intuitionistic
logic of constant domains CD. Nevertheless, we can prove within intuitionistic
logic the next theorem, which is its weaker version, and another important
result of this section. The description of a complement positive co-quasiorder
via its classes follows.

###### Theorem 3.7

Let $\tau$ be a co-quasiorder $\tau$ on a semigroup $S$.

  * _(i)_

If $\tau$ is complement positive, then

$\forall_{a,b\in S}\ \ (\tau(ab)\subseteq\tau a\cap\tau b).$

  * _(ii)_

If $\tau a$ is an sd-ideal of $S$ and $a\bowtie\tau a$ for every $a\in S$,
then $\tau$ is complement positive and

$\forall_{a,b\in S}\ \ (a\tau\cup b\tau\subseteq(ab)\tau).$

  * _(iii)_

If $a\tau$ is an sd-convex subset of $S$, and $a\bowtie a\tau$ for every $a\in
S$, then $\tau$ is a complement positive co-quasiorder.

###### Proof.

(i). Let $\tau$ be a complement positive co-quasiorder. For all $a,b,x\in S$
such that $x\in\tau(ab)$, that is $(x,ab)\in\tau$, by the co-transitivity of
$\tau$, we have

$((x,a)\in\tau\vee(a,ab)\in\tau)\wedge((x,b)\in\tau\vee(b,ab)\in\tau).$

But, $\tau$ is complement positive, so that we have
$(x,a)\in\tau\wedge(x,b)\in\tau$, i.e. $x\in\tau a\cap\tau b$.

(ii). Let $(x,y)\in\tau$ and $a,b\in S$. Then, by the co-transitivity of
$\tau$,

$(x,a)\in\tau\vee(a,ab)\in\tau\vee(ab,y)\in\tau.$

If $a\in\tau(ab)$, then, as $\tau(ab)$ is an ideal, we have $ab\in\tau(ab)$,
which is, by the assumption, impossible. Now, by the strong irreflexivity of
$\tau$, we have $x\\#a$ or $ab\\#y$, that is $(x,y)\\#(a,ab)$. Thus,
$(a,ab)\bowtie\tau$ for any $a,b\in S$. $(a,ba)\bowtie\tau$ can be proved
similarly. Thus, $\tau$ is a complement positive co-quasiorder.

Let $x\in a\tau\cup b$, $x\in S$. By the co-transitivity and complement
positivity of $\tau$, we have

$\displaystyle x\in a\tau\cup b\tau$ $\displaystyle\Leftrightarrow x\in
a\tau\vee x\in b\tau$
$\displaystyle\Leftrightarrow(a,x)\in\tau\vee(b,x)\in\tau$
$\displaystyle\Rightarrow((a,ab)\in\tau\vee(ab,x)\in\tau)\vee((b,ab)\in\tau\vee(ab,x)\in\tau)$
$\displaystyle\Rightarrow(ab,x)\in\tau$ $\displaystyle\Leftrightarrow
x\in(ab)\tau.$

(iii). Let $(x,y)\in\tau$. Then, by the co-transitivity of $\tau$,

$(x,a)\in\tau\vee(a,ab)\in\tau\vee(ab,y)\in\tau,$

for any $a,b\in S$. Let $(a,ab)\in\tau$, that is $ab\in a\tau$. Then, by
assumption, $a\in a\tau$ (and $b\in a\tau$), which is impossible. Now, by the
strong irreflexivity of $\tau$, we have $x\\#a$ or $ab\\#y$, that is,
$(x,y)\\#(a,ab)$. Thus $(a,ab)\bowtie\tau$ for any $a,b\in S$.
$(a,ba)\bowtie\tau$ can be proved similarly. Thus, $\tau$ is a complement
positive co-quasiorder. ∎

###### Theorem 3.8

A complement positive co-quasiorder with the constructive cm-property has the
complement cm-property.

###### Proof.

Let $\tau$ be a complement positive co-quasiorder with the constructive cm-
property on a semigroup $S$ and let $a,b,c,x,y\in S$ be such that
$(a,c),(b,c)\bowtie\tau$ and $(x,y)\in\tau$. Then we have

$\displaystyle(x,y)\in\tau$
$\displaystyle\Rightarrow(x,ab)\in\tau\vee(ab,c)\in\tau\vee(c,y)\in\tau$ by
co-transitivity $\displaystyle\Rightarrow
x\\#ab\vee(a,c)\in\tau\vee(b,c)\in\tau\vee c\\#y$ by strong reflexivity and by
constructive cm-property $\displaystyle\Rightarrow(ab,c)\\#(x,y)$ since
$(a,c)\bowtie\tau$ and $(b,c)\bowtie\tau$.

Hence $(ab,c)\bowtie\tau$, i.e. $(ab,c)\in\sim\tau$. ∎

####  3.2.2 Intuitionistic logic of constant domains CD as a background

If we have a complement positive co-quasiorder $\tau$ on a semigroup with
apartness $S$, we can construct special subsets and semigroups mentioned
above. Some other criteria for a co-quasiorder to be complement positive will
be given too.

###### Theorem 3.9

The following conditions for a co-quasiorder $\tau$ on a semigroup $S$ are
equivalent:

  * _(i)_

$\tau$ is complement positive;

  * _(ii)_

$\forall_{a,b\in S}\ \ (a\tau\cup b\tau\subseteq(ab)\tau)$;

  * _(iii)_

$\forall_{a,b\in S}\ \ (\tau(ab)\subseteq\tau a\cap\tau b)$;

  * _(iv)_

$a\tau$ is an sd-convex subset of $S$ and $a\bowtie a\tau$ for every $a\in S$;

  * _(v)_

$\tau a$ is an sd-ideal of $S$ and $a\bowtie\tau a$ for every $a\in S$.

###### Proof.

(i) $\Rightarrow$ (iii), (v) $\Rightarrow$ (i), (v) $\Rightarrow$ (ii), (iv)
$\Rightarrow$ (ii). Those implications are proved in the Theorem 3.7.

(iii) $\Rightarrow$ (iv). By Lemma 3.3, $a\tau$ is an sd-subset of $S$ such
that $a\bowtie a\tau$ for any $a\in S$. We have

$\displaystyle xy\in a\tau$ $\displaystyle\Leftrightarrow(a,xy)\in\tau$
$\displaystyle\Leftrightarrow a\in\tau(xy)\subseteq\tau x\cap\tau y$
$\displaystyle\Rightarrow a\in\tau x\wedge a\in\tau y$
$\displaystyle\Leftrightarrow x\in a\tau\wedge y\in a\tau.$

So, $a\tau$ is an sd-convex subset for any $a\in S$.

(i) $\Rightarrow$ (v). By Lemma 3.3, $\tau a$ is an sd-subset of $S$ such that
$a\bowtie\tau a$ for any $a\in S$. Let $a,x\in S$ be such that $x\in\tau a$,
i.e. $(x,a)\in\tau$. By the co-transitivity of $\tau$, we have

$(x,xs)\in\tau\vee(xs,a)\in\tau,$

for any $s\in S$. But, as $\tau$ is positive, we have only $(xs,a)\in\tau$,
i.e $xs\in\tau a$. In the same way one can prove that $sx\in\tau a$. Thus,
$\tau a$ is an ideal of $S$ for any $a\in S$.

(ii) $\Rightarrow$ (v). By Lemma 3.3, $\tau a$ is an sd-subset of $S$, and
$a\bowtie\tau a$ for any $a\in S$. Now, let $x\in\tau a$ and $s\in S$. Then,
by the co-transitivity of $\tau$, we have $(x,xs)\in\tau$ or $(xs,a)\in\tau$.
If $(x,xs)\in\tau$, then $xs\in x\tau\subseteq x\tau\cup
s\tau\subseteq(xs)\tau$, which is, by Lemma 3.3, impossible. Thus
$(xs,a)\in\tau$. As $(sx,a)\in\tau$ can be proved similarly, we have proved
that $\tau a$ is an sd-ideal of $S$. ∎

###### Theorem 3.10

Let $\tau$ be a complement positive co-quasiorder on a semigroup $S$. The
following conditions are equivalent:

  * _(i)_

$\tau$ has the constructive cm-property;

  * _(ii)_

$\forall_{a,b\in S}\ ((ab)\tau=a\tau\cup b\tau)$;

  * _(iii)_

$\tau a$ is an sd-completely isolated ideal of $S$ such that $a\bowtie\tau a$
for any $a\in S$.

###### Proof.

(i) $\Rightarrow$ (ii). By Theorem 3.9, $a\tau\cup b\tau\subseteq(ab)\tau$ for
all $a,b\in S$. To prove the converse inclusion, take $x\in(ab)\tau$. Then we
have

$\displaystyle x\in(ab)\tau$ $\displaystyle\Leftrightarrow(ab,x)\in\tau$
$\displaystyle\Rightarrow(a,x)\in\tau\vee(b,x)\in\tau$ by the cm-property
$\displaystyle\Leftrightarrow x\in a\tau\vee x\in b\tau$
$\displaystyle\Leftrightarrow x\in a\tau\cup b\tau.$

(ii) $\Rightarrow$ (iii). By Theorem 3.9, $\tau a$ is an sd-ideal of $S$ such
that $a\bowtie\tau a$, for any $a\in S$. Let $x,y\in S$ be such that
$xy\in\tau a$. Then $a\in(xy)\tau=x\tau\cup y\tau$ by the assumption. Thus,
$a\in x\tau$ or $a\in y\tau$. So, $x\in\tau a$ or $y\in\tau a$, and $\tau a$
is an sd-completely isolated ideal of $S$ for any $a\in S$.

(iii) $\Rightarrow$ (i). Let $a,b,c\in S$ be such that $(ab,c)\in\tau$. Then,
$ab\in\tau c$ and, since $\tau c$ is completely isolated, $a\in\tau c$ or
$b\in\tau c$, which means that $(a,c)\in\tau$ or $(b,c)\in\tau$. ∎

Following Bishop, every classical theorem presents the challenge: find a
constructive version with a constructive proof. This constructive version can
be obtained by strengthening the conditions or weakening the conclusion of the
theorem. There are, often, several constructively different versions of the
same classical theorem.

Comparing the obtained results for complement positive co-quasiorders with the
parallel ones for positive quasiorders in the classical background, we can
conclude that the classical Theorem 2.1 breaks into two new ones in the
constructive setting:

  * •

Theorem 3.7 obtained by weakening the conclusions,

  * •

Theorem 3.9 obtained by strengthening the conditions - here strengthening the
logical background. Recall that intermediate logic proves intuitionistically
as well as classically valid theorems, yet they often possess a strong
constructive flavour.

In addition, there are two definitions: those of the constructive cm-property,
and the complement cm-property. Nevertheless, the last definition, Theorem
3.8, is stronger.

###### Remark 10

For some classical theorems it is shown that they are not provable
constructively. Some classical theorems are neither provable nor disprovable,
that is, they are independent of BISH.

####  3.2.3 QSP for semigroups with apartness

Let us remember that in CLASS the compatibility property is an important
condition for providing the semigroup structure on quotient sets. Now we are
looking for the tools for introducing an apartness relation on a factor
semigroup. Our starting point is the results from Subsection 3.1.4, as well as
the next definition.

A co-equivalence $\boldsymbol{\kappa}$ is a _co-congruence_ if it is _co-
compatible_

$\forall_{a,b,x,y\in S}\,((ax,by)\in\kappa\ \Rightarrow\
(a,b)\in\kappa\vee(x,y)\in\kappa)$

###### Theorem 3.11

Let $S$ be a semigroup with apartness. Then

  * _(i)_

Let $\mu$ be a congruence, and $\kappa$ a co-congruence on $S$. Then, $\kappa$
defines an apartness on the factor set $S/\mu$ if and only if
$\mu\cap\kappa=\emptyset$.

  * _(ii)_

The quotient mapping $\pi:S\rightarrow S/\mu$, defined by $\pi(x)=x\mu$, is an
onto se-homomorphism.

###### Proof.

(i). If $\kappa$ defines an apartness on $S/\mu$, then, by Theorem 3.2(i),
$\mu\cap\kappa=\emptyset$.

Let $\mu$ be a congruence and $\kappa$ a co-congruence on a semigroup with
apartness $S$ such that $\mu\cap\kappa=\emptyset$. Then, by Theorem 3.2(i),
$\kappa$ defines apartness on$S/\mu$.

Let $a\mu\,x\mu\\#b\mu\,y\mu$, then $(ax)\mu\\#(bx)\mu$ which further, by the
definition of apartness on $S/\mu$, ensures that $(ax,by)\in\kappa$. But
$\kappa$ is a co-congruence, so either $(a,b)\in\kappa$ or $(x,y)\in\kappa$.
Thus, by the definition of apartness in $S/\mu$ again, either $a\mu\\#b\mu$ or
$x\mu\\#y\mu$. So $(S/\mu,=,\\#,\cdot\,)$ is a semigroup with apartness.

(ii). By Theorem 3.2(ii), $\pi$ is an onto se-mapping. By (i) and assumption,
we have

$\pi(xy)=(xy)(\sim\kappa)=x(\sim\kappa)\,y(\sim\kappa)=\pi(x)\pi(y).$

Hence $\pi$ is a homomorphism. ∎

As a consequence of Theorem 3.11 and Corollary 3.1 we have the next corollary.

###### Corollary 3.3

If $\kappa$ is a co-congruence on $S$, then the relation
${\sim}\kappa(={\neg}\kappa)$ is a congruence on $S$, and $\kappa$ defines an
apartness on $S/\sim\kappa$.

_The apartness isomorphism theorem for semigroups with apartness_ follows.

###### Theorem 3.12

Let $f:S\rightarrow T$ be an se-homomorphism between semigroups with
apartness. Then:

  * _(i)_

$\mathrm{coker}\,f$ is a co-congruence on $S$, which defines an apartness on
$S/\ker\,f$,

  * _(ii)_

the mapping $\theta:S/\ker\,f\to T$, defined by $\theta(x(\ker\,f))=f(x)$, is
an apartness embedding such that $f=\theta\circ\pi$; and

  * _(iii)_

if $f$ maps $S$ onto $T$, then $\theta$ is an apartness isomorphism.

###### Proof.

See [41]. ∎

Recall, following [47], BISH (and constructive mathematics in general) is not
the study of constructive things, it is a constructive study of things. In
constructive proofs of classical theorems, only constructive methods are used.

Although constructive theorems might look like the corresponding classical
versions, they often have more complicated hypotheses and proofs. Comparing
Theorem 2.4 (respectively Theorem 2.3) for classical semigroups and Theorem
3.12 (respectively Theorem 3.11) for semigroup with apartness, we have
evidence for that.

##  4 Concluding remarks

During the implementation of the FTA Project [25], the notion of commutative
constructive semigroups with tight apartness appeared. We put noncommutative
constructive semigroups with “ordinary” apartness in the centre of our study,
proving first, of course, that such semigroups do exist. Once again we want to
emphasize that semigroups with apartness are a new approach, and not a new
class of semigroups.

Let us give some examples of applications of ideas presented in the previous
section. We will start with constructive analysis. The proof of one of the
directions of the constructive version of the Spectral Mapping Theorem is
based on some elementary constructive semigroups with inequality techniques,
[12]. It is also worth mentioning the applications of commutative basic
algebraic structures with tight apartness within the automated reasoning area,
[16]. For possible applications within computational linguistic see [42]. Some
topics from mathematical economics can be approached constructively too (using
some order theory for sets with apartness), [2]. Contrary to the classical
case, the applications of constructive semigroups with apartness, due to their
novelty, constitute an unexplored area. In what follows some possible
connections between semigroups with apartness and computer science are
sketched, [41].

semigroups with apartness semigroups with apartness

$\updownarrow$ $\updownarrow$

bisimulation automated theorem proving

$\updownarrow$ $\updownarrow$

formal reasoning about processes knowledge representation and automated
reasoning

$\updownarrow$ $\updownarrow$

process algebra artificial intelligence

$\updownarrow$

transactions and concurrency

$\updownarrow$

databases

One of the directions of future work is to be able to say more about those
links. The study of basic constructive algebraic structures with apartness as
well as constructive algebra as a whole can impact the development of other
areas of constructive mathematics. On the other hand, it can make both proof
engineering and programming more flexibile.

Although the classical theory of semigroups has been considerably developed in
the last decades, constructive mathematics has not paid much attention to
semigroup theory. One of our main scientific activities will be to further
develop of the constructive theory of semigroups with apartness. Semigroups
will be examined constructively, that is with intuitionistic logic. To develop
this constructive theory of semigroups with apartness, we need first to
clarify the notion of a set with apartness. The initial step towards grounding
the theory is done by our contributing papers [17], [18], [40], [41], [20] \-
a critical review of some of those results as well as the solutions to some of
the open problems arising from those papers are presented in Section 3.

Why should a mathematician choose to work in this manner? As it is written in
one of the reviews of Errett Bishop’s monograph _Foundations of functional
analysis_ , [59], “to replace the classical system by the constructive one
does not in any way mutilate the great classical theories of mathematics. Not
at all. If anything, it strengthens them, and shows them, in a truer light, to
be far grander than we had known.” At heart, Bishop’s constructive mathematics
is simply mathematics done with intuitionistic logic, and may be regarded as
“constructive mathematics for the working mathematician”, [61]. The main
activity in the field consists in proving theorems rather than demonstrating
the unprovability of theorems (or making other metamathematical observations),
[3]. “Theorems are tools that make new and productive applications of
mathematics possible,” [33].

The theory of semigroups with apartness is, of course, in its infancy, but, as
we have already pointed out, it promises a prospective of applications in
other (constructive) mathematics disciplines, certain areas of computer
science, social sciences, economics.

To conclude, although one of the main motivators for initiating and developing
the theory of semigroups with apartness comes from the computer science area,
in order to have profound applications, a certain amount of the theory, which
can be applied, is necessary first. Among priorities, besides the growing the
general theory, are further developments of: constructive relational
structures - (co)quotient structures in the first place, constructive order
theory, theory of ordered semigroups with apartness, etc.

The Summary of the European Commission’s _Mathematics for Europe_ , June 2016,
[21], states that “mathematics should not only focus on nowadays’ applications
but should leave room for development, even theoretical, that may be vital
tomorrow.” With a strong belief in the tomorrow’s vitalness of the theory of
semigroups with apartness, the focus should be on its further development. On
the other hand, it is useful to “leave room” for “nowadays’ applications” as
well. All those will represent the core of our forthcoming papers.

### Acknowledgements

The authors are grateful to anonymous referees for careful reading of the
manuscript and helpful comments. M. M. is supported by the Faculty of
Mechanical Engineering, University of Niš, Serbia, Grant “Research and
development of new generation machine systems in the function of the
technological development of Serbia”. M. N. H. is supported by TWAS Research
Grant RGA No. 17-542 RG / MATHS / AF / AC _G -FR3240300147. The ICMPA-UNESCO
Chair is in partnership with Daniel Iagolnitzer Foundation (DIF), France, and
the Association pour la Promotion Scientifique de l’Afrique (APSA), supporting
the development of mathematical physics in Africa.

## References

  * [1] Aschieri F. _On Natural Deduction for Herbrand Constructive Logics III: The Strange Case of the Intuitionistic Logic of Constant Domains_. In Berardi S., Miquel A. eds.: CL&C 2018 EPTCS 281, 2018, pp. 1-9, doi:10.4204/EPTCS.281.1.
  * [2] Baroni M, Bridges DS. _Continuity properties of preference relations_ , Mathematical Logic Quarterly 2008\. 54(5):454–459. doi:10.1016/j.entcs.2008.03.004
  * [3] Beeson MJ. Foundations of Constructive Mathematics, Springer-Verlag, 1985. ISBN:978-3-642-68952-9.
  * [4] Bishop E. Foundations of Constructive Analysis, McGraw-Hill, New York, 1967.
  * [5] Bishop E, Bridges DS. Constructive Analysis, Grundlehren der mathematischen Wissenschaften 279, Springer, Berlin, 1985. ISBN-10:364264905X, 13:978-3642649059.
  * [6] Ćirić M, Bogdanović S. _The lattice of positive quasi-orders on a semigroup_ , Israel Journal of Mathematics 1997\. 98(1):157–166.
  * [7] Boorman SA, White HC. _Social structures from multiple networks. II. Role structures_ , The American Journal of Sociology, 1976\. 81(6):1384–1446. doi:10.1086/226228.
  * [8] Boyd JP. Social semigroups, a unified theory of scaling and blockmodelling as applied to social networks, George Mason University Press, 1991. ISBN-10:0913969346, 13:978-0913969342.
  * [9] Božić M, Romano DA. _Relations, functions and operations in the constructive mathematics_ , Publ. VTS, Ser.A: Math., 1987\. 2:25–39.
  * [10] Bridges DS. _A constructive look at the real number line_. In Ehrlich P., ed.: Real Numbers, Generalizations of the Reals, and Theories of Continua, Kluwer Academic Publishers, 1994. doi:10.1007/978-94-015-8248-3_2.
  * [11] Bridges DS, Reeves S. _Constructive Mathematics in Theory and Progamming Practic_ e, Philosophia Mathematica (3) 1999\. 7(1):63–104. doi:10.1093/philmat/7.1.65.
  * [12] Bridges DS, Havea R. _A Constructive Version of the Spectral Mapping Theorem_ , Mathematical Logic Quarterly 2001\. 47(3):299–304. ISSN-0942-5616.
  * [13] Bridges DS, Vîţā LS. Apartness and Uniformity - A Constructive Development, CiE series on Theory and Applications of Computability, Springer, 2011. ISBN-13:978-3642224140, 10:3642224148.
  * [14] Brouwer LEJ. _De onbetrouwbaarheid der logische principes, Tijdschrijt voor wijsbegeerte 2_ , 152–158, 1908. English translation: _The unreliability of the logical principles_. In Heyting A., ed.: Collected Works, Vol. 1 , North-Holland, Amsterdam 1975 pp. 107–111.
  * [15] Broy M. _Seamless model driven systems engineering based on formal models_. In Breitman K., Cavalcanti A., eds.: ICFEM 2009 (LNCS 5885), 2009 pp. 1–19. doi:10.1007/978-3-642-10373-5_1.
  * [16] Calder$\rm{\acute{o}}$n G. _Formalizing constructive projective geometry in Agda_ , 2017, The Proceedings of The 12th Workshop on Logical and Semantic Frameworks, with Applications, LSFA 2017 (Brasilia, 23-24 September 2017 - http://lsfa2017.cic.unb.br/).
  * [17] Crvenković S, Mitrović M, Romano DA. Semigroups with Apartness, Mathematical Logic Quarterly, 2013\. 59(6):407–414. doi:10.1002/malq.201200107.
  * [18] Crvenković S, Mitrović M, Romano DA. Basic Notions of (Constructive) Semigroups with Apartness, Semigroup Forum, Volume 92, Issue 3, June 2016 pp. 659–674. doi:10.1007/s00233-016-9776-y.
  * [19] van Dalen D, and de Vries F-J. _Intuitionistic free Abelian groups_ , Mathematical Logic Quarterly, 1988\. 34(1):3–12. doi:10.1002/malq.19880340102.
  * [20] Darp$\ddot{o}$ E, Mitrović M. _Some results in constructive semigroup theory_ , arXiv:2103.07105.
  * [21] European Commission, _Mathematics for Europe_ , June 2016,
  * [22] Ganyushkin O, Mazorchuk V. Classical Finite Transformation Semigroups, Algebra and Applications, Volume 9, Springer, Berlin, 2009. ISBN-978-1-84800-281-4.
  * [23] Grzegorczyk A. _A philosophically plausible formal interpretation of intuitionistic logic_ , Koninklijke Nederlandse Akademie van Wetenschappen, Proceedings, series A, vol. 67 (1964), pp. 596-601; also Indagationes mathematicae, vol. 26, 1964 pp. 596–601.
  * [24] Geuvers H, Wiedijk F, Zwanenburg J. _A constructive proof of the Fundamental theorem of algebra without using the rationals_ , 2002\. In Callaghan P., Luo Z., McKinna J., Pollack R., eds.: Proceedings of TYPES 2000 Workshop Durham UK. (Springer-Verlag) LNCS 2277 pp. 96–111. doi:10.1007/3-540-45842-5_7.
  * [25] Geuvers H, Pollack R, Wiedijk F, Zwanenburg J. _A constructive algebraic hierarchy in Coq_ , J. Symb. Comput., 2002. 34:271–286. doi:10.1006/jsco.2002.0552.
  * [26] Harper R. Practical Foundations for Programming Languages, Cambridge University Press, 2013. ISBN-10:1107029570, 13:978-1107029576.
  * [27] Heyting A. Intuitionistische axiomatick der projectieve meetkunde, Thesis, P. Noordhoof, 1925.
  * [28] Heyting A. _Zur intuitionistischen Axiomatik der projektiven Geometrie_ , Mathematische Annalen, 1927\. 98:491–538. ISSN-0025-5831; 1432-1807/e.
  * [29] Heyting A. Untersuchungen über intuitionistische Algebra, Nederl. Akad. Wetensch. Verh. Tweede Afd. Nat. 18/2, 1941.
  * [30] Heyting A. Intuitionism, an Introduction, North - Holland, 1956.
  * [31] Ishihara H. _Informal Constructive Reverse Mathematics_ , CDMTCS Research Report 229, University of Auckland, 2004. ID-117964913.
  * [32] Jacobs B. _Bisimulation and Apartness in Coalgebraic Specification_ ; 1995 - Notes of lectures given in January 1995 at the joint TYPES/CLICS workshop in Gothenburg and BRICS seminar in Aarhus.
  * [33] Judson TW. Abstract Algebra Theory and Applications, Orthogonal Publishing L3C, 2015. ISBN-10:0989897591, 13:9780989897594.
  * [34] Lallement G. Semigroups and combinatorial applications, J. Wiley & Sons, New York, 1979.
  * [35] Lidl R, Pilz G. Applied abstract algebra, Springer, 1998.
  * [36] Martin-L$\ddot{o}$f P. _Constructive mathematics and computer programming_ , In Kohen L. J., Los J., Pfeiffer H., Podewski K. P., eds.: The Proceedings of the Sixth International Congress of Logic, Methodology and Philosophy of Science, North-Holland Publishing Company, Amsterdam. 1982\. 104:153–175. doi:10.1016/S0049-237X(09)70189-2.
  * [37] Mikhalev AV, Pilz GF. The Concise Handbook of Algebra, Springer Science + Business Media, B. V., 2002. ISBN:978-94-017-3267-3.
  * [38] Mines R, Richman F, Ruitenburg W. A Course of Constructive Algebra, New York: Springer-Verlag, 1988. ISBN-978-0-387-96640-3.
  * [39] Mitrović M. Semilattices of Archimedean Semigroups, University of Niš - Faculty of Mechanical Engineering, Niš, 2003.
  * [40] Mitrović M, Silvestrov S. _(Apartness) Isomorphism theorems for basic constructive algebraic structures with special emphasize on constructive semigroups with apartness - an overview_. In Silvestrov S., Malyarenko M., Rančić M., eds.: Stochastic Processes and Algebraic Structures -From Theory Towards Applications. Volume II: Algebraic Structures and Applications, Västerȧs and Stockholm, Sweden, October 4-6, Springer 2020 pp. 653–686. doi:10.1007/978-3-030-41850-2_28.
  * [41] Mitrović M, Silvestrov S, Crvenković S, Romano DA. _Constructive semigroups with apartness: towards new algebraic theory_ , Journal of Physics : Conference Series (JPCS), Volume 1194, 2019, 012076, doi:10.1088/1742-6596/1194/1/012076.
  * [42] M. A. Moshier, _A rational reconstruction of the domain of feature structures_ , J. of Logic, Language and Information, 1995. 4(2):111–143. doi:10.1007/BF01048617.
  * [43] Petrich M. Introduction to semigroups. Merill, Ohio, 1973.
  * [44] Putcha MS. _Paths in graphs and minimal $\pi$-sequences in semigroups_, Discrete Mathematics 1975. 11:173–185. doi:10.1016/0012-365X(75)90009-6.
  * [45] Reddy PS, Dawud M. _Applications of Semigroups_ , Global Journal of Science Frontier Research: F Mathematics and Decision Sciences, Volume 15, Issue 3, 2015. ISSN-2249-4626, 0975-5896.
  * [46] Richman F. _Constructive aspect of Noetherian rings_ , Proc. Am. Math. Soc., 1974. 44(2):436–441. doi:10.2307/2040452.
  * [47] Richman F. _Interview with a constructive mathematician_ , Modern Logic, 1996. 6(3):247–271. ID:118795904.
  * [48] Romano DA. _Rings and fields, a constructive view_ , Mathematical Logic Quarterly, 1988\. 34(1):25–40. doi:10.1002/malq.19880340105.
  * [49] Romano DA. _Construction of free Abelian groups_ , Radovi mat., 1988. 4(1):151–158.
  * [50] Romano DA. _Coequality relations, a survey_ , Bull. Soc. Math. Banja Luka, 1996. 3:1–36.
  * [51] Romano DA. _Some relations and subsets generated by principal consistent subset of semigroup with apartness_ , Univ. Beograd, Publ. Elektrotehn. Fak. Ser. Mat. 2002. 13:7–25. URL https://www.jstor.org/stable/43666560.
  * [52] Romano DA. _A note on family of quasi-antiorder on semigroup_ , Kragujevac J. Math., 2005. 27:11–18.
  * [53] Romano DA. _A note on quasi-antiorder on semigroup_ , Novi Sad J. Math., 2007. 37(1):3–8.
  * [54] Ruitenburg WBG. Intuitionistic Algebra, Theory and Sheaf Models, Utrecht, Ph.D. Thesis, May 1982, 143 pages, D. van Dalen (adviser).
  * [55] Ruitenburg W. _Inequality in Constructive Mathematics_ , Notre Dame Journal of Formal Logic, 1991. 32(4):533–553. doi:10.1305/ndjfl/1093635926.
  * [56] Schein BM. _On certain classes of semigroups of binary relations_ , Sibirskiǐ Matematicheskiǐ Zhurnal 1965. 6:616–635, (in Russian).
  * [57] Schein BM. Book Review - Social semigroups a unified theory of scaling and blockmodelling as applied to social networks (by J. P. Boyd), Semigroup Forum, 1997. 54:264–268. ISSN-0037-1912; 1432-2137/e.
  * [58] Shevrin LN. Semigroups. In Skornyakov L. A., ed.: “General Algebra”. Vol II, Nauka, Moscow, 1991 pp. 11–119 (Russian).
  * [59] Stolzenberg G. _Review of Foundations of constructive analysis_ , Bulletin of the American Mathematical Society 1970\. 76(2):301–323. doi:10.1090/S0002-9904-1970-12455-7.
  * [60] Tamura T. _Quasi-orders, generalized archimedeaness and semilattice decompositions_ , Math. Nachr. 1975. 68:201–220. doi:10.1002/mana.19750680115.
  * [61] Troelstra AS, van Dalen D. Constructivism in Mathematics, An Introduction, (two volumes), North - Holland, Amsterdam 1988. ISBN-9780444703583, 9780080955100.