# Atomism Axiomatised Using Mereological Composition as a Primitive Notion111I
would like to express my sincere gratitude to Achille Varzi for his time and
effort in providing his expertise and guidance, which have been instrumental
in shaping the final outcome of this work.

Marcin Łyczak

(The work was written during my scholarship at Columbia University under the
supervision of Achille Varzi (16.11.2022 - 8.12.2022) and was submitted to
Synthese on 16.03.2023.)

###### Abstract

Atomism is the view that everything is composed of atoms. The view within the
framework of the contemporary formal approach is expressed on the ground of
mereology with the use of the primitive notion of being a part as every object
has at least one atomic part [2, 48], [3, 145], [17, 42], or using
mereological fusion [16, 24] which is defined by being a part. We will briefly
present a discussion between A. Varzi and A. Shiver concerning the two
approaches and propose a new intuitive axiomatic characterization of atomism.
We build a system with a primitive notion of composition that holds between
individuals and pluralities. We assume only two specific axioms: each object
is a unique composition of unique atoms, and being a composition of some
objects is equivalent to being the composition of all atoms of these objects.
In our approach, notions of part, and atom, are secondary to composition: atom
is defined as an object that cannot be a composition of two or more objects,
and part is defined as inclusion between atoms. We will show that the theory,
with only these two specific axioms, is sufficient to adequately express
atomism as we prove that the theory is definitionally equivalent to atomistic
extensional mereology with plural quantification allowed and mereological
fusion defined. Our theory requires neither full comprehension schema nor the
existence of any specific compositions (there are models with only atoms).
Therefore, it may constitute the basis on which atomistic concepts of reality
are further strengthened, specifically those in which the notion of being a
part is not used. To the best of our knowledge, our proposal is the only
formal theory of atomism using the primitive notion of composition.

## Introduction

In philosophy, there are many different kinds of atomism. Here, we understand
atomism in a very general sense: as a view that claims that everything that
exists is either a simple object or is composed of simple objects, with the
assumption that something exists. Atomism is justified by different theories,
where we find various interpretations of the statement

$\mbox{{Everything is composed of atoms}}.$ ($\mathsf{AT1}$)

Atomism within the framework of the contemporary formal approach is usually
expressed on the ground of mereology, which is a formal theory of parts and
wholes, originally formulated by S. Leśniewski. The central notion of
mereology is mereological composition which is usually defined with the use of
the primitive notion of being a part/proper part. These notions are
appropriately specified in different versions of mereology. Loosely speaking,
the mereological composition of given objects is a concrete whole composed of
all of them, and only them. In contemporary literature [2, 48], [3, 145], [17,
42], however, atomism is formulated without using the notion of composition as

$\mbox{{Every object has at least one atomic part}}.$ ($\mathsf{AT2}$)

A. Shiver criticizes articulating atomism as ($\mathsf{AT2}$) and argues that
($\mathsf{AT1}$) should be expressed using mereological fusion [16]. However,
as A. Varzi shows, having only assumptions of reflexivity and the transitivity
of being a part and the definition of mereological composition: sum or fusion,
formal counterparts of ($\mathsf{AT1}$) and ($\mathsf{AT2}$) are equivalent
already in classical logic [24]. As Varzi pointed out, the main problem of the
models considered by Shiver against ($\mathsf{AT2}$) does not lie in the wrong
formulation of atomism by ($\mathsf{AT2}$), but that being a part is not well
founded.222Currently, more powerful variants of atomism called ‘superatomisms’
have been proposed by Cotnoir [6]. In superatomism, the proper part relation
is well-founded i.e. no descending chain of a proper parthood relation can be
infinite. This is being analyzed and developed [7, 23]. On the other hand,
gunky models of atomism are also being considered [20]. In models of this kind
every object is composed of atoms but some objects may be divided infinitely
into smaller and smaller parts, and all of these parts have an uncountable
number of their own parts. We follow Varzi’s view that atomism is a thesis
about composition, not decomposition [24] and direct our attention here to
atomism in a broad sense as just ($\mathsf{AT1}$). We believe that Varzi is
formally right, at the same time we agree with Shiver in that ($\mathsf{AT2}$)
does not intuitively express the atomistic position. In defend of
($\mathsf{AT2}$) at least two issues can be indicated: ($\mathsf{AT2}$) is
expressible in first-order logic, and it is not necessary to decide how
mereological composition is defined and what its properties are. However, that
from an intuitive point of view, mereological composition very clearly express
atomism. Shiver expresses atomism using defined notion of mereological fusion
that is secondary to being a part. We propose reformulating Shiver’s approach
and take mereological composition as the only primitive notion.333Let us note
that there are philosophical arguments for treating mereological composition
as primitive [8, 12], but they need not relate to ($\mathsf{AT1}$) and so we
will not discuss them here. We aim to:

  * •

find a formal system with a primitive notion $F$ of composition that holds
between individuals, and pluralities;

  * •

show that with this notion the standard mereological notions of part and atom
are definable, and primitive operator $F$ can be understood as a standard
composition;

  * •

show that the system is definitionally equivalent to standard system of
extensional atomistic mereology, in which plural quantification is allowed.

We begin with some remarks on mereological composition, atomistic mereology,
and the discussion between Shiver and Varzi (1). Next, we provide new
axiomatics for atomistic extensional mereology, where a formal counterpart of
($\mathsf{AT1}$) is an axiom, and the only primitive notion is composition
(2). Finally, we prove definitional equivalence of the presented system with
the standard axiomatization of atomistic extensional mereology in which plural
quantification is allowed (3).

##  1 Mereological composition, extensional mereology and atomicity

The first version of mereology was given by Leśniewski in a natural language
[13] (trans. in [14]). He later presented a mature version of mereology on the
ground of ontology, which is a theory of objects, expressed in a first-order
identity-free language. The only primitive notion of his ontology was a two-
place predicate $\varepsilon$ read ‘is’, applied to two names of the same
category. Leśniewski added to his system a primitive name-forming operator
$pt$ applied to names, read ‘part of’. The atomic expression $x\varepsilon
pt(y)$ is read ‘$x$ is a part of $y$’. The original Leśniewski’s ontological
approach to mereology is described by R. Urbaniak in [22]. A. Tarski extracted
mereology from its ontological context and treated mereology as a theory of
mathematical relational structures with the primitive relation of being a
part, and used this as a foundation for point-free geometric considerations
[21]. Mereology today is very willingly treated as just first-order theory
with identity, with the only primitive predicate for ‘is a part/proper part’.
This approach was described by P. Simons in [17], and more recently by Varzi
and Cotnoir [3]. While mentioned approaches differ, they share a common core
[26]. We focus on mereology which allows plural quantification described in
[3, 238-245]. Mereology with plural quantification has greater expressive
power than first-order mereology, what is used to formal analyzes of atomism
[7, 10]. Quantification over pluralities allows us to say that for any object,
there exist atoms from which the object is composed, and this is crucial for
our characterization of atomism. As we mentioned, the mereological composition
of given objects is a concrete of all of them, and only them, put together.
Mereological composition is a subject of actual philosophical studies
concerning, inter alia, its extensionality, the relationship between wholes
and their parts, the existence of arbitrary compositions, and the nature of
how objects are put together [1]. In the original mereology, to say that
something is a mereological composition of some objects Leśniewski used
$x\varepsilon Kl(y)$. What is important is that in the expression
$x\varepsilon Kl(y)$ both $x$ and $y$ are variables of the same category. In
modern first-order approaches, counterparts of non-empty names used by
Leśniewski are constructed with the use of formulas with at least one free
variable. To say that $x$ is a mereological composition of objects that are
$\varphi$, $F_{\varphi_{y}}x$ is used, where $y$ is a free variable in the
formula $\varphi$. In the case of mereology with plural quantification, there
is no need to use formulas with free variables, because plural variables play
their role. The mereological composition is expressed then as $F_{zz}x$, where
$zz$ is a plural variable and $x$ is individual variable. In the case of
mereological relational structures, the notation $xFX$ is used, where $F$ is a
relation between an element $x$ belonging to the domain of a given structure
and $X$ is a distributive subset of the domain.

Shiver formulates atomism using plural quantification and defined mereological
fusion. We follow the nomenclature from [3, 238-245] and use individual
variables: $x,y,z$, and plural ones: $xx,yy,zz,...$ . The logical symbols are
classical connectives, quantifiers, identity $=$ applied to individual
variables, and $\prec$ applied to individual and plural variables on the left
and right side, respectively. Expression $x\prec yy$ is read ‘$x$ is one of
$yy$’s’. The only non-logical symbol is $P$, for ‘is a part of’ applied to
individual variables. We assume as a base only axioms of two sorted logic and
axioms for first-order identity. Following Varzi [26], we call extensional
mereology the theory which has the following theses:

$\displaystyle Pxx,$ ($\mathtt{ref}$) $\displaystyle Pxy\land Pyz\to Pxz,$
($\mathtt{trans}$) $\displaystyle Pxy\land Pyx\to x=y,$ ($\mathtt{ants}$)
$\displaystyle\neg Pxy\to\exists z(Pzx\land\neg Ozy),$ ($\mathtt{ssp}$)

where $O$ is a predicate for ‘overlapping’ defined as

$Oxy:=\exists z(Pzx\land Pzy).$ ($O$)

We denote the set of theses of extensional mereology with plural
quantification as $\mathsf{EM}_{\mathsf{pl}}$ and we use the following
notation

$\mathsf{EM}_{\mathsf{pl}}=\eqref{ring}+\eqref{antising}+\eqref{transing}+\eqref{ssp}.$

Let us briefly comment extensional mereology. Formulas ($\mathtt{ref}$),
($\mathtt{trans}$), and ($\mathtt{ants}$) taken as axioms state that the
semantic correlate of predicate $P$ is a partial order relation. This is the
core of mereological theories which describe being a part in an inclusive
sense. Let us focus for a moment on ($\mathtt{ssp}$) and its properties.
Formula ($\mathtt{ssp}$) is called the strong supplementation principle and
was considered in the context of mereology by Simons [17, 28-29], however its
even stronger version was used as a mereological axiom already by Leśniewski
[19]. ($\mathtt{ssp}$) is a reinforcement of widely discussed in philosophical
literature [4] the weak supplementation principle

$PPxy\to\exists z(Pzy\land\neg Ozx),$ ($\mathtt{wsp}$)

where $PP$ is a predicate for ‘proper part’ defined as

$PPxy:=Pxy\land\neg x=y.$

The axiom ($\mathtt{ssp}$) is stronger than ($\mathtt{wsp}$) because assuming
partial order axioms for $P$ ($\mathtt{ssp}$) implies ($\mathtt{wsp}$); the
converse does not hold. Moreover, what is more important for us,
($\mathtt{ssp}$) added to partial order axioms for $P$ allows one to prove
(a): the equivalence of two formulations of mereological composition: sum and
fusion, which we will introduce soon, as well as ensuring that (b): if there
is a given sum, then it is unique, and (c): if there is a given fusion, then
it is unique. Of course, (a) implies (b)$\leftrightarrow$(c). However, weak
supplementation principle ($\mathtt{wsp}$) added to partial order axioms for
$P$ allows to prove only (b) (see e.g. [15]). Thus, ($\mathtt{ssp}$) is
convenient for building weak mereological theories that do not determine which
sums/fusions exist, while still guaranteeing their generally wanted
properties.

We introduce a definition of Leśniewski’s mereological sum $F_{zz}x$, read
‘$x$ is a mereological sum of $zz$’s’; and a definition of mereological fusion
$F^{\star}_{zz}x$, read ‘$x$ is a mereological fusion of $zz$’s’ in the
following way:

$\displaystyle F_{zz}x\leftrightarrow\forall_{z\prec zz}Pzx\land\forall
y(Pyx\to\exists_{z\prec zz}Ozy),$ ($\mathtt{Df}.F$) $\displaystyle
F^{\star}_{zz}x\leftrightarrow\forall y(Oyx\leftrightarrow\exists_{z\prec
zz}Ozy). $ ($\mathtt{Df}.F^{\star}$)

In general extensional mereology, after Leśniewski, it is assumed that for any
objects represented by any non-empty general name there exists (unique)
mereological composition of them [11]. Regardless of the definition of
composition and its existential assumptions, an atom is any object that has no
proper parts, which we define as

$\displaystyle Ax\leftrightarrow\forall y(Pyx\to x=y).$ ($\mathtt{Df}.A_{P}$)

Using the above we can express ($\mathsf{AT2}$) as

$\forall x\exists y(Pyx\land Ay).$ ($\mathtt{AT2}_{P}$)

To express atomism, which we want to discuss here, Shiver uses the notion of
fusion. Using plural quantification, he define plural constant $aa$ for
‘atoms’, which we introduce as an instantiation of comprehension schema

$x\prec aa\leftrightarrow Ax.$ ($\mathtt{Df}.aa_{P}$)

Moreover, Shiver uses the predicate $S$ for ‘being a fusion of atoms’

$Sx:=\exists_{yy\preccurlyeq aa}F^{\star}_{yy}x,$ ($S$)

where $\preccurlyeq$ is many-many predicate read as ‘$xx$’s are among $yy$’s’
that we define as

$xx\preccurlyeq yy:=\forall z(z\prec xx\to z\prec yy)\land\exists x(x\prec
xx).$

Atomistic standpoint ($\mathsf{AT1}$) my be expressed as

$\forall x(Sx).$

Shiver expresses the atomistic standpoint in slighty different way, which he
calls general atomicity, by the formula

$\forall x\exists y(Pxy\land Sy).$

This approach is analyzed by Varzi in first-order mereology in [24] (and later
also in [3, 145-147] and [10]). We express Varzi analysis in mereology with
plural quantification, because we want to be consistent with earlier and later
consideration. We take the notion of atoms as Shiver does, and we introduce a
notion of atomic parts of

$y\prec\mathfrak{at}_{x}\leftrightarrow Pyx\land y\prec aa.$
($\mathtt{Df}.\mathfrak{at}^{\mathsf{ind}}_{P}$)

Following Varzi’s considerations, having only ($\mathtt{ref}$) and
($\mathtt{trans}$), axiom ($\mathtt{AT2}_{P}$) implies

$\forall x(\forall
y(Oyx\leftrightarrow\exists_{z\prec\mathfrak{at}_{x}}Oyz)),$

and

$\forall x(\forall_{y\prec\mathfrak{at}_{x}}Pyx\land\forall
y(Pyx\to\exists_{z\prec\mathfrak{at}_{x}}Oyz)).$

These two formulas, applying the definitions of mereological fusion
($\mathtt{Df}.F^{\star}$) and sum ($\mathtt{Df}.F$), yields

$\forall x(\mathcal{F}_{\mathfrak{at}_{x}}x),\mbox{ for
}\mathcal{F}\in\\{F^{\star},F\\}.$ ($\mathtt{AT1}_{\mathcal{F}}$)

The above schema expresses atomism ($\mathsf{AT1}$) in both senses of
mereological composition: fusion and sum.
From ($\mathtt{AT1}_{\mathcal{F}}$) and the reflexivity of being a part
($\mathtt{ref}$) we infer

$\forall x\exists y\exists_{zz\preccurlyeq
aa}(Pxy\land\mathcal{F}_{zz}y),\mbox{ for }\mathcal{F}\in\\{F,F^{\star}\\}.$

When $\mathcal{F}$ is $F^{\star}$, we use definition ($S$) and obtain Shiver’s
formula for general atomicity.

Following Varzi [26] we call atomistic extensional mereology a theory which is
extensional mereology and has as a thesis ($\mathtt{AT2}_{P}$). We denote
atomistic extensional mereology with the definition of mereological sum
($\mathtt{Df}.F$) allowing plural quantification by
$\mathsf{AEM}_{\mathsf{pl}}$

$\mathsf{AEM}_{\mathsf{pl}}=\mathsf{EM}_{\mathsf{pl}}+\eqref{TA2P}+\eqref{dfAP}+\eqref{defF}.$

As we mentioned, in $\mathsf{EM}_{\mathsf{pl}}$ formulas characterizing
mereological fusion ($\mathtt{Df}.F^{\star}$) and mereological sum
($\mathtt{Df}.F$) are equivalent. So, in
$\mathsf{AEM}_{\mathsf{pl}}+\eqref{aaP}+\eqref{atP}$ it does not really matter
which definition of composition we take: ($\mathtt{AT2}_{P}$) implies
($\mathtt{AT1}_{\mathcal{F}}$), and the converse implication follows just from
the definition of mereological sum.

Before we move on to the main considerations, we would like to discuss the
issue of the primitive notions that are used to axiomatize mereology. As we
have said, popular approaches to mereology use the primitive notion of being a
part/proper part. Possible axiomatizations with this notions is still being
discussed [5, 11, 25]. The rich catalog of axiomatizations with the primitive
notions of being external, overlapping, as well as attempts to base mereology
on other primitive concepts is given in [18]. In the latter mereology is
expressed on the basis of Leśniewski’s ontology. The only known axiomatics
with the primitive notion of mereological composition is Lejewski’s single
axiom for general extensional mereology [18, 222]. In this case, the
quantification over function symbols is used, which is allowed in the full
original version of Leśniewski’s ontology. Thus, this axiom is not
translatable into the language of modern mereologies, in particular also into
the language that we use in our approach. We also believe that our axiomatics
has the advantage of being more intuitive than Lejewski’s equivalence axiom,
which in the Polish notation has seventy-seven symbols.

##  2 Theory $\mathsf{ATC}$. Axiomatization

Now we formulate an axiomatic theory of atomism in which the primitive notion
is composition. We do not assume the existence of any specific compositions:
our theory is open to axiomatic strengthening as needed. We express it on the
basis of a very small fragment of the logic of plurals $\mathsf{PFO}$ [9,
15-19] without comprehension schema, and without assumption of non-emptiness
of plurals. In other words, in our proposal, one can accept that axioms or
reject them.
The only non-logical symbol of our theory is $F$ for composition, used in the
context with individual variables, and plural terms. Plural terms are: plural
variables, $aa$ for ‘atoms’, and $\mathfrak{at}_{\boldsymbol{xx}}$ for ‘atoms
of which $\boldsymbol{xx}$’s are composed of’.
The following two are specific axioms of our theory:

$\displaystyle\forall x\exists_{zz\preccurlyeq
aa}(F_{zz}x\land\forall_{yy\preccurlyeq aa}(F_{yy}x\leftrightarrow zz\approx
yy)\land\forall y(F_{zz}y\to x=y)),$ ($\mathtt{ATC1}$) $\displaystyle
F_{zz}x\leftrightarrow F_{\mathfrak{at}_{zz}}x,$ ($\mathtt{ATC2}$)

where :

$\displaystyle x\prec aa\leftrightarrow\forall yy\forall_{z\prec
yy}(F_{yy}x\to z=x),$ ($\mathtt{Df}.aa_{F}$) $\displaystyle
x\prec\mathfrak{at}_{zz}\leftrightarrow\exists_{y\prec
zz}\exists_{yy\preccurlyeq aa}(F_{yy}y\land x\prec yy),$
($\mathtt{Df}.\mathfrak{at}^{\mathsf{pl}}_{F}$) $\displaystyle xx\preccurlyeq
yy:=\forall z(z\prec xx\to z\prec yy)\land\exists xx\prec xx$ ($\preccurlyeq$)
$\displaystyle zz\approx yy:=\forall x(x\prec zz\leftrightarrow x\prec yy).$
($\approx$)

Let us briefly comment on our axiomatization. ($\mathtt{ATC1}$) states that
everything is a unique composition of unique atoms. Atom is defined as an
object that cannot be a composition of two or more objects, and atoms of
$\boldsymbol{zz}$’s are defined as the sum of all atoms of all individuals
that are $\boldsymbol{zz}$. The axiom ($\mathtt{ATC1}$) is intended to capture
($\mathsf{AT1}$), but ($\mathtt{ATC1}$) itself does not guarantee that $F$ is
the mereological sum in Leśniewski’s sense. This is why we need one more
axiom. ($\mathtt{ATC2}$) states that the composition of some objects is
equivalent to the composition of the atoms of these objects. Formulas
($\mathtt{Df}.aa_{F}$) and ($\mathtt{Df}.\mathfrak{at}^{\mathsf{pl}}_{F}$) are
instantiations of comprehension schema of axioms.444In $\mathsf{PFO}$, the
comprehension schema is the following: $\exists x(A(x))\to\exists zz\forall
x(x\prec zz\leftrightarrow A(x))$, because in $\mathsf{PFO}$, all plurals must
be non-empty. We do not assume either the full comprehension schema or that
every plural must be non-empty. Our instantiations of comprehension schema
($\mathtt{Df}.aa_{F}$) and ($\mathtt{Df}.\mathfrak{at}^{\mathsf{pl}}_{F}$) do
not have in the predecessor non-emptiness assumption. However, our axioms
guarantee that $aa$ is non-empty, and if $F_{zz}x$, then also $zz$ and
$\mathfrak{at}_{zz}$ are non-empty. Pluralities $aa$ and
$\mathfrak{at}_{\boldsymbol{xx}}$ are not primitive, as they are defined using
the primitive mereological composition $F$.
We denote our axiomatic theory of atomistic compositions as $\mathsf{ATC}$, so

$\mathsf{ATC}=\eqref{AC1}+\eqref{AC2}+\eqref{dfaa}+\eqref{dfpl}$

As we show, this axiomatic theory of atomism is definitionally equivalent to
atomistic extensional mereology with plural quantification.

##  3 Definitional equivalence of $\mathsf{ATC}$ and
$\mathsf{AEM}_{\mathsf{pl}}$

From axiom ($\mathtt{ATC1}$) we know that each individual there is exactly one
plurality that is a unique composition of unique atoms

$\forall x\exists^{1}zz(zz\preccurlyeq
aa\land(F_{zz}x\land\forall_{yy\preccurlyeq aa}(F_{yy}x\leftrightarrow
zz\approx yy)\land\forall y(F_{zz}y\to x=y)),$

where $\exists^{1}zzA(zz)\leftrightarrow\exists zzA(zz)\land\forall xx\forall
yy(A(xx)\land A(yy)\to xx\approx yy)$.
We can, thus, introduce one place operation that to every $x$ attributes the
plurality of all atoms of $x$. For convenience, we use in $\mathsf{ATC}$ the
same constant symbol $\mathfrak{at}$ as it is used for the atoms of
pluralities. We have

$\mathfrak{at}_{x}\preccurlyeq aa\land
F_{\mathfrak{at}_{x}}x\land\forall_{yy\preccurlyeq aa}(F_{yy}x\leftrightarrow
yy\approx\mathfrak{at}_{x})\land\forall y(F_{\mathfrak{at}_{x}}y\to x=y).$
($\mathtt{Df}.\mathfrak{at}_{F}^{\mathsf{ind}}$)

Let us note, that theorem $\forall x(\mathfrak{at}_{x}\preccurlyeq aa)$
guarantee that pluralities $aa$, and $\mathfrak{at}_{x}$ are always non-empty.
To prove definitional equivalence, we conservatively extend $\mathsf{ATC}$ by
a definition of being a part. We do this using many-many inclusion among atoms
of two given objects as

$Pxy\leftrightarrow\mathfrak{at}_{x}\preccurlyeq\mathfrak{at}_{y},$
($\mathtt{Df}.P_{F}$)

which may be read as: $x$ is a part of $y$ iff all atoms of $x$ are atoms of
$y$.
Now we turn to the main goal. We formulate proofs using natural deduction.
First, we note that $\mathsf{ATC}$ characterizes being a part as a partial
order:

######  Lemma 1.

($\mathtt{ref}$), ($\mathtt{trans}$), and ($\mathtt{ants}$) are provable in
$\mathsf{ATC}+\eqref{dfP}$.

###### Proof.

To obtain ($\mathtt{ref}$) we note that from
($\mathtt{Df}.\mathfrak{at}_{F}^{\mathsf{ind}}$) we have $\exists
x(x\prec\mathfrak{at}_{x})$, thus
$\mathfrak{at}_{x}\preccurlyeq\mathfrak{at}_{x}$, from reflexivity of
$\preccurlyeq$ i.e. $Pxx$. ($\mathtt{trans}$) we obtain directly from
transitivity of $\preccurlyeq$. To prove ($\mathtt{ants}$) we assume $Pxy\land
Pyx$ and by ($\mathtt{Df}.P_{F}$) we obtain
$\mathfrak{at}_{x}\preccurlyeq\mathfrak{at}_{y}\land\mathfrak{at}_{y}\preccurlyeq\mathfrak{at}_{x}$
i.e. $\mathfrak{at}_{x}\approx\mathfrak{at}_{y}$, by ($\approx$ ‣ 2). We have
$F_{\mathfrak{at}_{y}}y$ from
($\mathtt{Df}.\mathfrak{at}_{F}^{\mathsf{ind}}$), so using it with
$\mathfrak{at}_{x}\approx\mathfrak{at}_{y}$ we obtain and
$F_{\mathfrak{at}_{x}}y$, by ($\mathtt{Df}.\mathfrak{at}_{F}^{\mathsf{ind}}$),
and next again using ($\mathtt{Df}.\mathfrak{at}_{F}^{\mathsf{ind}}$) we get
$x=y$. ∎

In the proofs of ($\mathtt{ssp}$) and ($\mathtt{Df}.F$) we use the following
$\mathsf{ATC}+\eqref{dfP}$ theses:

$\displaystyle z\prec aa\land
z\prec\mathfrak{at}_{x}\to\mathfrak{at}_{z}\preccurlyeq\mathfrak{at}_{x},$
($\mathtt{T1}$) $\displaystyle z\prec aa\land Ozy\to z\prec\mathfrak{at}_{y}.$
($\mathtt{T2}$)

###### Proof.

For ($\mathtt{T1}$) we assume $z\prec aa\land z\prec\mathfrak{at}_{x}$, and we
show $\mathfrak{at}_{z}\prec\mathfrak{at}_{x}$. $\mathfrak{at}_{z}$ is non-
empty, so fix any $y\prec\mathfrak{at}_{z}$. Then from
$y\prec\mathfrak{at}_{z}\land z\prec aa\land F_{\mathfrak{at}_{z}}z$ using the
definition of atoms ($\mathtt{Df}.aa_{F}$) we have $y=z$. The latter with
$z\prec\mathfrak{at}_{x}$ yields $y\prec\mathfrak{at}_{x}$, so
$\mathfrak{at}_{z}\preccurlyeq\mathfrak{at}_{x}$.
For ($\mathtt{T2}$) we assume $z\prec aa$ and $Pcz\land Pcy$ for some $c$, and
we prove $z\prec\mathfrak{at}_{y}$. From
($\mathtt{Df}.\mathfrak{at}_{F}^{\mathsf{ind}}$) we have
$F_{\mathfrak{at}_{z}}z$ and so using $z\prec aa$ and identity we have
$z\prec\mathfrak{at}_{z}\land\forall y(y\prec\mathfrak{at}_{z}\to y=z)$, so
the only atom of $\mathfrak{at}_{z}$ is $z$. Using this and
$\mathfrak{at}_{c}\preccurlyeq\mathfrak{at}_{z}$ taken from $Pcz$ and
($\mathtt{Df}.P_{F}$) we obtain $z\prec\mathfrak{at}_{c}$. The latter with
$\mathfrak{at}_{c}\preccurlyeq\mathfrak{at}_{y}$ taken from $Pcy$ and
($\mathtt{Df}.P_{F}$) yields $z\prec\mathfrak{at}_{y}$. ∎

We take the definition ($O$) of overlapping as in $\mathsf{AEM}_{\mathsf{pl}}$
and we show that the strong supplementation principle is a thesis of
$\mathsf{ATC}+\eqref{dfP}$.

######  Lemma 2.

($\mathtt{ssp}$) is provable in $\mathsf{ATC}+\eqref{dfP}$.

###### Proof.

Assume that $\forall z(Pzx\to Ozy)$. We aim to show that $Pxy$, that is,
$\forall_{u}(u\prec\mathfrak{at}_{x}\to u\prec\mathfrak{at}_{y}$). Thus, fix
an arbitrary $u\prec\mathfrak{at}_{x}$. Thus, since $u\prec aa$
$u\prec\mathfrak{at}_{x}$ gives
$\mathfrak{at}_{u}\preccurlyeq\mathfrak{at}_{x}$ by ($\mathtt{T1}$) i.e.,
$Pux$, by ($\mathtt{Df}.P_{F}$). So $Ouy$ by the assumption. We have $u\prec
aa$ and $Ouy$ thus $u\prec\mathfrak{at}_{y}$ by ($\mathtt{T2}$). In
consequence we have $\mathfrak{at}_{x}\preccurlyeq\mathfrak{at}_{y}$, i.e.
$Pxy$. ∎

Now we have to prove that notion of composition axiomatized in $\mathsf{ATC}$
is the mereological sum in the Leśniewski sense, i.e. we have to show that
($\mathtt{Df}.F$) is a thesis of $\mathsf{ATC}$.

######  Lemma 3.

$\forall_{z\prec zz}Pzx\land\forall y(Pyx\to\exists_{z\prec zz} Ozy)\to
F_{zz}x$ is a thesis of $\mathsf{ATC}+\eqref{dfP}$.

###### Proof.

We assume $\forall z(z\\!\prec\\!zz\to Pzx)\\!\land\\!\forall y(Pyx\to\exists
z(z\\!\prec\\!zz\land Ozy))$. From $\forall z(z\\!\prec\\!zz\to Pzx)$ by
($\mathtt{Df}.P_{F}$) we obtain $\forall
z(z\\!\prec\\!zz\to\mathfrak{at}_{z}\preccurlyeq\mathfrak{at}_{x})$ thus by
($\mathtt{Df}.\mathfrak{at}^{\mathsf{pl}}_{F}$) and
($\mathtt{Df}.\mathfrak{at}_{F}^{\mathsf{ind}}$) we have
$\mathfrak{at}_{zz}\preccurlyeq\mathfrak{at}_{x}$. We assume additionally that
$\mathfrak{at}_{zz}\not=\mathfrak{at}_{x}$, so
$c\prec\mathfrak{at}_{x}\land\neg c\prec\mathfrak{at}_{zz}$. From
$c\prec\mathfrak{at}_{x}$, ($\mathtt{Df}.aa_{F}$), and
($\mathtt{Df}.\mathfrak{at}_{F}^{\mathsf{ind}}$) we obtain
$\mathfrak{at}_{c}\preccurlyeq\mathfrak{at}_{x}$, so $Pcx$ by
($\mathtt{Df}.P_{F}$). Thus, from assumption, we have $\exists
z(z\\!\prec\\!zz\land Ozc)$. This with $c\prec aa$, symmetry of $O$ and (t2)
from earlier lemma yields $\exists z(z\prec zz\land c\prec\mathfrak{at}_{z})$,
$\forall z(F_{\mathfrak{at}_{z}}z)$ we have from
($\mathtt{Df}.\mathfrak{at}_{F}^{\mathsf{ind}}$) thus
$c\prec\mathfrak{at}_{zz}$ by ($\mathtt{Df}.\mathfrak{at}^{\mathsf{pl}}_{F}$)
which is false by assumption so $\mathfrak{at}_{zz}=\mathfrak{at}_{x}$. As
always, we have $F_{\mathfrak{at}_{x}}x$ from
($\mathtt{Df}.\mathfrak{at}_{F}^{\mathsf{ind}}$), so using
$\mathfrak{at}_{zz}=\mathfrak{at}_{x}$ and
($\mathtt{Df}.\mathfrak{at}_{F}^{\mathsf{ind}}$) we get
$F_{\mathfrak{at}_{zz}}x$ and so using ‘$\leftarrow$’ of ($\mathtt{ATC2}$) we
finally obtain $F_{zz}x$ which we wanted to prove. ∎

######  Lemma 4.

$F_{zz}x\to\forall_{z\prec zz}Pzx\land\forall y(Pyx\to\exists_{z\prec zz}
Ozy)$ is a thesis of $\mathsf{ATC}+\eqref{dfP}$.

###### Proof.

We assume $F_{zz}x$ and proceed indirectly. From ‘$\to$’ of ($\mathtt{ATC2}$)
we obtain $F_{\mathfrak{at}_{zz}}x$. Using
($\mathtt{Df}.\mathfrak{at}_{F}^{\mathsf{ind}}$) we get
$\forall_{yy}(F_{yy}x\to yy\approx\mathfrak{at}_{x})$, so we take
$\mathfrak{at}_{zz}/yy$ and we obtain
$\mathfrak{at}_{x}\approx\mathfrak{at}_{zz}$. If $\neg\forall z(z\prec zz\to
Pzx)$, then we take $c/z\colon c\prec zz\land\neg Pcx$. From $c\prec zz$ we
obtain that $\mathfrak{at}_{c}\preccurlyeq\mathfrak{at}_{zz}$ by
($\mathtt{Df}.\mathfrak{at}^{\mathsf{pl}}_{F}$) and
($\mathtt{Df}.\mathfrak{at}_{F}^{\mathsf{ind}}$). The latter with
$\mathfrak{at}_{x}\approx\mathfrak{at}_{zz}$ yields
$\mathfrak{at}_{c}\preccurlyeq\mathfrak{at}_{x}$, i.e. $Pcx$, which is false
by assumption. Now, if $\neg\forall y(Pyx\to\exists z(z\\!\prec\\!zz\land
Ozy))$, then we take $c/y$: $Pcx\land \forall z(z\\!\prec\\!zz\to \neg Ozc)$.
From $Pcx$ we have $\mathfrak{at}_{c}\preccurlyeq\mathfrak{at}_{x}$ and from
($\mathtt{ATC1}$) we have that some object is in atoms of both $c$ and $x$:
$d\prec\mathfrak{at}_{c}\land d\prec\mathfrak{at}_{x}$. From
$d\prec\mathfrak{at}_{x}$ and $\mathfrak{at}_{x}=\mathfrak{at}_{zz}$ we have
$d\prec\mathfrak{at}_{zz}$. From the latter and
($\mathtt{Df}.\mathfrak{at}^{\mathsf{pl}}_{F}$) there is $e\prec zz$ such that
$d\prec\mathfrak{at}_{e}$. From $\forall z(z\\!\prec\\!zz\to \neg Ozc)$ with
$z/e$ we get $e\prec zz\to \neg Oec$, so $\neg Oec$, i.e. $\forall
y(Pye\to\neg Pyc)$ so using ($\mathtt{Df}.P_{F}$) and $d/y$ we have
$\mathfrak{at}_{d}\preccurlyeq\mathfrak{at}_{e}\to
\neg\mathfrak{at}_{d}\preccurlyeq\mathfrak{at}_{c}$. We have
$d\prec\mathfrak{at}_{e}$ and $d\prec aa$, so by
($\mathtt{Df}.\mathfrak{at}_{F}^{\mathsf{ind}}$) we have
$\mathfrak{at}_{d}\preccurlyeq\mathfrak{at}_{e}$ and thus
$\neg\mathfrak{at}_{d}\preccurlyeq\mathfrak{at}_{c}$ but we have
$d\prec\mathfrak{at}_{c}$ so with $d\prec aa$ and
($\mathtt{Df}.\mathfrak{at}_{F}^{\mathsf{ind}}$) yields
$\mathfrak{at}_{d}\preccurlyeq\mathfrak{at}_{c}$. ∎

Now we conservatively extend $\mathsf{ATC}$ by adding the predicate for being
an atom

$Ax\leftrightarrow x\prec aa.$ ($\mathtt{Df}.A_{F}$)

It is clear that in $\mathsf{ATC}$, formula ($\mathtt{AT2}_{P}$) is a thesis
because of ($\mathtt{ATC1}$) and ($\mathtt{Df}.aa_{F}$). Moreover, having
($\mathtt{Df}.F$) in $\mathsf{ATC}$ we can easily prove that equivalence
($\mathtt{Df}.aa_{P}$) is a thesis, and
($\mathtt{Df}.\mathfrak{at}^{\mathsf{ind}}_{P}$) may be proved with the use of
($\mathtt{Df}.\mathfrak{at}_{F}^{\mathsf{ind}}$). Thus, using lemmas 1-4 we
obtain that $\mathsf{AEM}_{\mathsf{pl}}$ is a subtheory of $\mathsf{ATC}$
conservatively extended by definitions: ($\mathtt{Df}.P_{F}$) of being a part
and ($\mathtt{Df}.A_{F}$) of predicate $A$:

######  Theorem 1.

$\mathsf{AEM}_{\mathsf{pl}}+\eqref{aaP}+\eqref{atP}\subseteq\mathsf{ATC}+\eqref{dfP}+\eqref{AF}$.

Now we are going to prove converse dependency. First, we show that the
mereological sum in $\mathsf{AEM}_{\mathsf{pl}}$ is extensional

######  Lemma 5.

$\forall xx\forall yy\forall z(xx\approx yy\land F_{xx}z\to F_{yy}z)$ is
provable in $\mathsf{AEM}_{\mathsf{pl}}$.

###### Proof.

We assume $F_{zz}x\land zz\approx yy$ and $\neg F_{yy}x$ We obtain (a):
$\forall z(z\prec zz\to Pzx)$ (b): $\forall y(Pyx\to\exists z(z\prec zz\land
Ozy))$, (c): $\neg\forall z(z\prec yy\to Pzx)\lor\neg\forall y(Pyx\to\exists
z(z\prec yy\land Ozy))$. If $\neg\forall z(z\prec yy\to Pzx)$ then we take
$c/z\colon c\prec yy\land\neg Pcx$, so $c\prec zz$ by $zz\approx yy$ but then
using (a) we have $Pcx$ which is false. Therefore, we have $\forall z(z\prec
yy\to Pzx)$ so using (c) we obtain $\neg\forall y(Pyx\to\exists z(z\prec
yy\land Ozy))$ we take $d/y\colon Pdx\land\forall z(z\prec yy\to\neg Ozd)$.
From $Pdx$ and (b) we have that $\exists z(z\prec zz\land Ozd)$ so we take
$e/z\colon$ $e\prec zz\land Oed$. From $e\prec zz$ and $zz\approx yy$ we have
$e\prec yy$ thus using $\forall z(z\prec yy\to\neg Ozd)$ we obtain $\neg Oed$
which yields a contradiction. ∎

As we see, all we needed was $\approx$ and logical axioms. Now we show that in
$\mathsf{AEM}_{\mathsf{pl}}$ with appropriate definitions everything is a
unique composition of unique atoms:

######  Lemma 6.

($\mathtt{ATC1}$) is provable in
$\mathsf{AEM}_{\mathsf{pl}}+\eqref{aaP}+\eqref{atP}$.

###### Proof.

From Varzi’s analysis we have ($\mathtt{AT1}_{\mathcal{F}}$) i.e.
$F_{\mathfrak{at}_{x}}x$ and $\mathfrak{at}_{x}\preccurlyeq aa$. The
uniqueness of a mereological sum holds in extensional mereology, as we note in
the section 1, thus $\forall y(F_{\mathfrak{at}_{x}}y\to x=y)$. From
$F_{\mathfrak{at}_{x}}x$ and lemma 5 we obtain $\forall_{yy\preccurlyeq
aa}(yy\approx\mathfrak{at}_{x}\to F_{yy}x)$, thus all we need to show is
$\forall_{yy\preccurlyeq aa}(F_{yy}x\to yy\approx\mathfrak{at}_{x})$. We
assume indirectly that $\neg\forall_{yy\preccurlyeq aa}(F_{yy}x\to
yy\approx\mathfrak{at}_{x})$ take $cc/yy$ and obtain $cc\preccurlyeq aa\land
F_{cc}x\land cc\not=\mathfrak{at}_{x}$. From $cc\not=\mathfrak{at}_{x}$ and
($\approx$ ‣ 2) we have $\exists z(z\prec cc\land\neg
z\prec\mathfrak{at}_{x}\lor\neg z\prec cc\land z\prec\mathfrak{at}_{x})$. We
take $c/z$ and we have two possibilities (a): $c\prec cc\land\neg
c\prec\mathfrak{at}_{x}$ or (b): $\neg c\prec cc\land
c\prec\mathfrak{at}_{x}$. We start with (a). From $F_{cc}x$ and the definition
of mereological sum ($\mathtt{Df}.F$) we obtain $\forall z(z\prec cc\to Pzx)$
thus using $c\prec cc$ we have $Pcx$. From $F_{\mathfrak{at}_{x}}x$ and
($\mathtt{Df}.F$) we have $\forall y(Pyx\to\exists
z(z\prec\mathfrak{at}_{x}\land Ozy)$ so using $Pcx$ we have $\exists
z(z\prec\mathfrak{at}_{x}\land Ozc)$ we take $d/z:$
$d\prec\mathfrak{at}_{x}\land Odc$. Both $c$ and $d$ are atoms, so from $Odc$
with the use of ($\mathtt{Df}.aa_{F}$) we have $c=d$. Thus from
$d\prec\mathfrak{at}_{x}$ we obtain $c\prec\mathfrak{at}_{x}$ which yields a
contradiction. In the case of (b) from $c\prec\mathfrak{at}_{x}$ and
($\mathtt{Df}.\mathfrak{at}_{P}^{\mathsf{pl}}$) we obtain $Pcx$. Next from
$F_{cc}x$ and definition of sum ($\mathtt{Df}.F$) we obtain $\forall
y(Pyx\to\exists z(z\prec cc\land Ozy))$. We take $c/z$ and using $Pcx$ we
obtain $\exists z(z\prec cc\land Ozc)$ We take $d/z$ and so $d\prec cc\land
Odc$. We know that $c$ is an atom because of $c\prec\mathfrak{at}_{x}$, and
$d$ is an atom because of $d\prec cc$ and $cc\preccurlyeq aa$, so $Ocd$ yields
$c=d$ and this with $d\prec cc$ yields $c\prec cc$ which yields a
contradiction with assumption. ∎

To prove ($\mathtt{ATC2}$) in $\mathsf{AEM}_{\mathsf{pl}}$ we need to
introduce the notion of atoms of $\boldsymbol{xx}$’s and we take the following
instantiation of comprehension schema

$y\prec\mathfrak{at}_{xx}\leftrightarrow\exists_{z\preccurlyeq xx}(Pyz\land
y\prec aa).$ ($\mathtt{Df}.\mathfrak{at}_{P}^{\mathsf{pl}}$)

Now we prove that, in atomistic extensional mereology with plural
quantification, being the mereological sum of some objects is equivalent with
mereological sum of atoms of these objects. Implication ‘$\leftarrow$’
requires the use of ($\mathtt{ssp}$).

######  Lemma 7.

$F_{\mathfrak{at}_{zz}}x\to F_{zz}x$ is provable in
$\mathsf{AEM}_{\mathsf{pl}}+\eqref{aaP}+\eqref{atP}+\eqref{dfatP}$.

###### Proof.

We assume $F_{\mathfrak{at}_{zz}}x$ and indirectly we assume $\neg F_{zz}x$.
We obtain the following (a): $\forall z(z\prec\mathfrak{at}_{zz}\to Pzx)$,
(b): $\forall y(Pyx\to\exists z(z\prec\mathfrak{at}_{zz}\land Ozy))$ and (c):
$\neg\forall z(z\prec zz\to Pzx)\lor\neg\forall y(Pyx\to\exists z(z\prec
zz\land Ozy))$. If it were the case that $\neg\forall z(z\prec zz\to Pzx)$
then we take $c/z$ and we have $c\prec zz\land\neg Pcx$. From $\neg Pcx$ and
($\mathtt{ssp}$) we obtain that there is $d$ such that $Pdc\land\neg Odx$.
From ($\mathtt{AT2}_{P}$) there is an atom of $d$: $Ae\land Ped$. From the
latter and $Pdc$ using ($\mathtt{trans}$) we have $Pec$. So, we have $c\prec
zz\land Pec\land Ae$ and thus using
($\mathtt{Df}.\mathfrak{at}_{P}^{\mathsf{pl}}$) we obtain
$e\prec\mathfrak{at}_{zz}$. The latter with (a) yields $Pex$, which is false
because we have $Ped\land\neg Odx$. So $\forall z(z\prec zz\to Pzx)$ and next
by (c): we obtain $\neg\forall y(Pyx\to\exists z(z\prec zz\land Ozy))$. We
take $f/y$ and so $Pfx\land\forall z(z\prec zz\to\neg Ozf)$. From $Pfx$ and
(b) we have $\exists z(z\prec\mathfrak{at}_{zz}\land Ozf)$ and we obtain
$g/z:g\prec\mathfrak{at}_{zz}\land Ofg$. From $g\prec\mathfrak{at}_{zz}$ and
($\mathtt{Df}.\mathfrak{at}^{\mathsf{ind}}_{P}$) we obtain that there is
$h\prec zz$ such that $Pgh\land Ag$. We have $Ofg$ so with $Ag$ using
definitions ($\mathtt{Df}.A_{P}$) and ($O$) we obtain $Pgf$. The latter,
combined with $Pgh$ which was obtained earlier yields $Ohf$. We have $h\prec
zz$ so using $\forall z(z\prec zz\to\neg Ozf)$ we obtain $\neg Ohf$ which
yields a contradiction. ∎

######  Lemma 8.

$F_{zz}x\to F_{\mathfrak{at}_{zz}}x$ is provable in
$\mathsf{AEM}_{\mathsf{pl}}+\eqref{aaP}+\eqref{atP}+\eqref{dfatP}$.

###### Proof.

We proceed indirectly. We assume $F_{zz}x$ and $\neg F_{\mathfrak{at}_{zz}}x$
and we obtain (a): $\forall z(z\prec zz\to Pzx)$, (b): $\forall
y(Pyx\to\exists z(z\prec zz\land Ozy))$ and also we have (c): $\neg\forall
z(z\prec\mathfrak{at}_{zz}\to Pzx)\lor\neg\forall y(Pyx\to\exists
z(z\prec\mathfrak{at}_{zz}Ozy))$. If it were the case that $\neg\forall
z(z\prec\mathfrak{at}_{zz}\to Pzx)$ then we take $c/x$ and so
$c\prec\mathfrak{at}_{zz}\land\neg Pcx$. From $c\prec\mathfrak{at}_{zz}$ and
definition of ($\mathtt{Df}.\mathfrak{at}_{P}^{\mathsf{pl}}$) we have that
there is $d\prec zz$ with $Pcd\land Ac$. From (a) and $d\prec zz$ we obtain
$Pdx$, so using $Pcd$ and ($\mathtt{trans}$) we obtain $Pcx$, which is false,
so $\forall z(z\prec\mathfrak{at}_{zz}\to Pzx)$ and next by (c) $\neg\forall
y(Pyx\to\exists z(z\prec\mathfrak{at}_{zz}\land Ozx))$. We take $e/y\colon
Pex\land\forall z(z\prec\mathfrak{at}_{zz}\to\neg Oze)$. From $Pex$ and (b) we
obtain $\exists z(z\prec zz\land Oze)$ We take $f/z$ and so $f\prec zz\land
Ofe$. From $Ofe$ we obtain $Pge\land Pgf$. From ($\mathtt{AT2}_{P}$) we obtain
that there is an atom of $g$: $Ah\land Phg$ from ($\mathtt{trans}$) we obtain
$Phe\land Phf$. We have $Phf\land f\prec zz\land Ah$ and by using
($\mathtt{Df}.\mathfrak{at}_{P}^{\mathsf{pl}}$) we get
$h\prec\mathfrak{at}_{zz}$. The latter with $\forall
z(z\prec\mathfrak{at}_{zz}\to\neg Oze)$ yields $\neg Ohe$, which yields a
contradiction with $Phe$. ∎

To end the proof we need to note a few more things. The notions of being a
part ($\mathtt{Df}.P_{F}$), atoms ($\mathtt{Df}.aa_{F}$), and atoms of:
($\mathtt{Df}.\mathfrak{at}_{F}^{\mathsf{ind}}$) and
($\mathtt{Df}.\mathfrak{at}^{\mathsf{pl}}_{F}$) in $\mathsf{ATC}$ are theses
of $\mathsf{AEM}_{pl}+\eqref{dfatP}$. ($\mathtt{Df}.P_{F}$) in one direction
follows just from ($\mathtt{trans}$) and conversely we have to use
($\mathtt{ssp}$) and ($\mathtt{AT2}_{P}$). ($\mathtt{Df}.aa_{F}$) follows from
the defined mereological sum ($\mathtt{Df}.F$), being an atom
($\mathtt{Df}.aa_{P}$) and the fact $\forall x(F_{\mathfrak{at}_{x}}x)$ proved
by Varzi. We have proved ($\mathtt{Df}.\mathfrak{at}_{F}^{\mathsf{ind}}$) in
lemma 6, and ($\mathtt{Df}.\mathfrak{at}^{\mathsf{pl}}_{F}$) can be easily
proved with the use of the definition of atom ($\mathtt{Df}.A_{P}$), atoms of
($\mathtt{Df}.\mathfrak{at}_{P}^{\mathsf{pl}}$), mereological sum
($\mathtt{Df}.F$) and the fact that in
$\mathsf{AEM_{\mathsf{pl}}}+\eqref{aaP}+\eqref{atP}$ we have $\forall
x(F_{\mathfrak{at}_{x}}x)$. Lastly, we note
($\mathtt{Df}.\mathfrak{at}_{P}^{\mathsf{pl}}$) is a thesis of $\mathsf{ATC}$,
and it can be proved with the use of
($\mathtt{Df}.\mathfrak{at}_{F}^{\mathsf{ind}}$), ($\mathtt{Df}.F$),
($\mathtt{Df}.\mathfrak{at}^{\mathsf{pl}}_{F}$), and ($\mathtt{Df}.P_{F}$).
Thus, using lemmas 5-8 we obtain that axiomatic theory of atomism
$\mathsf{ATC}$ presented herein, when extended by appropriate definitions is a
subtheory of atomistic extensional mereology:

######  Theorem 2.

$\mathsf{ATC}+\eqref{dfP}+\eqref{AF}\subseteq\mathsf{AEM}_{\mathsf{pl}}+\eqref{aaP}+\eqref{atP}+\eqref{dfatP}$.

Using theorems 1 and 2 we obtain the final result of the work that out theory
and atomistic extensional mereology extended with appropriate instantiations
of comprehension schema are definitionally equivalent

$\mathsf{ATC}+\eqref{dfP}+\eqref{AF}=\mathsf{AEM}_{\mathsf{pl}}+\eqref{aaP}+\eqref{atP}+\eqref{dfatP}.$

As we mentioned, in extensional mereology fusion ($\mathtt{Df}.F^{\star}$) and
sum ($\mathtt{Df}.F$) are equivalent. So $\mathsf{ATC}+\eqref{dfP}+\eqref{AF}$
is also equivalent to
$\mathsf{AEM}_{\mathsf{pl}}+\eqref{aaP}+\eqref{atP}+\eqref{dfatP}$ with fusion
instead of sum.

Perhaps some atomists would prefer to stay in first-order logic without plural
quantification. However, plural quantification in the case of atomism has its
advantages. First, it is open to the axiomatic characterization of
superatomism [7]. Second, as we have shown, atomism does not need to be based
on the primitive notion of being a part. Finally, we believe that it captures
both formally and intuitively what ($\mathsf{AT1}$) is meant to express.

In conclusion, we also wish to emphasize that though our axiomatic system
$\mathsf{ATC}$ for atomism is equivalent to atomistic extensional mereology
with plural quantification, $\mathsf{ATC}$ it is based on two axioms that
cannot be proven in any formulation of pure extensional mereology. However,
general exstensonal mereology can also be axiomatized, in plural logic, using
fusion as the primitive concept [27].

## References

  * [1] Carrara, M., Lando, G. (2021) S.I.: “Mereology and Identity”, Synthese, 198 (18): 4205–4227
  * [2] Casati, R., Varzi, A. (1999) Parts and Places. The Structures of Spatial Representation, MIT Press, Cambridge (MA), 1999
  * [3] Cotnoir, A., Varzi, A. (2021) Mereology, Oxford University Press
  * [4] Cotnoir A. (2021) “Is Weak Supplementation Analytic?”, Synthese, 198(18): 4229-4245
  * [5] Cotnoir, A., Varzi, C. A. (2018) “Natural Axioms for Classical Mereology”, Review of Symbolic Logic, 12(1) 201–208
  * [6] Cotnoir, A. (2013) “Beyond Atomism”, Thought, 2(1): 67–72
  * [7] Dixon, T. (2020) “Between Atomism and Superatomism”, Journal of Philosophical Logic, 49(6): 1215–1241
  * [8] Fine, K. (2010) “Towards a Theory of Part”, Journal of Philosophy, 107(11): 559–589
  * [9] Florio, S. Linnebo, Ø. (2021) The Many and the One: A Philosophical Study of Plural Logic, Oxford: Oxford University Press
  * [10] Giordani, A., Calosi, C. (2023) “Atoms, Combs, Syllables and Organisms”, Philosophical studies, 180:1995–2024
  * [11] Hovda, P. (2008) “What is Classical Mereology?”, Journal of Philosophical Logic, 38(1): 55–82
  * [12] Kleinschmidt, S. (2019) “Fusion First”, Noûs, 53(3): 689-707
  * [13] Leśniewski, S. (1916) Podstawy ogólnej teoryi mnogości. I [Foundations of the general theory of sets. I], Prace Polskiego Koła Naukowego w Moskwie: Moskwa 1” [On the foundations of mathematics], Przegląd Filozoficzny, XXX: 164–206
  * [14] Leśniewski, S. (1992) Collected Works I; Surma, S.J., Srzednicki, J.T., Barnett, D.I., Rickey, V.F., Eds.; Kluwer: Dordrecht, The Netherlands
  * [15] Loss, R. (2021) “Two Notions of Fusion and the Landscape of Extensionality”, Philosophical Studies, 178(10): 3443–3463
  * [16] Shiver, A. (2014) “How do You Say “Everything is Ultimately Composed of Atoms”?”, Philosophical Studies, 172(3): 607–614
  * [17] Simons, P. (1987) Parts: A Study in Ontology, Oxford: Clarendon Press.
  * [18] Sobociński, B. (1984) “Studies in Leśniewski’s Mereology”, In: Srzednicki, J.T.J., Rickey, V.F. (eds) Leśniewski’s Systems. Nijhoff International Philosophy Series, vol. 13, Dordrecht: Springer
  * [19] Świętorzecka, K., Łyczak, M. (2020) “Mereology with Super-Supplementation Axioms. A Reconstruction of the Unpublished Manuscript of Jan F. Drewnowski”, Logic and Logical Philosophy, 29(2): 189–211
  * [20] Tsai, H., Varzi, A. (2015) “Atoms, Gunk, and the Limits of “Composition””, Erkenntnis, 81(2): 231–235
  * [21] Tarski, A. (1956) “Foundations of the Geometry of Solids”, in: Logic, Semantics, Metamathematics. Papers from 1923 to 1938, Oxford, 1956, 24–29
  * [22] Urbaniak R. (2014) Leśniewski’s Systems of Logic and Foundations of Mathematics, Springer
  * [23] Uzquiano, G. (2017) “Atomism and Composition”, Thought, 6(4): 232–40
  * [24] Varzi, A. (2017) “On Being Ultimately Composed of Atoms”, Philosophical Studies, 174(11): 2891–2900
  * [25] Varzi, A. (2019) “On Three Axiom Systems for Classical Mereology”, Logic and Logical Philosophy, 28(2): 203–207
  * [26] Varzi, A. (2019) “Mereology”, The Stanford Encyclopedia of Philosophy (Spring 2019 Edition), E. Zalta (ed.), https://plato.stanford.edu/archives/spr2019/entries/mereology/
  * [27] Varzi, A., Łyczak, M. (2022) “Fusion as a Primitive Notion of General Extensional Mereology” (unpublished manuscript created during Marcin Łyczak internship at Columbia University 16.11.2022- 8.12.2022)