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 Gärdenfors's conceptual spaces [Gä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
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.
Specialisation relation x → y Intensional inclusion 2.1. Existence and existential dependence UFO introduces an existence predicate defined on any possible entity, ex(x,t) of existence at time t:
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. a7 P(x, x) (reflexivity) a8 P(x, y) ∧ P(y, x) → x = y (anti-symmetry) a9 P(x, y) ∧ P(y, z) → P(x, z) (transitivity) a10 O(x, y) ↔ ∃z(P(z, x) ∧ P(z, y)) (Overlap) a11 ¬P(y, x) → ∃z(P(z, y) ∧ ¬O(z, x)) (Strong supplementation) a12 PP(x, y) ↔ P(x, y) ∧ ¬P(y, x) (Proper Part) a13 ∃xφ (x) → ∃z F φ (z) (Fusion)
In axiom (a13), F φ (z) is an abbreviation for the following formula:
Axiom (a13) reads as follows "if φ is non-empty, then z is a fusion of the all the φ -things", where φ 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 φ is instantiated), then it is unique. Moreover, in what follows, we shall assume that the φ s that may occur are always instantiated. Thus, we can introduce the sum of φ things by means of Russellian definite description.
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).
The relation that connects moments to the object that they are about is the relation of inherence, which is captured by the following axioms.
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) ∧ ∃y in(x, y)
A moment cannot inhere two separate individuals:
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:
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) → ∃y 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).
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.
Universals then are divided into substantial universals and moment universals depending on which type of entity they are related to.
a29 SubstantialUniversal(u) ↔ Universal(u) ∧ ∀x(x :: u → Substantial(x)) a30 MomentUniversal(u) ↔ Universal(u) ∧ ∀x(x :: u → Moment(x))
Universals in [Gui05] (Axiom 22, p. 221), are assumed to satisfy the principle of instantiations [Arm97], that is:
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 Universal(u) → ∃y y :: u 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.):
We replace here sets with mereological sums.6 Axiom (a13) was indeed a schema. The φ s can be here instantiated by open formulas x :: u, where u is a universal in UFO. The formula σ 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.
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. We introduce now the specialisation relation between universals, which is defined in terms of extensional inclusion. a34 x y → Universal(x) ∧ Universal(y) a35 x y ↔ ∀z(z :: x → z :: y) By means of this definition, it follows that the specialisation relation is reflexive and transitive:
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 PartiallyCharacterise(u, u ) → Universal(u) ∧ Universal(u ) a37 PartiallyCharacterise(u, u) a38 PartiallyCharacterise(u, u )∧PartiallyCharacterise(u , u ) → PartiallyCharacterise(u, u ) a39 PartiallyCharacterise(u, u ) ∧ x :: u → x :: u a40 (PartiallyCharacterise(u, u ) → x :: u) → x :: 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 (a13), since every universal is always partially characterised by at least one universal, we can assume the following definition. 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:
By means of this definition, we can define the relation of intensional inclusion between universals as follows.
That is, a universal u is intensionally included in u if and only if, the intension of u is a part of the intension of u .
We can show now that if u is intensionally included in u , then the extension of u is part of the extension of u. We show that by showing that every instance of u is an instance of u.
Suppose that the intension of u is part of the intension of u and that x :: u . Then, by axiom (a39), x instantiates every universal in the intension of u . Since the intension of u is included in the intension of u , 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.
Suppose that the extension of u coincides with the extension of u , 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 Sortal(x) → ∃y(SubstanceSortal(y) ∧ x y) a45 Endurant(x) → ∃!y(SubstanceSortal(y) ∧ x :: y)
We phrase the definitions of rigidity, non-rigidity, and anti-rigidity for universals in UFO as follows: 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).
a49 RidigSortalUniversal(x) ↔ SortalUniversal(x) ∧ Rigid(x) a50 NonRidigSortalUniversal(x) ↔ SortalUniversal(x) ∧ ¬Nonrigid(x) a51 AntiRidigSortalUniversal(x) ↔ SortalUniversal(x) ∧ Antirigid(x)
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).