Universal Space in GFO

Abstract

Space, besides time, is one of the most fundamental categories. The top-level ontology General Formal Ontology (GFO) includes a space theory as one of its modules, called GFO-Space. Former work presents axiomatizations in connection with GFO-Space and its core notions of space regions and their boundaries (leading to surfaces, lines and points), together with relations between those space entities. In contrast to standard mathematical and physical theories in space-related applications, among the space entities of GFO there is none yet that covers “all of space” or “all space regions at once”, which we call 'universal space'. In the current paper, we address the problem of introducing the notion of universal space, motivated by aligning the theory more easily with the usual understanding and treatment in standard mathematical modeling. Our approach to its solution sets out from extending GFO-Space by (1) the category of balls, in order to (2) define a metric by recourse to balls. On that basis, we consider constructions of universal space and clarify that notion ontologically against the background of GFO. This procedure is associated with classifications of shapes of space entities and further future work.

Keywords

• Top-level ontology
• GFO
• ontology of space
• universal space
• metric space

-

CEUR ceur-ws.org

1. Introduction

From its early days on, the General Formal Ontology (GFO) [ 1, 2 ] has been concerned with space and time as two fundamental categories for which adequate theories should become part of. Its theory of space, GFO-Space, has been axiomatized in first-order logic (FOL) in a series of theories including those in [ 3, 4, 5 ]. It is currently reworked into a dedicated module in GFO 2.0 [ 6 ], the next version of the top-level ontology. The present paper continues this line of research by extending GFO-Space with steps in three diferent directions that build upon one another, despite originating from diverse motivations.

Analogously to its theory of time [ 7 ], GFO research on space is strongly inspired by the work of Franz Brentano [ 8 ]. One specialty is the relation of coincidence of boundaries of space nEvelop-O LGOBE CEUR Workshop Proceedings entities, which allows distinct boundaries to have no distance between them. While this is a useful feature for modeling entities with conflicting properties without any spatial gap, it complicates other common constructs and means, among them measuring the distance between space entities. Indeed, the introduction of a (pseudo)metric within GFO-Space has been a goal for a long time, as distance and representing measurements are crucial for applications.

Besides Brentano’s work, GFO-Space is influenced to some extent by Leibniz’ idea of relational space. Main aspects of the latter are (1) that space entities are dependent on material entities that stand in relations to each other and (2) that particular relations are constitutive for the determination of space. As two examples of such relations one may consider the betweenness of points and the equidistance between four points, which have been utilized by Alfred Tarski in his work on axiomatic geometry [ 9 ]. Similar to Leibniz, we assume that space regions derive from material objects and relate to each other, thereby giving rise to further regions. The category of space regions is very fundamental for GFO-Space (it is represented as a primitive in its FOL axiomatizations) and is intended to grasp three-dimensional, extended entities, which are assumed to be bounded and thus cannot be infinitely extended. Consequentially, it follows from the axiomatization in [ 4 ] that there is no greatest space entity that would cover “all others”, “all of space”, and not even “all space regions” only. Put diferently and up to now, GFO-Space does not enjoy any notion of universal space.

Obviously, this stands in conflict with Newton’s approach of a container space [ 10 ], for example, as well as with the usual understanding of space as broadly assumed in mathematics and physics. There, space is seen as universal space, i.e., as a kind of container in which material objects are located and which comprises “all” space entities. This established practice in mathematics suggests to us to at least consider relating GFO-Space to the notion of universal space and thereby analyze the latter ontologically.

Another line of extending GFO-Space concerns morphology. The aspect that space entities exhibit shapes has not yet been integrated into GFO-Space. Space entities are thus not yet explicitly distinguished in terms of their shapes. One topic of interest is to study which shaperelated classification can already be achieved by means of any selected axiomatization. Another topic, related to the former, is to see what becomes possible by extending the signature and axiomatization in order to capture certain categories of shapes. For the purposes of the present paper, it turns out that a limited extension with the shape-based category of balls1 yields a theory that allows for progress regarding defining a metric and the problem of universal space.

The paper proceeds with reporting briefly on related work in Section 2, before Section 3 summarizes key notions from GFO-Space and elaborates on several of its philosophical foundations. Section 4 is devoted to a technical extension of the axiom system established for GFO-Space so far. In particular, it contributes (1) the introduction of an initial, tailored axiomatization of balls (including their center and radius) and (2) the definition of a distance relation for GFO-Space, based on balls, together with evidence that it satisfies the conditions of a pseudometric. Section 5 then discusses the treatment of notions of universal space, before the paper concludes with further discussion and an outlook at future work in Section 6.

1We follow the mathematical distinction in [ 11 ] between spheres and balls. A ball is a solid three-dimensional body, extended in all directions around a center point up the exact same distance, the ball’s radius. A sphere is the surface of a ball with the same center and radius, i.e., a 2-dimensional entity embedded in 3-dimensional space.

2. Related Work

One of the overarching principles of our investigations is the axiomatic method, fully developed by David Hilbert [ 12, 13, 14 ] as a part of Hilbert’s program. We extend this framework by adding an ontological level in form of a top-level ontology. Another source of our investigations are the ideas of Alfred Tarski who established the research field of model theory [ 15 ].

Starting with a very narrow perspective and within the field of applied ontology, to the best of our knowledge, we are not aware of other approaches that relate to top-level axiomatizations of space on a similar basis, i.e., adopting the approach of Franz Brentano [ 8 ] and/or establishing axiomatic systems involving coincidence. However, there is earlier work in philosophy in response to Brentano, e.g. by Roderick M. Chisholm [ 16 ], and work including formalizations referring to boundaries [17], which we have taken into account and analyzed earlier, a.o. in [ 4 ]. We further point to Ingvar Johansson’s material on space in [18], which we also draw inspirations from. CODI [19], primarily developed by Torsten Hahmann, is a recent and extensive multidimensional theory of mereotopology based on two eponymous primitives, (CO) spatial containment and (DI) a relation for comparing dimensionsionality of space entities. A striking diference to GFO-Space is the availability of cross-/multi-dimensional entities in CODI. [19] includes a recommendable elaborate state of the art, including relating the approach to GFO-Space. Prior work of our own that contextualizes the present paper is referred to in the previous section, whereas the subsequent Section 3 summarizes and stresses details of our former work that are of relevance for the current contribution.

Broadening the view towards the domain of top-level ontologies and their treatment of space, one observes diferent approaches concerning the inclusion of axiomatic theories of space. For instance, DOLCE [20] deliberately avoids the inclusion of a detailed space axiomatization in order to leave users of the ontology more freedom. In the case of BFO [21], as another example, we find categories similar to those in GFO, e.g. of space regions and points, but we are not aware of an extensive formalization of a space theory (though of some formal work on temporal and spatial projection [22]).

We cannot broaden our perspective to work on space in general, because this fundamental notion is being dealt with in a plurality of areas, such that the literature is vast. Sufice it to say that axiomatic approaches in mathematics – and in geometry, in particular – play another major role for our work. Anew, Hilbert and Tarski are important representatives in this respect [ 9, 13 ]. Beeson [23] gives an impression of the rich amount of theories and considerations available even if narrowing down within mathematics, without yet thinking of other related notions such as topological spaces, manifolds, and many more.

3. Basic Principles of GFO-Space

In this section we not only establish the basic terminology for the remainder of the paper and summarize key aspects of GFO-Space mainly from [ 4, 5 ], but in addition we provide some of its underlying philosophical attitudes with novel and extended views.

First of all, the two central kinds of space entities in GFO are space regions and boundaries. Space regions are construed as three-dimensional entities of a certain finite extent and with genuine properties such as their shape. Due to being delimited, every space region is tied to a spatial boundary, which itself can be subject to having a boundary. Therefore, boundaries can be distinguished into two-dimensional surfaces, one-dimensional lines and zero-dimensional points,2 which constitute important special cases among all kinds of lower-dimensional entities.

Let us shift the perspective from categories of space entities to key relations they stand in. Besides the relation of spatial boundary of, GFO-Space addresses mereological relations together with “relatives” of parthood, such as tangential part-of and inner part-of (i.e., non-tangential). Notably, while spatial part-of presupposes the same dimension among its arguments, being hyper part-of crosscuts at least one and possibly multiple levels of dimension. For instance, a point interior to a space region is no part of it, but is a hyper part of the region. The upper point of ‴ in Figure 1 is an example of a hyper part of the depicted cylinder . Overall, Figure 1 illustrates most of those notions described so far, including space region and spatial boundary (with surface, line, and point) as well as part-of, hyper part-of, tangential and inner parts.

Despite referring frequently to “dimension” in the paragraphs above, dimensions themselves are not in the domain of GFO-Space. However, there is a relation of being equidimensional. In connection with that, tangential part-of and inner part-of are broader than (hyper) part-of insofar that the former apply to arguments that can be equidimensional or not, because their definitions allow their arguments to stand in either the part-of or the hyper part-of relation.

Finally,3 the relation of coincidence and its underlying ideas, originating from Franz Brentano [ 8 ], is an outstanding relation of GFO-Space, which applies to spatial boundaries only. Intuitively speaking, two distinct boundaries that coincide have no distance between them, but “touch” at their overall extent (or one may say, those boundaries are “congruent”); cf. Figure 2.

Following Franz Brentano [ 8 ] further, a strong non-reductionist stance underlies GFO-Space, where higher-dimensional entities shall not be and are not reduced to lower-dimensional ones. Accordingly, there remains a clear diference between, for example, a space region and the set of its hyper parts, which cannot be equated with one another, notwithstanding the fact that 2More precisely, the distinction of boundaries is into surface/line/point regions, of which surfaces, lines and points are the special cases in which each such region is in addition connected (in contrast to scattered).

3We mention only the major relations of relevance in the sequel; various specific others are defined in [ 4, 5 ]. the latter set allows for uniquely identifying the space region (Theorem T5 in [ 4 ]). Similarly, we aim at complementing contemporary mathematical treatments of spatial modeling with an axiomatic approach. This should transcend formal reductions of space entities to mere sets of points within, say, a Euclidean (container) space. Likewise, we see our work on a similar level of abstraction as the study of topological manifolds. The diference consists in the mathematical framework, where also topological manifolds rely on sets of points of the Euclidean space, established over the real numbers. Instead, the framework of GFO-Space is based on mereotopological notions that – we think – is better suited to capture genuine spatial phenomena and properties axiomatically. Morphology and shapes, resp., are prime targets in this respect, where characterizing balls below is just a minimal start.

Another aspect concerns the distinction of relational and container space approaches. In GFO, space regions are abstracted from material objects, such that space is generated and determined by material objects and the relations that hold between them. This phenomenal space resulting from material objects appears to the mind, such that we further claim that there is some subject dependence. Seemingly in contrast, that leads to the question of how to analyze the idea of a container space. A container can be understood as a background-space which – according to Immanuel Kant [24] – can be accessed without any experience. Contrary to Kant, we defend the position that the background-space, which we call universal space, is abstracted from our real experience of the material things in the world. We first experience material things in the world, then we abstract forms and shapes from these things, and finally we embed these forms into a universal space. Some aspects of this process have been analyzed by Jean Piaget [25].

Yet another matter of relevance derives from our axiomatic approach, namely its potential for the classification of space entities. For every first-order signature and logical language on its basis, a system of invariants results from sentences in the logical language; cf. [ 3 ] for initial remarks along these lines, while the overall topic shall be pursued in our future work.

We conclude this section by returning to GFO-Space and the axioms systems developed for it. In particular, in the remainder of the paper we refer to the system of axioms in [ 4 ], therein called BS, here as BS16, and to the extension developed in [ 5 ] as BS19 (indices indicate the publication year). BS16 is based on four primitives: the category of space regions ( ), the binary relations of being a spatial part ( binary relation of spatial coincidence ( ) and being a spatial boundary ( ), as well as the ). The overall axiomatization BS19, comprising of BS16 and the additions in [ 5 ], contains 4 primitive relations (B1-B4), 37 definitions (D1-D37), 33 axioms (A1-A33) and 22 theorems (T1-T22). As Section 4 builds upon this system, the numbering of signature elements and axioms are continued across the works and do not start as D1 for the first definition herein, for example. Note, however, that argumentation and results in the remaining sections hardly utilize axioms of BS19, such that there is no need to list all of them herein; where we rely on an axiom, it is explicitly stated.

4. Introducing a Distance Relation by means of Balls

Oriented at our main goals for this paper, we proceed via three main steps in the next sections. 1. We provide an axiomatic extension BS23 of the theory BS19, introducing balls together with related and required notions, including a treatment of real numbers. 2. A pseudometric is added to BS23, basically defined via balls (and auxiliary notions). 3. We account for constructions of a universal space given BS23.

The introduction of balls into our theory will rely on the notions of center and radius, where the latter is captured as a real number for each ball. Accordingly, certain preliminaries must be dealt with before we can introduce balls axiomatically.

4.1. Relativization of the Theory and Integration of the Real Numbers

In order to equip balls with a radius, we aim at introducing the ordered field of real numbers into BS23. As such an extension of the domain interacts with existing definitions, axioms and theorems, prior to that we relativize BS19, the GFO-Space axiomatization that we start from, to space entities. For this purpose, first D 38 defines a new sub domain predicate () .

D38. () ∶= () ∨ ()

(Space entities are space regions or lower-dimensional entities.)

For the primitive relations ,

and we add a new domain constraint axiom.

A34. (, ) ∨ (, ) ∨ (, ) → () ∧ () (Only space entities are subject to the relations , and .)

A precise inductive description of the process of relativization w.r.t. a predicate can be found in [26]. For a formula we obtain the relativized version by replacing all subformulae of the form ∀ by ∀ (() → ) , and all subformulae of the form ∃ by ∃ (() ∧ ) now modify BS19 by replacing any definition of the form ( 1, ..., ) ∶= by ( ⋀=1 ( ) ∧ , and any axiom or theorem with free variables 1, ..., by ⋀=1 ( ) → . in . We 1, ..., ) ∶= For example, the relativization of axiom A12 (() → ∃ ( , ) ) yields () → (() → ∃ (( ) ∧ ( , ))).

However, since only space entities are subject to the relations and , this relativization is

equivalent to A12 under D38 and A34. A similar efect occurs for most definitions, where newly defined categories inherit their exclusive applicability to space entities from the categories that were used to define them. Eventually, relativizing BS19 afects only two of its definitions, five axioms and seven theorems.4

After these preparations, we extend BS19 by adding a theory for capturing first-order properties of the real numbers. New signature elements are a (sub) domain predicate (thus unary) for the reals ‘∈ ℝ’, a binary predicate < for their ordering, functional constants 0 and 1 and binary function symbols for addition + and multiplication ×. We also use the symbols ≤, ≥ and > in the usual way as abbreviations. The theory we adopt consists of domain constraints for each new symbol and of 12 well-known first-order axioms of ordered fields [ 27].5

4.2. Balls with Center and Radius

Next, we introduce centers, radii and balls as new primitives for BS23 (B5–7), in order to declare ifrst axioms on them.

( is the center of the ball . Alternatively: is a ball around )

( is a ball.) ( is the radius of the ball .) B5. () B6. (, )

B7. (, ) A35. () → () A36. (, ) → 0() ∧ ( ) ∧ (, ) A37. (, ) → > 0 ∧ ( ) A38. 0() ∧ > 0 → ∃! ((, ) ∧ ( , )) A39. () → ∃ ( , ) A40. (, ) ∧ ( , ) → (, ) A42. () → ∃! ( , )

A35–37 are domain constraint axioms for these new primitives. Every ball is a topoid (i.e., a connected space region) with a point (0 ) as its center (an inner hyper part) and a positive real number as its radius.

We introduce existence and uniqueness conditions. For any point and any positive real number there exists a unique ball having as center and as radius (A38). Due to coincidence in GFO-Space, the center of a ball is not unique as points (0 ) are concerned – but it is unique w.r.t. the coincidence equivalence class of all center points of the ball. That means, the same ball has diferent center points, but those are all coincident (i.e., there is no distance between them, cf. D39 in the next section).

(Every ball is a topoid.) (The center of a ball is an inner point.) (The radius of a ball is a positive number.) A41. (, ) ∧ (, ) → ( , )

(Every point that coincides with the center of a ball is also a center of that ball.) 4For precise reference, these are D12, D13, A2, A4, A8-10, T1-5 and T8-9, all from [ 4 ].

5For a complete list of the definitions and axioms in BS23 as well as detailed proofs for theorems and propositions introduced subsequently in this work, please contact us.

(For any given radius and center point there is a unique ball.)

(Every ball has a center.) (Any center points of the same ball coincide.) (Every ball has a unique radius.)

Since the radius of a ball is unique, we introduce it also as a function:6

() = ∶↔ ( , ).

When we think of balls, we automatically assume that a ball with a smaller radius is actually smaller than a one with a bigger radius. This is captured in Axiom 43 for the special case of two balls sharing a center point.

A43. (, ) ∧ (, ) ∧ () ≤ ( ) → (, )

(If two balls share a center point, the one with smaller radius is a part of the other one.)

Axiom 43 together with 41 and the antisymmetry of the

relation (A5 in [ 4 ]) entail T23.

T23. (, ) ∧ (, ) ∧ (, ) ∧ (, ) ∧ (, ) → = (A ball is uniquely determined by its radius and the coincidence equivalence class of its center.)

The final axiom on balls shall achieve that the universal space introduced in Section 5 is topologically equivalent to an open ball and, in particular, it shall not exhibit any holes. A44. 0() ∧ ( ) → ∃ ((, ) ∧ (( , ) ∨ ℎ ( , ))) (For any point and any space entity, there is a ball around that point that contains the space entity.)

4.3. A Distance Relation with Pseudometric Properties

Our goal in this section is to introduce a metric for GFO-Space. More precisely and in view of the coincidence relation (relating distinct points that are intuitively understood to have zero distance) the efort results in providing a pseudometric. For this purpose, we first define a distance relation by means of balls and then enhance BS23 with further axioms to ensure that the distance relation is well defined and has the desired properties of a pseudometric.

The basic idea for defining the distance between two points (predicate 0 ) originates from this observation: Two non-overlapping balls touch each other if and only if the distance of their centers equals the sum of their radii (see Figure 3).

Two equidimensional space entities touch each other if they are externally connected, i.e., if they are connected7 but do not overlap. Hence, balls lend themselves to defining the distance between two points if the latter are chosen as centers of two balls that are externally connected ( ). Since balls are topoids (A35) and extended entities themselves (due to their non-zero 6We overload the symbol , as the reading is easily distinguished by the arity (and the respective context). Being a function on space entities only, it is a partial function w.r.t. the overall domain of BS23.

7To stay within the terminology of [ 4 ]: if their sum is a connected space entity. radius by A37), considering the distance of a point to itself as well as to coincident neighbors must be treated separately as edge cases, in which the points’ distance is 0.8 Thus we define a predicate (, , ) with the reading ‘the distance between points and is ’ as follows. D39. (, , ) ∶= 0() ∧ 0( ) ∧ (((, ) ∧ = 0) ∨ (¬(, ) ∧ ∃ ((, ) ∧ ( , ) ∧ (, ) ∧ () + ( ) = ))) ( and have a distance of .)

To ensure that this distance relation is unique in its third argument and is well defined for all pairs of points we add the next three axioms.

A45. 0() ∧ 0( ) ∧ ¬(, ) → ∃ ((, ) ∧ ¬ℎ ( , )) (For any two non-coincident points there is a ball around the first that does not contain the second point.) A46. (, ) ∧ 0( ) ∧ ¬ℎ ( , ) → ∃! (( , ) ∧ (, )) (Any point not contained in a given ball is the center of a unique ball that touches the other one externally.) A47. (, 1) ∧ ( , 1) ∧ ( 1, 1) ∧ (, 2) ∧ ( , 2) ∧ ( 2, 2) → ( 1) + ( 1) = ( 2) + ( 2) (The sum of the radii of two externally connected balls only depends on their center points.) Axiom A45 can be seen as GFO’s version of Kolmogorov’s separation axiom, cf. [28, Chapter 16]. Jointly with A46 it enforces that any two points have a distance, by ensuring a ball around a first point out of the two, whereas A 46 implies the existence of a ball around the second that touches the first externally (see Figure 4).

Eventually, A47 guarantees uniqueness of the distance relation in its third argument, i.e., the distance of two points does not depend on the choice of the balls realizing it. Hence and akin to above, we define a functional version of distance, but with symbol :

(, ) = ∶↔ (, , ).

Another observation relates distance and radius, capturing in A48 (via tangential parthood) that the radius of a ball is exactly the distance between its center and any point on its surface. Note that this connection would allow for an alternative definition of the distance relation. A48. (, ) ∧ 0( ) ∧ ( , ) → (, ) = ()

(The distance of the center of a ball to a point of its surface is the radius of the ball.) 8Note that the coincidence relation for points is reflexive on spatial boundaries (A19 in [ 4 ]), so the distance of a point to itself can be regarded as a special case of the distance of two coincident points.

There are four conditions we deem necessary for a distance relation for GFO-Space: 1. (, ) ≥ 0 2. (, ) = 0 3. (, ) = ( , ) 4. (, ) + ( , ) ≥ (, )

if and coincide Observe that 1., 3. and 4. are the conditions for a pseudometric. Since coincident points have a distance of 0, this relation cannot be a metric. However, 1. and 2. together yield a weak version of positive-definiteness.

As direct corollary of these properties we have equal distance of coincident pairs of points: T24. 0() ∧ 0( ′) ∧ 0( ) ∧ 0( ′) ∧ (, ′) ∧ ( , ′) → (, ) = ( ′, ′) (The distance of two points only depends on their respective coincidence equivalence classes.) Next we aim at augmenting BS23 with further axioms such that those four properties desired for can be proved. Indeed, the first three conditions are already satisfied due to the construction of the distance relation in D39, plus A37 requiring that any radius is strictly greater than 0.

The fourth condition is the triangle inequality, which is mildly more demanding in proving it – the remainder of this section is devoted to this endeavor.

First, we postulate four cases for the positional relationship between three points in GFOSpace, that are to be considered in the proof of the triangle inequality: 1. all of them coincide 2. two coincide and one does not coincide with those two 3. none of them coincide, but they lie on a straight line9 4. none of them coincide and they don’t lie in a straight line.

The fourth case is the standard case where the points are coincident with vertices of a proper triangle. In this case there are three unique balls around the points that touch each other pairwise (cf. Figure 5 (1), (2)). This situation is captured via the predicate : D40. (, , ) ∶= ∃ ((, ) ∧ ( , ) ∧ (, ) ∧ (, ) ∧ ( , ) ∧ ( , )) (Three points form a vertex triangle if there are balls around them that touch each other pairwise.)

To characterize the third case we use the following property: If three points lie on a line, there are balls around the outer points that touch in the point in between (cf. Figure 5 (3)). In this connection, D41 defines when two space entities touch at a third one.

D41. ℎ(, , ) ∶= (, ) ∧ ∃ ((, ) ∧ ( , ) ∧ (, ) ∧ ( , ))

Note that an entity that two others touch in need not be the maximal space entity with this property. In fact, if two space entities touch in a third one, they also touch in every part and hyper part of that third one.

Drawing inspiration from Euclidean space, if two balls in ℝ3 touch, they touch in exactly one point. We adopt a similar condition for GFO-Space, modulo coincidence. That means, if two balls touch at a point, they likewise touch in all coincident points. They touch even in ( and touch at .) 9More precisely: there is a straight line and three points on this line that coincide with them. mereological sums of points, where such sums are no boundaries and thus cannot coincide, as coincidence is constrained to equidimensional boundaries in its arguments (A22 in [ 4 ]). From these considerations, we postulate technically A49: A49. () ∧ () ∧ ℎ(, , ) → ∃ (0() ∧ ∀ (( ) ∧ ( , ) → (, )))

(If two balls touch at a space entity, then there is a point such that all parts of the space entity that are spatial boundaries coincide with that point.)

Using this property we can finally define what it means for three points to align: D42. (, , ) ∶= ∃ ((, ) ∧ (, ) ∧ ℎ(, , ))

(There is a straight line containing , and in that order.)

Finally, A50 postulates that the four cases above as exhaustive and mutually exclusive: A50. ((, ) ∨ (, ) ∨ (, )) (, , ) two of them coincide.)

∨. ((, , ) ∨ (, , ) ∨ (, , )) ∨.

(Three points are either in a line or they for a vertex triangle or at least

Using axiom A50 together with the other axioms and definitions allows us to prove the triangle inequality for all cases. Since these proofs are merely technical and do not present interesting ideas, they are not included here (but we share them gladly on request).

5. Universal Space

The final goal for this work is to bridge the gap between relational space approaches and container space approaches. A universal space for GFO-Space, denoted by , shall play the role of a container space. Such a container space is characterized by the condition that it contains all space entities. We assume that a universal space is presented by a set of points. The relation between space regions and sets of points is established by the following theorem from [ 4 ], which states that if a space entity has at least one 0-dimensional hyper part, it is identical with all space entities that have the same 0-dimensional hyper parts.

T5. ∃ (0ℎ (, ) ∨ 0ℎ (, )) → (∀ (0ℎ (, ) ↔ 0ℎ (, )) ↔ = )

For the construction of the universal space we need a similar but potentially stronger identity criterion: Hypothesis (Strong identity criterion). Two space entities are identical if and only if they have the same points as parts or hyper parts.

Note, that this criterion implies that the space entities have the same properties, while it is not clear how to derive these properties from the set of points alone. Since a set has no form, the origin of shapes does not belong to set theory, but to the ontological region of psychology; and it is studied in the field of cognitive science, cf. e.g. [ 29].

Given a model of GFO-Space that fullfills the strong identity criterion, we construct ( ) by equipping the set of all 0 entities (points) in with the pseudometric introduced in Section 4.3. In the following, we denote the interpretation of a symbol in the model by . For a space entity in , we define the set (

) ∶= { ∣ ⊧ 0( ) ∧ (ℎ ( , ) ∨ ( , ))}.

We set ( ) ∶= 0 , which equals the union of the sets over all members of the universe of , as can easily be verified. The idea stated above then boils down to letting ( ) be ( ) equipped with the pseudometric . Although space regions themselves are not, at least not necessarily, subsets of ( ) , we can say: a space region is contained in ( ) if ( ) is a subset of ( ) .

Originally, we considered a diferent construction for ( ) by fixing a point 10 and defining a series of “balls” by [] ∶= { ∣ ⊧ 0()∧∃ ( (, )∧ ( ) = ∧ℎ (, )} . Now we can set ( ) as the union of all [] where is a natural number. As in the previous construction, ( ) is the set ( ) equipped with the pseudometric . By this approach it is clear: If in for any ball the set of points that are hyper parts of is topologically equivalent to a ball in ℝ3, then the universal space is topologically equivalent to ℝ3. 11 Axioms A38, A43 and A44 together ensure that the constructions yield the same result.

If we identify diferent coinciding points, then the basic idea of Brentano’s theory about space and time is lost. Thus for any Model that captures these ideas ( ) cannot be a metric space. Since points are spatial boundaries, though, the restriction of the coincidence relation to points is an equivalence relation (Axioms A19-A21 in [ 4 ]). Because the distance of two points depends only on their respective equivalence classes (T24), induces a distance relation on the quotient space ( )/ . The second condition for in 4.3 together with the pseudometric properties of ensures that this distance relation is indeed a metric.

On the other hand, we may ask whether a standard metric space, as for example the three dimensional Euclidean space ℝ3, can be transformed into a universal Brentano space ( ) , such that the identification of coinciding points, the quotient space ( )/ , yields the space ℝ3. In the 1-dimensional case, such a construction is reminiscent of the model construction for GFO-Time in [ 7 ]. An analogous construction for GFO-Space is an unsolved problem. We expect that there are models of GFO-Space such that ( )/ is isometric to ℝ3. 10 as a constant in BS23 11This does not mean that ()

is a ball, since any ball is bounded.

6. Conclusions

GFO-Space is an ontology that formalizes ideas of Franz Brentano on space and time. His important contribution is a deeper understanding of the notion of the continuum [ 8 ]. Moreover, he introduced the notion of the coincidence of boundaries. GFO-Space axiomatizes an ontological category the instances of which are space regions and space entities derived from them. Another origin of GFO-Space are the ideas of Leibniz that space is relational, i.e., that space is generated and determined by material objects and the relations between them. However, the predominant approach to space is the conception to understand it as a container in which entities are located. This container space plays a decisive role in physics, the natural sciences in general, and in mathematics [18]. In the present paper, we propose a framework that integrates all these approaches into a uniform system. In particular, we close the gap between relational space and container space by starting from a relational space approach and construct a universal space, which can be understood as a container space, from entities within GFO-Space.

6.1. Discussion

A deeper understanding of space requires an investigation of space entities themselves. The usual approach in mathematics is to represent a geometric entity by a set of points in a container space. We defend the idea that the predominant mathematical approaches must be complemented by an axiomatic approach. In Section 4 we followed this approach exemplarily by introducing balls with centers and radii into the theory. It turns out that by this introduction of balls we already gained a much more expressive theory that allows to define concepts like the straightness of a line and, maybe most importantly, an adequate distance relation between points.

Taking the proposed complementation further means, for example, to go far beyond balls and study a direct description of the morphology of space entities; again, this is to be pursued by direct axiomatization and the analysis of axiomatic systems, without a detour through a representation by sets [30, 31].

Our investigation further emphasizes the relevance of pseudometric spaces. The integration of the ideas of Brentano and the presented conception of a universal space may lead to a new view on container space, potentially as a pseudometric space. This appears beneficial in terms of expressive power as well as to maintain Bretano’s ideas on the continuum [ 8 ].

Yet another formal aspect of the direct axiomatic approach concerns the introduction of new invariant systems for the classification of geometric entities. These new invariant systems can be established by using formal languages, notably first-order logic, and corresponding theories. For every signature and logical language on its basis, a system of invariants can be established that divides space entities into corresponding equivalence classes. The invariants can be expressed by the sentences in the logical language.

As a final point, we mention the background of our work concerning the principles of integrative realism [ 1 ], which is hardly addressed above, while several aspects remain open. For example, further investigation is needed to understand the evolution of space and spatial notions w.r.t. the mind. It seems promising to research ideas of J. Piaget [25] further, which provide an important contribution to the evolution of the notion of space. We believe that Piaget’s ideas can be included in the conception of the integrative realism.

6.2. Future Research

The current paper touches a variety of open problems and may open new lines of research. GFO‑Space, in the spirit of Franz Brentano, is a rich theory that raises many questions. In the following we collect some of these problems.

1. Introducing further shapes within the current framework, including planar surfaces, circles, polyhedra, and features such as the volume of a space entity, length of a line, tangent to a line. 2. The problem of the classification of space entities. Such a classification is based on various conceptualizations. Which of the classical results of topological manifolds can be formalized and reconstructed in the current framework? Which would need a further extension of the signature? 3. Metalogical investigations of the considered theories. These include the consistency and (un)decidability of the theories. How many complete extensions of the theories exist? 4. Relations between GFO-Space and the three-dimensional Euclidean space ℝ3. As sketched in Section 5 we currently discuss a mapping of GFO-Space into ℝ3 via the coincidence relation. In any model of GFO-Space, is an equivalence relation on the constructed universal space ( ) , and its quotient space ( )/ is a metric space. We may try to construct a model for which ( )/ is homeomorphic to ℝ3.

Then we can investigate how other space entities of relate to ℝ3. 5. The extension of the current theories to the visual field. Here we start with the notion of an object situation for which we assume the Euclidean metric. If we add an observer to the situation then we must introduce the visual field, depending on the observer. The visual ifeld has usually a non-Euclidean metric. We may ask how to reconstruct a perceived real situation from diferent perspectives (based on the visual field). 6. The application of the presented framework to other theories, but also to practical problems, including the following: a) A psychological investigation in the spirit of Piaget’s approach. Has the motor experience space another metric than the visual space? How can a child learn the coordination of both? b) How can the ideas of GFO be applied to the navigation problem in minimally invasive surgeries? c) Further applications in the fields of anatomy, geography, and environmental sciences.

Acknowledgments

The authors acknowledge the financial support by the Federal Ministry of Education and Research of Germany and by Sächsisches Staatsministerium für Wissenschaft, Kultur und Tourismus in the programme Center of Excellence for AI-research „Center for Scalable Data Analytics and Artificial Intelligence Dresden/Leipzig“, project identification number: ScaDS.AI. [17] B. Smith, A. Varzi, Fiat and bona fide boundaries, Philosophy and Phenomenological

Research 60 (2000) 401–420. [18] I. Johansson, Ontological Investigations, Routledge, 1989. [19] T. Hahmann, Codi: A multidimensional theory of mereotopology with closure operations,

Applied Ontology 15 (2020) 251–311. [20] S. Borgo, C. Masolo, Ontological foundations of DOLCE, in: R. Poli, M. Healy, A. Kameas (Eds.), Theory and Applications of Ontology: Computer Applications, Springer Netherlands, Dordrecht, 2010, pp. 279–295. doi:10.1007/978-90-481-8847-5_13. [21] R. Arp, B. Smith, A. D. Spear, Building Ontologies with Basic Formal Ontology, MIT Press,

Cambridge, MA, 2015. [22] K. Trentelman, A. Ruttenberg, B. Smith, An axiomatisation of Basic Formal Ontology with projection functions, in: K. Taylor, T. Meyer, M. Orgun (Eds.), Advances in Ontologies: PreProceedings of the 6th Australasian Ontology Workshop, AOW 2010, Adelaide, Australia, Dec 7, Council for Scientific and Industrial Research (CSIR), Meraka Institute, Pretoria, South Africa, 2010, pp. 71–80. [23] M. Beeson, A constructive version of Tarski’s geometry, Annals of Pure and Applied Logic 166 (2015) 1199–1273. doi:10.1016/j.apal.2015.07.006. [24] I. Kant, Kritik der reinen Vernunft, Meiner Verlag, 1998. [25] J. Piaget, Die Entwicklung des räumlichen Denkens beim Kinde, Klett, 1975. [26] W. Rautenberg, A Concise Introduction to Mathematical Logic, 3. ed., Springer, London, 2010. doi:10.1007/978-1-4419-1221-3. [27] B. Laferriere, G. Laferriere, M. N. Nguyen, Introduction to Mathematical Analysis I, PDXOpen: Open Educational Resources, 2016. URL: https://pdxscholar.library.pdx.edu/ pdxopen/12. [28] E. Schechter, Handbook of Analysis and its Foundations, Academic Press, San Diego, CA, 1997. [29] G. L. Murphy, The Big Book of Concepts, MIT Press, 2002. [30] L. Albertazzi, A science of qualities, Biological Theory (2015). doi:10.1007/ s13752-015-0213-3. [31] L. Albertazzi, Styled morphogeometry, Axiomathes (2020). doi:10.1007/ s10516-019-09438-x.

References

[1] H. Herre , General Formal Ontology (GFO): A foundational ontology for conceptual modelling , in: R. Poli, M. Healy , A . Kameas (Eds.), Theory and Applications of Ontology: Computer Applications , Springer, Heidelberg, 2010 , pp. 297 - 345 . doi: 10 .1007/ 978 - 90- 481- 8847- 5_ 14 .

[2] F. Loebe , P. Burek , H. Herre , GFO : The General Formal Ontology, Applied Ontology 17 ( 2022 ) 71 - 106 . doi: 10 .3233/AO- 220264.

[3] R. Baumann , H. Herre , The axiomatic foundation of space in GFO, arXiv .org, 2011 . URL: http://arxiv.org/abs/1110.5832.

[4] R. Baumann , F. Loebe , H. Herre , Towards an ontology of space for GFO , in: R. Ferrario , W. Kuhn (Eds.), Formal Ontology in Information Systems - Proceedings of the 9th International Conference, FOIS 2016 , Annecy, France, Jul 6- 9 , volume 283 of Frontiers in Artificial Intelligence and Applications , IOS Press, Amsterdam, 2016 , pp. 53 - 66 . doi: 10 .3233/978- 1- 61499 - 660- 6- 53.

[5] R. Baumann , F. Loebe , H. Herre , Properties defined on the basis of coincidence in gfospace , in: A. Barton , S. Seppälä , D. Porello (Eds.), Proceedings of the Joint Ontology Workshops 2019 Episode V: The Styrian Autumn of Ontology, Graz , Austria, September 23-25 , 2019 , volume 2518 of CEUR Workshop Proceedings, CEUR-WS.org , 2019 . URL: https: //ceur-ws. org/ Vol- 2518 /paper-FOUST3.pdf.

[6] P. Burek , F. Loebe , H. Herre , Towards GFO 2 . 0: Architecture, modules and applications , in: B. Brodaric , F. Neuhaus (Eds.), Formal Ontology in Information Systems - Proceedings of the 11th International Conference, FOIS 2020 , Cancelled / Bozen-Bolzano, Italy, Sep 14-17 , volume 330 of Frontiers in Artificial Intelligence and Applications , IOS Press, 2020 , pp. 32 - 45 . doi: 10 .3233/FAIA200658.

[7] R. Baumann , F. Loebe , H. Herre , Axiomatic theories of the ontology of time in GFO, Applied Ontology 9 ( 2014 ) 171 - 215 . doi: 10 .3233/AO- 140136.

[8] F. Brentano , Philosophische Untersuchungen zu Raum, Zeit und Kontinuum, Meiner Verlag, 1976 .

[9] A. Tarski , What is elementary geometry? , in: L. Henkin , P. Suppes , A . Tarski (Eds.), The Axiomatic Method , volume 27 of Studies in Logic and the Foundations of Mathematics, Elsevier , 1959 , pp. 16 - 29 . doi: 10 .1016/ S0049 - 237X( 09 ) 70017 - 5 .

[10] I. Newton , Mathematische Grundlagen der Naturphilosophie, Meiner Verlag, 1988 .

[11] E. W. Weisstein , CRC Encyclopedia of Mathematics , 3. ed., Chapman & Hall/CRC Press, Boca Raton, FL, USA, 2009 . URL: https://zbmath.org/? q=an:1179 . 00007 .

[12] D. Hilbert , Axiomatisches denken, Mathematische Annalen 78 ( 1918 ) 405 - 415 .

[13] D. Hilbert , M. Toepell , P. Bernays , Grundlagen der Geometrie, Teubner-Archiv zur Mathematik / Supplement, 14. aufl. ed., Teubner , Stuttgart, 1999 . URL: https://zbmath.org/? q=an: 0933 .01031, literaturverz . S. [ 385 ] - 401 .

[14] D. Hilbert , P. Bernays , Grundlagen der Mathematik vol. 1 , Springer, 1934 .

[15] A. Tarski , Über den begrif der logischen folgerung , Journal of Symbolic Logic 2 ( 1937 ) 83 - 84 . doi: 10 .2307/2267371.

[16] R. M. Chisholm , Boundaries as dependent particulars , Grazer Philosophische Studien 20 ( 1983 ) 87 - 95 .