=Paper=
{{Paper
|id=Vol-3249/paper6-FOUST
|storemode=property
|title=On the Analysis of FORT; Arguments, Alignment to FOs, and CLIF
Validation
|pdfUrl=https://ceur-ws.org/Vol-3249/paper6-FOUST.pdf
|volume=Vol-3249
|authors=Fatme Danash,Danielle Ziebelin
|dblpUrl=https://dblp.org/rec/conf/jowo/DanashZ22
}}
==On the Analysis of FORT; Arguments, Alignment to FOs, and CLIF
Validation==
https://ceur-ws.org/Vol-3249/paper6-FOUST.pdf
On the Analysis of FORT; arguments, alignment to
FOs, and CLIF validation
Fatima Danash1,2 , Danielle Ziebelin1,2
1
Université Grenoble Alpes, Grenoble 38000, France
2
LIG, Laboratoire d’Informatique de Grenoble, Grenoble 38000, France
Abstract
Foundational relations are formal and generic relations presenting a basic pillar of foundational ontologies
(FOs). The employment of these relations in practice has become widely prevalent by means of FOs.
However, for the utilization of sole foundational relations, we believe that a basis done exclusively on a FO
is unsatisfactory due to (1) the difficulties that modelers face upon selecting a FO for practice, and (2) the
fact that no FO incorporates inclusively the basic set of foundational relations in which we are interested.
Hence, we have proposed in an earlier work an entity-type-free minimal set of Foundational Ontological
Relations Theory (FORT). In this paper, we expound on the two arguments for FORT, compare and
elucidate an alignment between FORT’s micro-theories and the relation-based content of some FOs, and
associate FORT with a CLIF-serialization that validates the consistency of the theory.
Keywords
Foundational Relations, FORT, Foundational Ontologies, Common Logic, CLIF
1. Introduction
Foundational relations are formal and generic relations that play a fundamental role in the
ontological foundations of conceptual modeling. These relations have been highly investigated
in the applied ontological and philosophical literature, such as the parthood and connection
relations in mereological and topological theories.
The practice in foundational relations as a language of primitive relations and rule constraints
has shown itself convenient in several application domains, such as contextualizing parthood
typologies in cognitive sciences [1], linguistics [2], ontology [3], and conceptual modeling [4].
Depending on the requirements of the intended application domain, the needed foundational
relations are specified, (re-)formalized, and (re-)used. For the application of our approach, we
are specifically interested in the relations that are imperative for the representation-of and
reasoning-over the structural, semantic, and spatial constraints of an entity, across any domain.
This comprises modeling the link between; an entity as a whole and its different inseparable
parts; an entity as collective whole and the entities that it groups under certain semantics;
an entity and its constituents; an entity and the spatial region that locates it; and the spatial
constraints among entities. To be applicable on an entity across any domain, this requires that
the relations be generic i.e. independent of relata types. Hence, we target the following set of
The Eighth Joint Ontology Workshops (JOWO’22), August 15-19, 2022, Jönköping University, Sweden
Envelope-Open fatme.danash@univ-grenoble-alpes.fr (F. Danash); danielle.ziebelin@univ-grenoble-alpes.fr (D. Ziebelin)
© 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
CEUR
Workshop
Proceedings
http://ceur-ws.org
ISSN 1613-0073
CEUR Workshop Proceedings (CEUR-WS.org)
foundational relations; parthood, dependence, constitution, membership, and location with the
formal properties and relations that are required to characterize them.
Moreover, foundational relations, together with general primitive concepts, form the pillars of
foundational ontologies (FOs) aka upper/top-level ontologies. Nowadays, FOs are establishing
forward the development of specific (core, domain, and application) ontologies and ontology-
driven conceptual models i.e. enhancing the construction of models that are compliant with
FOs and their ontological commitments, which guarantees their validation. In addition to that,
achieving interoperability between models is reinforced upon the employment of FOs such as
in the integration of different ontologies that comply to a unique FO in inter-disciplinary fields.
As a consequence, the employment of foundational relations has become widely prevalent by
means of FOs, where a unique set of relations is offered and formalized in each.
Although some relations are commonly addressed among FOs, this set varies according to
the ontological commitments made by each FO. For instance, a FO that revokes the co-existence
of multiple individuals in the same space-time would treat the relation between a constituent
and the constituted entity as an identity but not a constitution, and thus rejects the inclusion
of constitution within its set of foundational relations. Thus, it is noticed that no FO covers
completely the set of foundational relations in which we are interested (1). In addition to that,
upon selecting a FO for practice, it is often recognized that modelers do face some complications
concerning the complexity of the FO, the obligation to conform to the ontological commitments
of the FO, and the concept-hierarchy mappings (2).
Based on the two preceding issues, we believe that for the representation and employment of
solely foundational relations in general, and the mentioned set of relations in particular, a basis
done exclusively on a FO is unsatisfactory.
Hence, in [5], we have posed our research problem of why not have a theory of pure founda-
tional relations besides large complex FOs. And to overcome this problem, we have proposed
an entity-type free theory of a minimal set of foundational ontological relations (FORT). The
approach followed for the development of FORT includes a methodology of four steps to be ac-
complished. In [5], we have successfully achieved the first step; formalizing FORT in first-order
logic (FOL) as the expressive logical language for the specification of formal theories such as
FOs. For that, we have selected, characterized, and axiomatized the minimal set of relations
that establish FORT. In this paper, we first present FORT briefly (Section 2) for the reader to
have the formalization available. Then we proceed with the second step of the methodology;
expounding the arguments for FORT that derive from the two challenges that modelers face
upon using FOs for the sake of foundational relations (Section 3); elucidating an alignment
between FORT’s micro-theories and the relation-based content of some FOs (Section 4); and
associating FORT with a CLIF-serialization as a Common Logic [6] ontology that validates
the existence of models for FORT using consistency checks (Section 5). Whereas the third
and fourth steps of the methodology are in progress and involve; FORT’s translation into a
decidable knowledge representation language that supports reasoning and inference services
(an SROIQ-DL specification); and its implementation in an ontological language supporting its
practices in ontology-driven conceptual modeling tasks (an OWL2-DL ontology).
Therefore, the contributions of this paper are twofold; (a) the positioning and alignment of
FORT with respect to some FOs, and (b) the validation of FORT’s consistency while providing a
CLIF-serialization.
Figure 1: FORT’s relation modules, their interlinks (plain lines) and participation, as axioms in the
formalization of other relations (dotted lines).
2. Preliminary work; FORT
In this section, we illustrate briefly the work done around FORT in [5]. FORT is group of
intralinked relation micro-theories, also called ontology modules, that are interlinked as shown
in figure 1. FORT as a theory presents a minimal set of foundational ontological relations that
are free of entity-types. It is intended to aid modelers who aim to use foundational relations
in practice, without wanting to commit to a set of entity-types upon using a FO. This is by
importing FORT as a language of primitive relations and rule constraints into the user’s model
(which represents a certain application using domain-specific categories and links).
In the following, we clarify some characteristics of FORT. First, the notion of intralinked
relation micro-theories corresponds to a group of definitions, axioms, and theorems that char-
acterize our view (ontological analysis) of a specific relation. Theoretically, each relation has
been thoroughly discussed taking into account its literary ontological and philosophical work.
Empirically then, the relation has been formalized by importing, reusing and adapting extant
theories according to our ontological analysis and requirements.
Second, the notion of interlinked micro-theories corresponds to links drawn between the rela-
tions of each micro-theory using axioms.
Third, the notion of entity-type free corresponds to the theory not committing to specific kinds,
aka categories, for the entities participating in the relation; the domain and range of relations.
Instead, FORT characterizes formally the relations by normalizing constraints on the relata
of the relation upon their identification in practice. This is done by introducing axioms that
project restrictions on the types that will be allocated for each relation while used in conceptual
models, since the theory’s utilization is intended as a. This makes the theory straightforward to
integrate within extant theories, without obliging the compliance to a hierarchy of entity types.
Fourth, a basic assumption that FORT makes is to distinguish the parthood relation from mem-
bership and constitution. This demarcation is adopted to (a) refrain a philosophical debate on
the consideration of these relations as part-whole typologies, (b) delimit the scopes upon which
transitivity holds, and (c) advocate for the additional semantics that each relation acquires
divergent from one another.
The axiomatization of FORT’s micro-theories is briefly illustrated in the appendix section (with-
out presenting that of imported theories i.e. the closure extensional mereology (CEM), the
minimal mereotopology (MT), and Varzi’s location (L) theories).
At this point, one might argue that FORT is just a repository of relations gathered as a grab-bag
ontology. However, FORT offers more than just a repository; (1) positioning FORT concerning
the well-known literary work on foundational relations where the analysis and valorization
of extant work have been performed; (2) analyzing the requirements in the ontology-driven
conceptual modeling context in general, and concerning our motivation in particular, where
the selection, re-use, and re-formalization of foundational relations have been rendered; and
(3) offering what preceded within a generic context as an entity-type free theory where the
significance of FORT lies. We believe that such an approach is not a repository, but a theory.
While a major limitation of the approach is in its assumption of being atemporal, the forte
contribution points of FORT are twofold. First, the relations being generic and entity-type free
offering modelers wide semantics of primitive relations without obliging primitive concepts.
Second, the selected set of relations being ample for representing the internal structure, spatial
conditions, and interrelations between entities as a minimal, yet inclusive, group of imported
and formulated micro-theories of relations.
3. Arguments for FORT
In this section, we expound on the arguments for FORT that derive from two challenges (issues
introduced in section Section 1) faced by modelers employing FOs for with the aim to use
foundational relations. In particular, we focus on the selected set of relations in which we are
interested. It is important to point out that the two defended arguments promote the need
for FORT, but do not make assumptions of drawbacks or shortcomings on extant FOs, nor do
they argue for eliminating the practice on existing FOs and their corresponding conveniences.
The employment of FORT is an option in the conceptual modeling tasks that do not seek the
adoption of a category hierarchy but only the utilization of foundational relations.
The difficulties upon the adoption and employment of a FO:
The first difficulty is the responsibility that a FO choice incorporates towards understanding
the different ontological and philosophical assumptions made in each FO. With the numerous
FOs available today, the modeler having to choose a FO for practice has to understand several
points; what does each FO offer differently from one another? what are the theoretical modeling
decisions made in each FO, i.e. the ontological commitments that correspond to the world view
it acquires? how are these ontological commitments empirically translated into formalizations?
Performing such a comparison between FOs is a difficult task since most differences occur at a
high meta-physical level which requires deep philosophical understanding. After having this
comparison, the modeler has to elect a FO for practice according to the needs of the application
domain. This involves answering the following; how can the modeling dilemmas present in the
application domain be represented in each FO? how are these representations different, and
what are the conveniences offered by each? Only if the modeler can answer all these questions,
that necessitate massive work and time efforts, then the proper justification of the choice of FO
can be made.
The second difficulty is the entire commitment to the assumptions made in the chosen FO
regarding its world-view. Upon employing a FO, the modeler is committed to its view on the
elements of reality that is wholly interpreted in its formalization. This can be problematic for
the modeler when the modeling dilemma ought to be modeled, cannot be fully represented
by the chosen FO due to the fact that a specific assumption made by it, rejects this view in
the dilemma. In case the assumption in the FO is ignored, the representation will yield in
contradicting semantics. And in case all assumptions are complied to, then the representation
of the dilemma is not fully achieved. Knowing that the list of ontological commitments varies
from one FO to another, one might want to comply with one assumption from one FO e.g.
BFO’s [7] reductionist view (rejects for the co-existence of two entities in the same space-time
location), and another assumption from another FO (that the first, BFO, rejects) e.g. DOLCE’s
[8] parthood theory (general extensional mereology GEM) to solve the modeling dilemma
he has. This representation is not plausible, and the modeler needs thus to presuppose the
requirements of the modeling problem in order to make the best choice of FO with the least
missing representations.
The third difficulty is the obligation to adhere to the categories-hierarchy of the chosen FO. This
does not only oblige modelers to map the domain-specific types (aka kinds or categories) in
their models to the top-level categories in the chosen FO, but also to comply to the constraints
that each type acquires. For example, the category ”Non-Agentive-Physical-Object” in DOLCE
is disjoint from the category ”Amount-of-Matter”, and requires that any instance of the former
be generically constantly constituted by an instance of the latter by the axioms characterizing
both categories. Thus, all categories that are mapped to any of the preceding two, will acquire
additional inherited axioms and semantics that the modeler shall comply with.
Thus, several obstacles arrive with FOs in general, and with the commitment to category
hierarchies in particular. If the aim behind using a FO is foundational relations, then why not
have a relation-centered approach and ignore any taxonomic category axioms?
No FO incorporates inclusively the specified set of foundational relations:
In this argument, we highlight an issue that is not (yet) handled in extant FOs. There is currently
no FO that incorporates the intended foundational relations altogether; parthood, dependence,
constitution, membership, and location. We elaborate on our claim by addressing some FOs.
BFO does not (and cannot) express constitution due to its reductionist view. BFO is a
realist ontology capturing the world as (multiple) particular perspectives of reality i.e. possibly
multiple instantiations of the same particular individual. For constitution, BFO regards the
entities participating in a constitution relation, e.g. the vase and the clay, as the same spatio-
temporal individual that instantiates different universals at the same space-time location i.e. an
identity relation instead. Such an argument is added to BFO’s formalization using an axiom
that prevents two material entities from occupying the same spatial region unless they coincide
i.e. the relations collapse to an identity. Now if constitution is to be represented in BFO, then
it will be a relationship taking place between an individual and itself as an instance of two
different universals i.e. individual ID1 as an instance of a statue and the same ID1 as an instance
of clay. This thus requires the fact that individual ID1 be instantiating two classes at the same
time instance t. Let’s say BFO succeeds in representing such restrictions on a constituted
relation. What about the specificity vs generality of this constitution? In other words, is it a
constitution that is applied specifically to these to individuals? Or is it a constitution that takes
place between any instance of the category of the constituent entity (any instance of clay) and
any of the constituted entity (any instance of statue)? In the latter case, the representation of
constitutional dependence (generic) between the constituent and the constituted entity, which is
an important axiom in the characterization of the constitution relation, will still be unachievable.
This is because constitutional dependence requires the two class types to be disjoint to ensure
that the causal existential connection between instances of the classes comes to an end. Thus,
constitution remains to be problematic for BFO.
DOLCE, on the other hand, does not explicitly define a locative relation nor does it adopt a
specific location theory such as that of Varzi. Instead it offers locative representations via
qualities and quales as will be explained in section 4. In view of such a comprehensive treatment
of relations, membership is not (yet) covered within DOLCE’s specification. Although in the
earlier analysis of building DOLCE, in [9] which presented a preliminary work for DOLCE as
a systematic methodology for selecting and defining some general ontological categories and
relations, the authors have already considered the treatment of the membership relation. The
analysis has been induced in terms of parthood in the spirit of the analysis presented in [10],
with an interpreting a unifying relation that binds all members of a whole (collective/aggregate)
together and a maximality constraint on the members with respect to his relation. However, no
consideration of membership has (yet) been shown in DOLCE.
Similar to DOLCE, with some differences in their treatment of regions, UFO does not integrate a
theory of location relations. Instead it presents an entity-type based approach of attributes and
attribute value spaces following [11]. Such an approach can cover the locative representation
between regions, and between entities (i.e. material ones) and regions. However, what about
representing locative relations between entities that are not spatial regions? For example,
consider two entities that occupy a shared spatial region. On the one side, these entities are
not parts and do not share any parts i.e. mereology is insufficient. On the other side, these
entities are not exactly located in the same spatial region i.e. the ”being exactly located at”
primitive of the Varzi’ location theory is also insufficient. There is a need for a module other
than mereology or basic region locations, such as containment [12] and inclusion theories [13],
for clarifying and determining the spatial information embodied between entities in ontologies
and enhancing their automatic reasoning.
Thus, each of the tackled FOs lacks some relation(s) due to some of its ontological commitments.
If the intended relations are specified, then why not have an inclusive relation theory that
encompasses the desired relations entirely?
4. Aligning FORT to some FOs
In this section, we align and elucidate a relation-based comparison between each micro-theory
in FORT and the corresponding consideration of the relation made in the FOs; BFO, DOLCE, and
UFO, summarized in table 1. The FOs that we inspect are those to which our theory presents
high similarities.
4.1. Ontological dependence
The dependence relation is generally defined in terms of an existence primitive relation, also
referred to as ”being present”. The existence relation is pretty similarly presented in all FOs;
existsAt in BFO, PRE (being present at) in DOLCE as binary predicates between an entity and
an instance of time, and ex in UFO as a unary predicate due to a single time slice formalization.
Table 1
A relation-based comparison between the micro-theories in FORT and the corresponding consideration
of the relations in the FOs; BFO, DOLCE, and UFO.
Foundational Relations FORT BFO DOLCE UFO
existential dependence SED & GED (s-depends-On) YES YES
parthood CEM theory own mereology GEM GEM
parthood & dependence componentOf - (possible) (possible)
& elementOf
parthood & connection MT theory - - -
EntityToRegion Location Location𝑉 𝑎𝑟𝑧𝑖 (occupies-SR) (qualities) (attributes)
EntityToEntity Location EL LocatedIn - -
Membership memberOf (+U) memberOf (-U) - memberOf
Constitution constitutes - YES YES
Constitutional dependence SCD & GCD - YES YES
In BFO; ontological dependence is introduced in the form of entity types that are dependent
on other entity types i.e. 𝑆𝑝𝑒𝑐𝑖𝑓 𝑖𝑐𝑎𝑙𝑙𝑦𝐷𝑒𝑝𝑒𝑛𝑑𝑒𝑛𝑡𝐶𝑜𝑛𝑡𝑖𝑛𝑢𝑎𝑛𝑡𝑠 such as: qualities, functions, roles,
and dispositions, and 𝐺𝑒𝑛𝑒𝑟𝑖𝑐𝑎𝑙𝑙𝑦𝐷𝑒𝑝𝑒𝑛𝑑𝑒𝑛𝑡𝐶𝑜𝑛𝑡𝑖𝑛𝑢𝑎𝑛𝑡𝑠. This dependence is carried out via
relation s-depends_on has as a domain a 𝑆𝑝𝑒𝑐𝑖𝑓 𝑖𝑐𝑎𝑙𝑙𝑦𝐷𝑒𝑝𝑒𝑛𝑑𝑒𝑛𝑡𝐶𝑜𝑛𝑡𝑖𝑛𝑢𝑎𝑛𝑡 and as a range; an
𝐼 𝑛𝑒𝑝𝑒𝑛𝑑𝑒𝑛𝑡𝐶𝑜𝑛𝑡𝑖𝑛𝑢𝑎𝑛𝑡 or 𝑃𝑟𝑜𝑐𝑒𝑠𝑠 in case of a one-sided s-dependence, or a 𝐷𝑒𝑝𝑒𝑛𝑑𝑒𝑛𝑡𝐶𝑜𝑛𝑡𝑖𝑛𝑢𝑎𝑛𝑡 in
case of a reciprocal s-dependence.
In UFO, in addition to existential dependence 𝑒𝑑(𝑥, 𝑦) and independence 𝑖𝑛𝑑(𝑥, 𝑦), functional
dependence is also studied in its generic 𝑔𝑓 𝑑(Φ, Ψ) and individual 𝑖𝑓 𝑑(𝑥, Φ, 𝑦, Ψ) -defined in
terms of 𝑔𝑓 𝑑- forms according to the treatment of functional parts by Guizzardi in [4].
DOLCE introduces two types of dependence relations; specific between particulars 𝑆𝐷(𝑥, 𝑦)
or universals/properties 𝑆𝐷(Φ, Ψ), and generic between universals/properties 𝐺𝐷(Φ, Ψ). Using
these two types, other forms are also defined e.g. one-sided and mutual dependencies.
Similar to DOLCE’s account for dependence, FORT analysis two types of the relation, namely
existential dependence in two forms, specific 𝑆𝐸𝐷(𝑥, 𝑦) and generic 𝐺𝐸𝐷(𝑥, 𝑦) within a non-
modal approach. This is less similar to UFO’s approach, and completely dissimilar from that of
BFO which does not meet our interpretation as explained in section 3.
4.2. Parthood
FORT adopts CEM, while DOLCE and UFO both adopt GEM, and BFO constructs its own
mereology within its continuant part of relation.
FORT further accounts the combination of parthood with dependence to introduce the notion
of inseparable parts (essential and mandatory); elements and components. This is plausible in
DOLCE since the primitive relations (parthood and specific/generic existential dependence)
exist. In UFO, it is feasible using the existential dependence relation to introduce essential parts
(aka elements in FORT) but not mandatory parts (aka components in FORT). However, UFO
does define dependent parts as components using the 𝑐𝑜𝑚𝑝𝑜𝑛𝑒𝑛𝑡𝑂𝑓 (𝑥, 𝑦) relation that is proper
parthood 𝑃𝑃(𝑥, 𝑦) accompanied with a restriction on the individual functional dependence of
the whole on the part 𝑖𝑓 𝑑(𝑥, 𝑥 ′ , 𝑦, 𝑦 ′ ).
For the mereotopological theoretical aspect, none of the considered FOs imports the connection
topological theory, whereas FORT imports minimal mereotopology i.e. the primitive connection
relation with its corresponding topological predicates.
4.3. Location
Since locative relations in FORT are divided into three types, we investigate according to each
type, the similar relations in each of the studied FOs.
• region-to-region locative relations: Without committing to a region entity type, FORT
suggests the use of the primitive parthood relation 𝑝𝑎𝑟𝑡 − 𝑜𝑓 to express mereotopological
representations between entity types that can be regions. This is similar to BFO’s uti-
lization of its own mereological relation 𝑐𝑜𝑛𝑡𝑖𝑛𝑢𝑎𝑛𝑡𝑃𝑎𝑟𝑡𝑂𝑓 between spatial regions, and
DOLCE’s and UFO’s use of the primitive mereological relation 𝑃𝑎𝑟𝑡𝑂𝑓.
• entity-to-region locative relations: In FORT, we import Varzi’s location theory [14],
which in turn links to the imported mereotopological theory. While BFO uses the
𝑜𝑐𝑐𝑢𝑝𝑖𝑒𝑠𝑆𝑝𝑎𝑡𝑖𝑎𝑙𝑅𝑒𝑔𝑖𝑜𝑛 relation to express the spatial region that an independent con-
tinuant entity is acquiring, both DOLCE and UFO adopt different views for location
representations via qualities (in DOLCE) and attributes (in UFO). In DOLCE, in terms
of quality types and quales, location can be described as a scenario encompassing; (a) a
quality type, which in the case of expressing a location, is the spatial location of an entity
e.g. 𝑆𝐿1 as a instance of the class 𝑆𝑝𝑎𝑡𝑖𝑎𝑙𝐿𝑜𝑐𝑎𝑡𝑖𝑜𝑛 which is a subclass of 𝑃ℎ𝑦𝑠𝑖𝑐𝑎𝑙𝑄𝑢𝑎𝑙𝑖𝑡𝑦,
which is a subclass of 𝑄𝑢𝑎𝑙𝑖𝑡𝑦, (b) a quale i.e. the spatial region which the entity is covering
e.g. 𝑆𝑅1 which is an instance of the 𝑆𝑝𝑎𝑡𝑖𝑎𝑙𝑅𝑒𝑔𝑖𝑜𝑛 which is a subclass of 𝑃ℎ𝑦𝑠𝑖𝑐𝑎𝑙𝑅𝑒𝑔𝑖𝑜𝑛,
which is a subclass of 𝑅𝑒𝑔𝑖𝑜𝑛, and (c) a relation 𝑄𝑙𝑡 that links both the quality type and it
corresponding quale i.e. links 𝑆𝑅1 to 𝑆𝐿1, at a specific time. Whereas in UFO, a similar
representation is done using attributes and attribute value spaces.
• entity-to-entity locative relations: these are expressed in FORT using the entity location
𝐸𝐿 primitive relation indicating ”located at/on/in”. BFO in turn uses a simple primitive
relation 𝑙𝑜𝑐𝑎𝑡𝑒𝑑 − 𝐼 𝑛 between two independent continuants that are not spatial regions,
while both DOLCE and UFO do not account for such a representation.
4.4. Membership
FORT examines membership 𝑚𝑒𝑚𝑏𝑒𝑟𝑂𝑓 (𝑥, 𝑦) as a primitive relation that is defined in terms of
ground axioms with the characterization of its whole entity. Although FORT does not account
for entity types, it requires restriction on the range of the membership relation to be unified
𝑈𝑅𝑖 (𝑦) , through its members, by a unification relation 𝑅𝑖 (𝑥, 𝑥) . The axiomatization provided in
FORT is similar to that in BFO except that BFO uses a class type 𝐴𝑔𝑔𝑟𝑒𝑔𝑎𝑡𝑒𝐸𝑛𝑡𝑖𝑡𝑦 to characterize
the whole while FORT does not, and BFO does not oblige the binding of all members according
to a similarity constraint i.e. unifying relation. UFO also provides a membership primitive
𝑚𝑒𝑚𝑏𝑒𝑟𝑂𝑓 (𝑥, 𝑦) that holds between an object and a collection following the preliminary analysis
in [15] and [16]. However, for DOLCE, membership is not (yet) considered although the notion
has been addressed in the preliminary studies for ontological distinctions as mentioned in
section 3.
4.5. Constitution
FORT treats constitution in a very similar manner to that in DOLCE and UFO. Using a con-
stitution primitive 𝑐𝑜𝑛𝑠𝑡𝑖𝑡𝑢𝑡𝑒𝑠(𝑥, 𝑦) ( 𝐾 (𝑥, 𝑦) in DOLCE, and 𝑐𝑜𝑛𝑠𝑡𝑖𝑡𝑢𝑡𝑒𝑑𝐵𝑦(𝑦, 𝑥) in UFO) along
with defining specific and generic constitutional dependencies 𝑆𝐶𝐷(𝑥, 𝑦)/𝐺𝐶𝐷(Ψ, Φ). However,
in contrary to DOLCE’s concept 𝐴𝑚𝑜𝑢𝑛𝑡𝑂𝑓 𝑀𝑎𝑡𝑡𝑒𝑟, FORT does not restrict types but applies
additional axiomatization on the relata of the relation. For BFO, as discussed in section 3,
constitution is not regarded.
5. FORT as a CL-ontology
In this section, we associate the theory with another logical language; a CLIF-serialization
as a Common Logic (CL) [6] ontology that validates the existence of models for FORT using
consistency checks.
CL, which is an extension of KIF (Knowledge Interchange Format), is a logical language based
on FOL, with the purpose of standardizing syntax (e.g. “CLIF ”; the Common Logic Interchange
Format) and semantics for information interchange and transmission. CL is used in ontological
theories as a formal language tool to prove the consistency of a theory by validating the
existence of model(s) M for a theory T . For example, BFO 1 and some of DOLCE’s modules 2 are
encoded in CLIF. In addition to FOs, an open-access repository of first-order theories “Colore ”
is implemented as CL-ontology modules 3 such as mereology.
5.1. A CLIF-serialization of FORT
Considering that FORT is a group of interlinked ontology modules that imports and reuses
some extant theories from the literature, firstly we import those that are already encoded and
available online at the “Colore ” repository. These are; the CEM mereological theory4 , the MT
mereotopological theory along with the basic connection topological theory5 , Varzi’s Location
theory6 , and their corresponding definitions. We modified some files e.g. the mereological
definitions file to account for additional definitions e.g. overcross, undecross, etc, the location
root file to remove region axioms, etc.
Secondly, we initiate the serialization of FORT’s micro-theories in the sense of ”what-comes-
fir st?” i.e. starting by the basic primitive relations that do not necessitate the use of other
primitives, and passing to relations that import other relations in their modules. The full CL
formalization of the theory is available online on GitHub repository; FORT.
In the process of encoding the CL ontology of FORT, we face some limitations in the language’s
syntax. In the following, we identify the issue, locate it in the theory, and propose a solution to
dealing with it.
What is the issue? Since FORT is an entity-type free theory, then it’s FOL formalization
1
https://github.com/BFO-ontology/BFO-2020/tree/master/21838-2/common-logic
2
https://github.com/gruninger/colore/tree/master/ontologies
3
https://github.com/gruninger/colore/tree/master/ontologies
4
https://raw.githubusercontent.com/gruninger/colore/master/ontologies/mereology/cem_mereology.clif
5
https://raw.githubusercontent.com/gruninger/colore/master/ontologies/combined_mereotopology/mt.clif
6
https://raw.githubusercontent.com/gruninger/colore/master/ontologies/location_varzi/L_location.clif
comprises mostly variables quantifying over binary predicates (aka relations) without defining
unary ones that represent entity types. However, in cases where restrictions on relata types
are crucial for the characterization of a relation, we have used unary predicates (e.g. Ψ, Φ, 𝜑)
that resemble entity types. More precisely, these are functions that quantify over a list of entity
types that the modeler or the user in application would have. As expressed earlier, the practice
of FORT is intended as a relation theory to be imported within the user’s application (which is a
complete model of concepts and relations) to add semantics and rule constraints. This strategy
of dealing with unary predicates that range over a finite set of universals is inline with that
proposed by the Common Logic working group 7 , and followed by DOLCE, as follows: ∃𝜑(𝜑(𝑥))
corresponds to ⋁Φ∈Π (Φ(𝑥)) and ∀𝜑(𝜑(𝑥)) corresponds to ⋀Φ∈Π (Φ(𝑥)) where Π refers to the
finite list of concept names in the ontology. According to such a treatment, it is possible to
express existential and universal quantification on universals in DOLCE. However, FORT does
not provide a hierarchy of concepts, thus asserting ranging predicates on a set of universals Π
is not possible. The same issue also applies on quantifying over binary predicates that resemble
relations.
Where is the issue located in FORT? We track this issue by identifying the definitions and
axioms in FORT that use such a quantification over unary/binary predicate names. These are:
(a) the use of a universal quantifier on concepts in the generic existential dependence relation,
and (b) the use of existential quantifiers on the unifying relations in the definition of a unified
entity.
How can the issue be resolved? We elucidate a possible strategy to resolve this issue. If we
quantify over unary/binary predicate names in CLIF serializations, the syntax will be violated.
If we withdraw the usage of these predicates as ranging over finite sets, the expressive power
of some relations in FORT drops. The most suitable strategy is to consider these predicates
(Ψ, Φ, 𝜑, 𝑅𝑖 ) as functions that themselves range over unary and binary predicates and do not
need quantification. In other words; the usage of 𝜑(𝑥) shall correspond to a definition of 𝜑 as
𝜑(𝑥) = ∃Φ(Φ ∈ Π∧(Φ(𝑥))) in which in practice will be encoded as 𝜑(𝑥) = 𝐶1 (𝑥)∨𝐶2 (𝑥)∨...∨𝐶𝑛 (𝑥)
where each of 𝐶𝑖 (𝑥) will correspond to a category in the user’s model. Similarly for role names,
the usage of 𝑅𝑖 (𝑥) shall correspond to the union of all unifying relations, thus can be considered
as the parent of all unification relations. The sole drawback of this solution is that it adds to
modelers the effort of adding some definitions to their models to maintain the validity and
consistency of the theory, while achieving the intended expressive power. The sole difference
in comparison to DOLCE’s strategy lies in the finite set Π where DOLCE restricts the elements
of its set to its defined category types, while FORT offers the possibility for the user to specify
the user-categories that the predicates will range over.
5.2. Automatic translations and consistency checks
Besides a CLIF serialization, we performed an automatic translation of FORT into the LADR
syntax of Prover9 which is the format required by Prover9 and Mace4, and to the TPTP format,
to offer multiple serializations of CL.
7
cl.tamu.edu
For this translation, several tools exist such as the CLtools repository 8 , which has been pre-
viously adopted by 9 for a theory’s translation to Ladr syntax. However, no maintenance of
the tool or resolving of its issues has been carried out in the last decade. Another tool is the
macleod program 10 which consists of python scripts that can; translate a CLIF file to tptp
and ladr formats; extract an OWL approximation of a clif ontology/module; verify the logical
consistency of a clif ontology; verify the non-trivial logical consistency of a CLIF ontology; and
prove theorems/lemmas that encode intended consequences of an ontology or module.
So, we adopted the macleod program, in which we had to modify some configuration files and
adapt some scripts, to build TPTP and Prover9 translations for each ontology module.
As for running consistency checks, we used the ”darwin11 ” consistency checker in “The
Heterogeneous tools set” [17] (Hets) 12 to check the consistency of each ontology module,
followed by the full FORT theory, yielding in consistent results.
6. Conclusion
In this paper, we have illustrated our previous work on FORT [5] that corresponds to the first
step of FORT’s methodology, as a preliminary for this paper’s presentation. Then we proceeded
forward to accomplish the second step of the methodology where the contributions twofold.
The first contribution is the positioning and alignment of FORT concerning some selected FOs.
To do so, we defended and expounded two arguments for FORT (Section 3); (a) the difficulties
that modelers encounter upon adopting and employing a FO; and (b) the fact that no FO (yet)
incorporates inclusively the specified set of foundational relations (parthood, dependence, con-
stitution, membership, and location with the formal properties and relations that are required to
characterize them) with elaborating on those relations that are not handled each FO. In addition,
we elucidated a relation-based comparison between each module in FORT and its corresponding
aligned relation in each of the selected FOs, to which FORT presents high similarities (Section 4).
The second contribution is the validation of FORT’s consistency while providing a CLIF-
serialization, translating into TPTP and Prover9 formats, and performing consistency checks to
each module and to the full theory (Section 5).
For our future work, we plan to the next steps of the methodology; a decidable knowledge
representation language formalization that supports reasoning services i.e a DL-SROIQ formal-
ization; and an OWL2-DL lite implementation of FORT. Such an approach is in line with some
approaches in the Semantic Web community which advocate that re-usability is enhanced by
eliminating domain/range constraints. Providing such an OWL ontology of relations (FORT-
ontology) serves as an ontological tool offering a language of primitive relations and rules, and
enhances and facilitates ontology-driven conceptual modeling tasks.
8
https://github.com/cmungall/cltools
9
http://www.cs.toronto.edu/ torsten/DCT-BCont/
10
https://github.com/thahmann/macleod
11
http://combination.cs.uiowa.edu/Darwin/
12
Hets is a parsing, static analysis and proof management tool incorporating various provers and different
specification languages. It can be used either in its web-based interface http://rest.hets.eu/or installed it in a Docker
container following the instructions http://hets.eu/
References
[1] S. Pribbenow, Meronymic Relationships: From Classical Mereology to Complex Part-Whole
Relations, 2002, pp. 35–50. doi:10.1007/978- 94- 017- 0073- 3_3 .
[2] M. Winston, R. Chaffin, D. Herrmann, A taxonomy of part-whole relationships, Cognitive
Science - COGSCI 3 (1987).
[3] T. Bittner, M. DONNELLY, B. Smith, Individuals, universals, collections: On the founda-
tional relations of ontology (2004).
[4] G. Guizzardi, The problem of transitivity of part-whole relations in conceptual modeling
revisited, 2009, pp. 94–109. doi:10.1007/978- 3- 642- 02144- 2_12 .
[5] F. Danash, D. Ziebelin, FORT: a minimal Foundational Ontological Relations Theory
for Conceptual Modeling Tasks, in: The 41st International Conference on Conceptual
Modeling (ER2022), Forum track, 2022.
[6] Common Logic (CL): A framework for a family of logic-based languages., Standard ISO/IEC
24707:2018, International Organization for Standardization, Geneva, CH, 2018.
[7] B. Smith, P. Grenon, H. Stenzhorn, A. Spear, BFO basic formal ontology, http://
basic-formal-ontology.org/, 2002.
[8] C. Masolo, S. Borgo, A. G. N. Guarino, A. Oltramari, WonderWeb Deliverable D18 Ontology
Library (final), Technical Report, IST Project 2001-33052 WonderWeb: Ontology Infras-
tructure for the Semantic Web, 2003. URL: http://www.loa.istc.cnr.it/old/DOLCE.html.
[9] A. Gangemi, N. Guarino, C. Masolo, A. Oltramari, Understanding top-level ontological
distinctions, in: OIS@IJCAI, 2001. URL: http://ceur-ws.org/Vol-47/gangemi.pdf.
[10] N. Guarino, C. Welty, Identity, unity, and individuality: Towards a formal toolkit for
ontological analysis, Proceedings of ECAI-2000: The European Conference on Artificial
Intelligence (2000).
[11] G. Guizzardi, C. Masolo, S. Borgo, In defense of a trope-based ontology for conceptual
modeling: An example with the foundations of attributes, weak entities and datatypes,
volume 4215, 2006, pp. 112–125. doi:10.1007/11901181_10 .
[12] T. Bittner, Axioms for parthood and containment relations in bio-ontologies, in: KR-MED,
2004.
[13] M. Donnelly, T. Bittner, C. Rosse, A formal theory for spatial representation and reasoning
in biomedical ontologies, Artificial intelligence in medicine 36 (2006) 1–27. doi:10.1016/
j.artmed.2005.07.004 .
[14] R. Casati, A. C. Varzi, Parts and Places: The Structures of Spatial Representation, MIT
Press, 1999.
[15] G. Guizzardi, Ontological Foundations for Structural Conceptual Models, Ph.D. thesis,
2005.
[16] G. Guizzardi, G. Wagner, J. Almeida, R. Guizzardi, Towards ontological foundations for
conceptual modeling: The unified foundational ontology (ufo) story, Applied ontology 10
(2015). doi:10.3233/AO- 150157 .
[17] T. Mossakowski, C. Maeder, M. Codescu, E. Kuksa, C. Lange, Hets for common logic users
- version 0.99 -, 2013.
A. FORT’s micro-theories
A.1. Ontological dependence
∀(𝑥, 𝑦)𝑆𝐸𝐷(𝑥, 𝑦) =𝑑𝑓 ∀𝑡(𝐸(𝑥, 𝑡) → 𝐸(𝑦, 𝑡)) ∧ ¬(𝑥 = 𝑦) ∧ ∃𝑡𝐸(𝑥, 𝑡) (Dd1)
(∀𝑥, 𝑦, 𝑧)𝑆𝐸𝐷(𝑥, 𝑦) ∧ 𝑆𝐸𝐷(𝑦, 𝑧) → 𝑆𝐸𝐷(𝑥, 𝑧) (Dt1)
∀(Φ, 𝜑)𝐺𝐸𝐷(Φ, 𝜑) =𝑑𝑓 ∀𝑥, 𝑡((Φ(𝑥) ∧ 𝐸(𝑥, 𝑡)) → ∃𝑦(𝜑(𝑦) ∧ 𝐸(𝑦, 𝑡))) ∧ ∃𝑥, 𝑡(Φ(𝑥) ∧ 𝐸(𝑥, 𝑡))∧
¬∃𝑧(Φ(𝑧) ∧ 𝜑(𝑧)) (Dd2)
∀(Φ, 𝜑, 𝛼)𝐺𝐸𝐷(Φ, 𝜑) ∧ 𝐺𝐸𝐷(𝜑, 𝛼) ∧ ¬∃𝑥(Φ(𝑥) ∧ 𝛼(𝑥)) → 𝐺𝐸𝐷(Φ, 𝛼) (Dt2)
Where Φ and 𝜑 are variables that range over universal concepts i.e. correspond to Φ =
⋁Ψ∈Π (Ψ(𝑥)) where Π refers to the finite list of concept names in the ontology.
A.2. Parthood
(∀𝑥, 𝑦)𝐶𝑜𝑚𝑝𝑜𝑛𝑒𝑛𝑡𝑂𝑓 (𝑥, 𝑦) =𝑑𝑓 𝑃(𝑥, 𝑦) ∧ 𝐺𝐸𝐷(Φ(𝑦), Ψ(𝑥)) (Pd1)
(∀𝑥, 𝑦, 𝑧)𝐶𝑜𝑚𝑝𝑜𝑛𝑒𝑛𝑡𝑂𝑓 (𝑥, 𝑦) ∧ 𝐶𝑜𝑚𝑝𝑜𝑛𝑒𝑛𝑡𝑂𝑓 (𝑦, 𝑧) → 𝐶𝑜𝑚𝑝𝑜𝑛𝑒𝑛𝑡𝑂𝑓 (𝑥, 𝑧) (Pt1)
(∀𝑥)¬𝐶𝑜𝑚𝑝𝑜𝑛𝑒𝑛𝑡𝑂𝑓 (𝑥, 𝑥) (Pt2)
(∀𝑥, 𝑦)𝐶𝑜𝑚𝑝𝑜𝑛𝑒𝑛𝑡𝑂𝑓 (𝑥, 𝑦) → ¬𝐶𝑜𝑚𝑝𝑜𝑛𝑒𝑛𝑡𝑂𝑓 (𝑦, 𝑥) (Pt3)
(∀𝑥, 𝑦)𝐶𝑜𝑚𝑝𝑜𝑛𝑒𝑛𝑡𝑂𝑓 (𝑥, 𝑦) → 𝑃𝑃(𝑥, 𝑦) (Pa1)
(∀𝑥, 𝑦)𝐶𝑜𝑚𝑝𝑜𝑛𝑒𝑛𝑡𝑂𝑓 (𝑥, 𝑦) → ∃𝑧(𝑃(𝑧, 𝑦) ∧ ¬𝑂(𝑧, 𝑥)) (Pt4)
(∀𝑥, 𝑦)𝐸𝑙𝑒𝑚𝑒𝑛𝑡𝑂𝑓 (𝑥, 𝑦) =𝑑𝑓 𝑃(𝑥, 𝑦) ∧ 𝑆𝐸𝐷(𝑦, 𝑥) (Pd2)
(∀𝑥, 𝑦, 𝑧)𝐸𝑙𝑒𝑚𝑒𝑛𝑡𝑂𝑓 (𝑥, 𝑦) ∧ 𝐸𝑙𝑒𝑚𝑒𝑛𝑡𝑂𝑓 (𝑦, 𝑧) → 𝐸𝑙𝑒𝑚𝑒𝑛𝑡𝑂𝑓 (𝑥, 𝑧) (Pt5)
(∀𝑥)¬𝐸𝑙𝑒𝑚𝑒𝑛𝑡𝑂𝑓 (𝑥, 𝑥) (Pt6)
(∀𝑥, 𝑦)𝐸𝑙𝑒𝑚𝑒𝑛𝑡𝑂𝑓 (𝑥, 𝑦) → ¬𝐸𝑙𝑒𝑚𝑒𝑛𝑡𝑂𝑓 (𝑦, 𝑥) (Pt7)
(∀𝑥, 𝑦)𝐸𝑙𝑒𝑚𝑒𝑛𝑡𝑂𝑓 (𝑥, 𝑦) → 𝑃𝑃(𝑥, 𝑦) (Pa2)
(∀𝑥, 𝑦)𝐸𝑙𝑒𝑚𝑒𝑛𝑡𝑂𝑓 (𝑥, 𝑦) → ∃𝑧(𝑃(𝑧, 𝑦) ∧ ¬𝑂(𝑧, 𝑥)) (Pt8)
A.3. Entity-to-entity location:
(∀𝑥)𝐸𝐿(𝑥, 𝑥) (ELa1)
(∀𝑥, 𝑦, 𝑧)(𝐸𝐿(𝑥, 𝑦) ∧ 𝐸𝐿(𝑥, 𝑧) → 𝐸𝐿(𝑥, 𝑧)) (ELa2)
(∀𝑥, 𝑦)(𝑃(𝑥, 𝑦) → 𝐸𝐿(𝑥, 𝑦)) (ELa3)
(∀𝑥, 𝑦, 𝑧)(𝑃(𝑥, 𝑦) ∧ 𝐸𝐿(𝑦, 𝑧) → 𝐸𝐿(𝑥, 𝑦)) (ELt1)
(∀𝑥, 𝑦, 𝑧)(𝐸𝐿(𝑥, 𝑦) ∧ 𝑃(𝑦, 𝑧) → 𝐸𝐿(𝑥, 𝑦)) (ELt2)
(∀𝑥, 𝑦, 𝑧)(𝐸𝐿(𝑥, 𝑦) ∧ 𝐿(𝑦, 𝑧) → 𝑊 𝐿(𝑥, 𝑧)) (ELt3)
(∀𝑥, 𝑦, 𝑧, 𝑤)(𝐸𝐿(𝑥, 𝑦) ∧ 𝐿(𝑥, 𝑧) ∧ 𝐿(𝑦, 𝑤) → 𝑃(𝑧, 𝑤)) (ELt4)
A.4. Membership
(∀𝑥)¬𝑚𝑒𝑚𝑏𝑒𝑟𝑂𝑓 (𝑥, 𝑥) (Ma1)
(∀𝑥, 𝑦)𝑚𝑒𝑚𝑏𝑒𝑟𝑂𝑓 (𝑥, 𝑦) → ¬𝑚𝑒𝑚𝑏𝑒𝑟𝑂𝑓 (𝑦, 𝑥) (Ma2)
(∀𝑥, 𝑦)𝑚𝑒𝑚𝑏𝑒𝑟𝑂𝑓 (𝑦, 𝑥) → ∃𝑡, 𝑚1 , 𝑚2 (𝑚1 ≠ 𝑚2 ∧ 𝐸(𝑥, 𝑡) ∧ 𝑚𝑒𝑚𝑏𝑒𝑟𝑂𝑓 (𝑚1 , 𝑥) ∧ 𝑚𝑒𝑚𝑏𝑒𝑟𝑂𝑓 (𝑚2 , 𝑥))
(Ma3)
(∀𝑥, 𝑝, 𝑦)𝑚𝑒𝑚𝑏𝑒𝑟𝑂𝑓 (𝑦, 𝑥) ∧ 𝑃𝑃(𝑝, 𝑥) → ∃𝑜(𝑚𝑒𝑚𝑏𝑒𝑟𝑂𝑓 (𝑜, 𝑥) ∧ 𝑂(𝑜, 𝑝)) (Ma4)
(∀𝑥, 𝑦)𝑚𝑒𝑚𝑏𝑒𝑟𝑂𝑓 (𝑥, 𝑦) → (𝑃𝑃(𝑥, 𝑦) ∧ ∀𝑚(𝑚𝑒𝑚𝑏𝑒𝑟𝑂𝑓 (𝑚, 𝑦) → 𝑥 = 𝑑 ∨ ¬𝑂(𝑚, 𝑥))) (Ma5)
(∀𝑥, 𝑦)𝑚𝑒𝑚𝑏𝑒𝑟𝑂𝑓 (𝑦, 𝑥) → (∀𝑤(𝑂(𝑤, 𝑥) ↔ ∃𝑚(𝑚𝑒𝑚𝑏𝑒𝑟𝑂𝑓 (𝑚, 𝑥) ∧ 𝑂(𝑤, 𝑚)))) (Ma6)
(∀𝑥, 𝑦)𝑅𝑖 (𝑥, 𝑦) → 𝑅𝑖 (𝑥, 𝑥) ∧ 𝑅𝑖 (𝑦, 𝑦) (Ra1)
(∀𝑥, 𝑦)𝑅𝑖 (𝑥, 𝑦) → 𝑅𝑖 (𝑦, 𝑥) (Ra2)
(∀𝑧)𝒰𝑅𝑖 (𝑧) =𝑑𝑓 ∀𝑟(𝑅𝑖 (𝑟, 𝑟) → 𝑃(𝑟, 𝑧)) ∧ ∀𝑚(𝑂(𝑚, 𝑧) ↔ ∃𝑟(𝑅𝑖 (𝑟, 𝑟) ∧ 𝑂(𝑚, 𝑟))) ∧ ∀𝑎, 𝑏(𝑅𝑖 (𝑎, 𝑎)∧
𝑅𝑖 (𝑏, 𝑏) ∧ 𝑃(𝑎, 𝑧) ∧ 𝑃(𝑏, 𝑧) → 𝑅𝑖 (𝑎, 𝑏)) (Rd1)
(∀𝑥, 𝑦)𝑚𝑒𝑚𝑏𝑒𝑟𝑂𝑓 (𝑦, 𝑥) → ∃𝑖(𝒰𝑅𝑖 (𝑥) ∧ (∀𝑡(𝑒𝑥𝑖𝑠𝑡𝑠(𝑥, 𝑡) → 𝒰𝑅𝑖 (𝑥))) (Ma7)
(∀𝑥, 𝑦, 𝑤, 𝑧)𝑚𝑒𝑚𝑏𝑒𝑟𝑂𝑓 (𝑥, 𝑦) ∧ 𝑚𝑒𝑚𝑏𝑒𝑟𝑂𝑓 (𝑤, 𝑧) ∧ ∃𝑖(𝒰𝑅𝑖 (𝑦) ∧ 𝒰𝑅𝑖 (𝑧)) → 𝑦 = 𝑧 (Mt1)
A.5. Constitution
(∀𝑥)¬𝑐𝑜𝑛𝑠𝑡𝑖𝑡𝑢𝑡𝑒𝑠(𝑥, 𝑥) (Ca1)
(∀𝑥, 𝑦)𝑐𝑜𝑛𝑠𝑡𝑖𝑡𝑢𝑡𝑒𝑠(𝑥, 𝑦) → ¬𝑐𝑜𝑛𝑠𝑡𝑖𝑡𝑢𝑡𝑒𝑠(𝑦, 𝑥) (Ca2)
(∀𝑥, 𝑦, 𝑧)𝑐𝑜𝑛𝑠𝑡𝑖𝑡𝑢𝑡𝑒𝑠(𝑥, 𝑦) ∧ 𝑐𝑜𝑛𝑠𝑡𝑖𝑡𝑢𝑡𝑒𝑠(𝑦, 𝑧) → 𝑐𝑜𝑛𝑠𝑡𝑖𝑡𝑢𝑡𝑒𝑠(𝑥, 𝑧) (Ca3)
(∀𝑥, 𝑦)𝑐𝑜𝑛𝑠𝑡𝑖𝑡𝑢𝑡𝑒𝑠(𝑥, 𝑦) → ∃𝑡(𝐸(𝑥, 𝑡) ∧ 𝐸(𝑦, 𝑡)) (Ca4)
(∀𝑥, 𝑦, 𝑧)𝑐𝑜𝑛𝑠𝑡𝑖𝑡𝑢𝑡𝑒𝑠(𝑥, 𝑦) ∧ 𝑃(𝑧, 𝑦) → ∃𝑥 ′ (𝑃(𝑥 ′ , 𝑥) ∧ 𝑐𝑜𝑛𝑠𝑡𝑖𝑡𝑢𝑡𝑒𝑠(𝑥 ′ , 𝑧)) (Ca5)
(∀𝑥, 𝑦)𝑆𝐶𝐷(𝑥, 𝑦) =𝑑𝑓 ∃𝑡𝐸(𝑥, 𝑡) ∧ ∀𝑡(𝐸(𝑥, 𝑡) → 𝑐𝑜𝑛𝑠𝑡𝑖𝑡𝑢𝑡𝑒𝑠(𝑦, 𝑥)) (Cd1)
(∀Φ, Ψ)𝐺𝐶𝐷(Φ, Ψ) =𝑑𝑓 ¬∃𝑧(Φ(𝑥) ∧ Ψ(𝑧)) ∧ ∀𝑥(Φ(𝑥) → ∃𝑡𝐸(𝑥, 𝑡)) ∧ ∀𝑥, 𝑡(Φ(𝑥)∧
𝐸(𝑥, 𝑡) → ∃𝑦(Ψ(𝑦) ∧ 𝑐𝑜𝑛𝑠𝑡𝑖𝑡𝑢𝑡𝑒𝑠(𝑦, 𝑥)) (Cd2)
(∀𝑥, 𝑦)𝑆𝐶𝐷(𝑥, 𝑦) → 𝑆𝐸𝐷(𝑥, 𝑦) (Ct1)
(∀Φ, Ψ)𝐺𝐶𝐷(Φ, Ψ) → 𝐺𝐸𝐷(Φ, Ψ) (Ct2)
(∀𝑥, 𝑦, 𝑧)𝑆𝐶𝐷(𝑥, 𝑦) ∧ 𝑆𝐶𝐷(𝑦, 𝑧) → 𝑆𝐶𝐷(𝑥, 𝑧) (Ct3)
(∀Φ, Ψ, 𝜑)𝐺𝐶𝐷(Φ, Ψ) ∧ 𝐺𝐶𝐷(Ψ, 𝜑) ∧ ¬∃𝑧(Φ(𝑧) ∧ 𝜑(𝑧)) → 𝐺𝐶𝐷(Φ, 𝜑) (Ct4)
(∀𝑥, 𝑦, Φ, Ψ)𝑐𝑜𝑛𝑠𝑡𝑖𝑡𝑢𝑡𝑒𝑠(𝑥, 𝑦) ∧ Φ(𝑥) ∧ Ψ(𝑦) → 𝐺𝐶𝐷(Ψ, Φ) (Ca7)
(∀𝑥, 𝑦)𝑐𝑜𝑛𝑠𝑡𝑖𝑡𝑢𝑡𝑒𝑠(𝑥, 𝑦) → ∀𝑧(𝑃(𝑧, 𝑥) → 𝐸𝑙𝑒𝑚𝑒𝑛𝑡𝑂𝑓 (𝑧, 𝑥)) (Ca8)