In this paper, we present a succinct formalisation of the main categories of the Unified Foundational Ontology (UFO) by summarising and simplifying a fragment of the version of [Gui05]. In this version, we show that the use first-order modal logic with no higher-order constructs suffices for many modelling tasks. We focus here on the case of universals. We slightly modify the original version of UFO by presenting new definitions of the intension and of the extension of universals and by approaching a taxonomy of universals.
The Unified Foundational Ontology (UFO) was proposed in [Gui05] as an ontology for general conceptual modelling languages. Two crucial aspects of the UFO program is that it aims to be cognitively grounded, e.g. by means of the use of Ga¨rdenfors’s conceptual spaces [Ga¨r00] and by the careful confrontation with the relevant literature in Linguistics and Cognitive psychology, and philosophically aware, by means of a close comparison with the essential literature in philosophy of language, ontology, and analytical metaphysics.
The aim of this brief paper is to present the main categories of UFO by proposing an axiomatisation restricted to first-order modal logic. One of the crucial feature of UFO is that it includes universals in its domain of quantification. In the original presentation of [Gui05], sets were used to define the extension of a universal and a number of other categories, e.g. quality spaces, which led in a number of places to higher-order constructions. The motivation of this first-order rephrasing is, on the one hand, to show that firstorder logic appears sufficient at least for a significant number of the modelling tasks of UFO and, on the other hand, to prepare the ground for discussing suitable reasoners for UFO. UFO uses modal reasoning in particular for dealing with the concept of existential dependence and for classifying types of universals, e.g. to define properties of universals such as rigidity and anti-rigidity. For this reason, modalities are included in our proposed formalisation. However, a first-order modal version of UFO can in principle be translated into a first-order version UFO, along the lines of the translation discussed in [BG07]. By means of that, we can start approaching the goal of developing fragments of UFO in tractable languages (e.g. description logics). Moreover, a first-order formulation of UFO in principle allows us to adapt the methodology of [KM11] for proposing a (modular) consistency proof for UFO, which is still missing. Finally, by rephrasing UFO in a first-order language, we enhance the possibility of developing a precise comparison with other foundational first-order ontologies (e.g. with DOLCE [BM09]).
As we shall see, first-order modal formulas are sufficient to present the treatment of universals in UFO. To do that, we shall replace sets with mereological fusions of individuals of the selected types and we shall relate the extensions of universals, which provide the classes of entities to which the universals apply, to the mereological aggregate of individuals that instantiate the universal. This approach is not going to be equivalent to the set-theoretic formulation, since by means of a first-order definition of mereological sums we cannot define all the sets, however, in practice this suffices to include all the sets that we actually intend to specify in many modelling tasks. Similar reasons are discussed to motivate the use of a first-order version of fusion in mereology, cf. [Var16].
The main differences of this formalisation of UFO with respect to [Gui05] are the following: 1. We define the extension of universal as the mereological fusion of its instances. 2. We propose a novel treatment of the definition of intension of a universal and of the relationship between the intension and the extension of universals. 3. We approach a taxonomy of types of universals.
In what follows, for reasons of space, we omit the treatment of quality and quality structures, which is an important aspect of UFO [Gui05], and we leave if for future work. The remainder of this paper is organised as follows. In Section 2, we present the main taxonomy of UFO. Section 3 presents the treatment of universals, which contains the main departure from the formalisation in [Gui05]. Section 4 concludes and indicates future work.
In this Section, we provide a first-order modal version of the axioms of UFO developed in [Gui05]. For our purposes, the first order modal logic S5 plus the Barcan formula and its converse suffices [FM12]. That means that we assume a fixed domain for every possible world. This assumption is traditionally associated to a possibilistic view of the entities of the domain, namely, the domain includes all the possibilia. In the following formulas, we shall drop the universal quantifier in case its scope takes the full formula, that is, all the open formulas are understood as universally quantified. Moreover, in this setting, all the axioms and the theorems that follow from them are necessarily true.
The main taxonomy of UFO is depicted in Figure 1. The links of the tree represent inclusions of classes and the children categories are intended to provide a disjoint partition of the parent node. The main difference with respect to [Gui05] is that we dropped the category of sets in favour of the category of mereologial sums.2 Figure 1 can be captured by a list of axioms such as the following (we omit the full list for reasons of space): a1 a2 a3
In the following table, we summarise the notation of the main relation and function symbols, that we deal with in the remainder of this paper.
ed(x; y) ind(x; y) xPy xPPy xOy in(x; y)
Existential dependence Existential independence Parthood Proper Parthood Overlapping Inherence b (x) x :: y ext(x) int(x) x v y x ,! y
Bearer of a moment (function) Instantiation relation Extension of a universal (function) Intension of a universal (function) Specialisation relation Intensional inclusion 2This category has the same motivations and applications as the category of “arbitrary sums” in DOLCE [BM09]. Its role is to allow the modeller to introduce general arbitrary sums of elements of possibly heterogeneous provenance.
a4 a5 a7 a8 a9 a10 a11 a12 a13 a14 ex(x; t) ! Thing(x) ^ Time(t) ed(x; y) $
(ex(x; t) ! ex(y; t)) a6 ind(x; y) $ :ed(x; y) ^ :ed(y; x)
UFO introduces an existence predicate defined on any possible entity, ex(x; t) of existence at time t:3
By means of the existence predicate, we can define the relation of existential dependence between two entities:
The notion of existential dependence is the first place where modal reasoning is required.4 We also define the notion of existential independence accordingly: We adopt the following formalisation of the general extensional mereology. For a discussion of this axioms and their motivations, we refer to [Hov09]. We only recall here the main axioms and definitions; for the purposes of the subsequent definitions, that suffices.
P(x; x) (reflexivity) P(x; y) ^ P(y; x) ! x = y (anti-symmetry) P(x; y) ^ P(y; z) ! P(x; z) (transitivity) O(x; y) $ 9z(P(z; x) ^ P(z; y)) (Overlap) :P(y; x) ! 9z(P(z; y) ^ :O(z; x)) (Strong supplementation) PP(x; y) $ P(x; y) ^ :P(y; x) (Proper Part) 9xf (x) ! 9z Ff (z) (Fusion) In axiom (a13), Ff (z) is an abbreviation for the following formula: Ff (z) $ 8y(O(y; z) $ 9w(f (w) ^ O(w; y))))
Axiom (a13) reads as follows “if f is non-empty, then z is a fusion of the all the f -things”, where f is a formula that does not contain z and y as free variables. In fact, axiom (a13) is a schema.5 By strong supplementation, if the fusion exists (i.e. if f is instantiated), then it is unique. Moreover, in what follows, we shall assume that the f s that may occur are always instantiated. Thus, we can introduce the sum of f things by means of Russellian definite description. a15
s z:Ff (z) = i z: 8y(O(y; z) $ 9w(f (w) ^ O(w; y))) (Sum of f -things) 3For reasons of space, we do not explicitly discuss here the nature of the category Time; we add it as a separate subcategory of Thing.
4Existential dependence is indeed a genuinely modal notion. However, it is interesting to investigate whether it is viable to present a non-modal version of UFO by replacing the existential dependence with the non-modal axiomatization of the “grounding” relation between particulars, cf. [Fin12]. The motivation for that move is to provide a purely first-order version of UFO. We shall investigate this approach in future work.
5Our formulation of general sums corresponds to the third definition proposed in [Var16] and it is the one used or instance in DOLCE, cf. [MBG+03].
Moments are sometimes known as what tropes, abstract particulars, or particular qualities in the philosophical literature [Gui05]. In UFO, moments can be viewed as individualised properties, such as the color or the weight of an object, for the case of intrinsic moments, or a kiss or a handshake, for the case of relational moments (relators). a16 Moment(x) ! IntrinsicMoment(x) _ Relator(x) a17 :9x(IntrinsicMoment(x) ^ Relator(x))
The relation that connects moments to the object that they are about is the relation of inherence, which is captured by the following axioms. a18 in(x; y) ! Moment(x) ^ Endurant(y) a19 in(x; y) ! ed(x; y) a20 :in(x; x) a21 in(x; y) ! :in(y; x) a22 in(x; y) ^ in(y; z) ! :in(x; z)
That is, a moment can be defined as an endurant that inheres some endurant, which is the bearer of the moment. a23 Moment(x) $ Endurant(x) ^ 9y in(x; y)
A moment cannot inhere two separate individuals: a24 in(x; y) ^ in(x; z) ! y = z
By axiom (a23), the bearer of a moment always exists and, by (a24), the bearer of a moment is unique. Hence, we can define the following function symbol to indicate the unique bearer of a moment: a25 b (x) = iy: in(x; y)
Substantials are endurants that are not moments. Substantials represent concrete objects of our everyday experience and are described by means of universals and moments. Since “there are no propertyless individuals” ([Bun77], the following axiom is required. a26 Substantial(x) ! 9y in(y; x)
Two substantials that are disjoint (they do not overlap, cf. axiom (a10)) are existentially independent, that is, the only ontological dependence between substantials may be that of (essential) parthood: a27 Substantial(x) ^ Substantial(y) ^ :O(x; y) ! ind(x; y)
Substantials are then subsequently divided into objects and amounts of matter (cf. Figure 1). 3. Universals In this reformulation of UFO, universals are still in the domain of quantification, that is they are, from a logical perspective, first-order citizens. The relation of instantiation relates the individuals and the universals that may categorise them. a28 x :: u ! Individual(x) ^ Universal(u)
Universals then are divided into substantial universals and moment universals depending on which type of entity they are related to. a29 a30
Universals in [Gui05] (Axiom 22, p. 221), are assumed to satisfy the principle of instantiations [Arm97], that is: f1
(9y y :: u)
When defining the extension of a universal as the fusion of the entities that instantiate the universal, we need here a stronger principle, that entails (f1) and that always excludes empty universals: a31
In [Gui05], the extension of a universal is a set, for this reason the version of UFO of [Gui05] admits sets as particulars in the ontology. The extension of a universal is there defined by means of the following formula ([Gui05], Definition 6.5, p. 219.): f2 ext(u) = fx j instantiates(x; u)g
We replace here sets with mereological sums.6 Axiom (a13) was indeed a schema. The f s can be here instantiated by open formulas x :: u, where u is a universal in UFO. a32 s z: x :: u = i z: 8y(O(y; z) $ 9w(w :: u ^ O(w; y))) (Sum of u-instances) The formula s z: x :: u reads as follows “z is the sum of the xs that instantiate u”. Since we are assuming that the universals are always non-empty (cf. axiom (a31)), by axiom (a13), the sum always exists. Moreover, the sum is unique by axiom (a11). Henceforth, we can introduce a functional symbol that indicates the extension of a universal intended as the mereological sum of the individuals that instantiate it. a33 ext(u) = s z: x :: u
The function symbol ext is well defined because of the unicity and the existence of the mereological fusion. Moreover, since the extensions of universals is a mereological sum, if a particular instantiates a universal, by axiom (a32), then the particular is part of the extension of the universal.
6An alternative approach to our mereological definition of the extension of universal is to keep sets as particulars in the ontology and introduce (a number of) axioms of the Zermelo-Fraenkel first-order version of set theory. We leave a comparison of the two approaches for future work.
t1 x :: y ! P (x; ext(y))
We introduce now the specialisation relation between universals, which is defined in terms of extensional inclusion. a34 x v y ! Universal(x) ^ Universal(y) a35 x v y $ 8z(z :: x ! z :: y)
By means of this definition, it follows that the specialisation relation is reflexive and transitive: t2 x v x t3 x v y ^ y v z ! x v z
We approach here the definition of the intension of a universal and we relate it to its extension. The relationship between the intension and the extension of a universal is captured by establishing the following quite classical philosophical principle: given two universals u and v, if the intension of u is included in the intension of v, then the extension of v is included in the extension of u. Note that, as we shall see, the other direction of that principle entails that co-extensional universals have the same intension, which is rather strong and amounts to reducing universals to the sums of the entities that they instantiate, a position that contrasts with the cognitive motivations of UFO.7 Notice that in this treatment, we assume that the intensions of universals are time-independent.
Firstly, we define the following notion of partial characterisation of a universal, which is reflexive and transitive.8 a36 a37 a38 a39
PartiallyCharacterise(u; u)
Axiom (a39) and (a40) are illustrated as follows. Suppose that the universal man is characterised by animal and rational. Then, everything that is a man, must be an animal and must be rational (by (a39)) and everything that is both rational and an animal must be a man (by (a40)).
By means of the relation of partial characterisation, we can define the intension of a universal u as the fusion of all the universals that partially characterise u. By axiom 7In [Gui05], the intension of a universal was approached as follows. Firstly, the elementary specification of a universal is introduced as the collection of the universals v that specify some of the instances of u, cf. (Definition 6.7, p. 220). Once the notion of elementary specification is defined, the notion of characterisation is available and, by means of that, we can define the intension of a universal in terms of elementary specifications.
8We could also assume a strict notion of partial characterisation that excludes that a universal can be specified by itself. In that case, we need to assume an axiom that states that every universal is partially characterised by another universal. We can do that by assuming that universals are divided into atomic and complex universals and assume that complex universals are characterised by means of a number of atomic universals, along the line of the definition of complex concepts in [SMP15]. (a13), since every universal is always partially characterised by at least one universal, we can assume the following definition. a41 intension(y; u) $ y = s z:PartiallyCharacterise(v; u)
Since the intension of a universal is unique (due to the unicity of the fusion), we can introduce the function symbol int that indicates the intension of a universal: a42 int(u) = y $ intension(y; u)
By means of this definition, we can define the relation of intensional inclusion between universals as follows. a43 u ,! u0 $ P (int(u); int(u0))
That is, a universal u is intensionally included in u0 if and only if, the intension of u is a part of the intension of u0.
We can show now that if u is intensionally included in u0, then the extension of u0 is part of the extension of u. We show that by showing that every instance of u0 is an instance of u.
t4 u ,! u0 ! ext(u0) v ext(u)
Suppose that the intension of u is part of the intension of u0 and that x :: u0. Then, by axiom (a39), x instantiates every universal in the intension of u0. Since the intension of u is included in the intension of u0, then x instantiates every universal in the intension of u. Thus, by (a40), x instantiates u.
We refrain from assuming the other direction because of the following reasons. f3 ext(u0) v ext(u) ! u ,! u0
Suppose that the extension of u coincides with the extension of u0, then by (f3), we would infer by strong supplementation that also their intensions coincides. This amounts to viewing universals as definable extensionally, against the idea of UFO that construes them as intensional properties (cf. [Gui05], p.120, and [Gui15]).
To conclude our presentation of universals, we briefly approach a formalisation of the hierarchy of types of universals in UFO (cf. [Gui05], Chapter 4). Universals are divided according to the following rationale: the type of entity that they apply to, their being sortals or non-sortal, their being rigid, anti-rigid, or non-rigid. In what follows, we present one branch of the taxonomy tree to illustrate the possibilities (Figure 2).
Sortals are defined by means of the following two axioms: firstly, every sortal is specialised by a substance sortal; secondly, substance sortals provide a partition of the individuals. a44 a45
We phrase the definitions of rigidity, non-rigidity, and anti-rigidity for universals in UFO as follows: a46 a47 a48 a49 a50 a51
Rigid, non-rigid and anti-rigid sortal universals are defined by the following axioms (note that the definition for rigid, non-rigid, and anti-rigid non-sortals are analogous).
One important aspect that is missing in our treatment of sortals is the role of identity criteria: Identity is bound to sortals, i.e., there are is no identity judgement that can be done without the support of a sortal. In [Gui15], sortal-bounded identity principles are approached by the use of individual concepts that trace individuals from world to world. In future work, we envisage using individual concepts in order to characterize sortal dependent identity criteria. In other words, each sortal dependent identity criteria would manifest itself as constrains over the type of states that can be referred to by the individual concepts classified by that sortal.
We started developing a first-order modal version of UFO. Future work is planned specifically in two directions. Firstly, we shall provide an exhaustive axiomatisation of UFO in first-order modal logic, for instance by approaching the treatment of quality structures and the theory of relators. Secondly, we are interested in developing the taxonomy of universals in full detail by introducing identity criteria provided by sortals and by approaching phased sortals (i.e., roles and phases).