GFO Part I Basic Principles



Ontological Investigations	Conceptual Modelling	Onto-Builder
Axiomatic Foundations	Domain Ontologies	Onco-Workstation
Metalogical Analyses	Ontology Languages	SOP-Creator

			Onto-Med >> Theories >> GFO Part I Basic Principles
			Overview General Formal Ontology (GFO)	Next: 14.3 Instantiation and Categories Up: 14 Ontologically Basic Relations Previous: 14.1 Entity and Existential 14.2 Set and Set-theoretical Relations The membership relation is the basic relation of set theory. $\GSet(x)$ denotes the category of all sets, represented as a unary predicate. Usually, the notation $\in$ is used for type-free systems (e.g. ZF), but it may be adapted for typed languages. $x \in y$ implies that either and are both sets, or is a so-called class-urelement and is a set. The subset relationship $\subseteq$ is defined in terms of membership: $x \subseteq y \Ldef \forall z (z \in x \Limp z \in y)$ . We include in the ontology of sets an axiomatic fragment of formal set theory, say of ZF, in particular, the axiom of extensionality: $\GSet(x) \wedge \GSet(y) \rightarrow (\forall u ( u \in x \leftrightarrow u \in y)) \rightarrow x = y)$ As sets can be nested, we can consider all set-urelements that occur in a set. First, there is the least flattened set $y = \Gtrans(x)$ , which extends the nested set on the first level of nesting with all class-urelements contained in any depth of nesting. That means, satisfies the conditions $x \subseteq y$ , and for every $z \in y$ holds that $z \subseteq y$ . Then the class $\Gsupp(x) = \{ a \:\vert\:$ is a class-urelement and $a \in \Gtrans(y) \}$ , called the support of , contains all class-urelements of and only them. A class is said to be pure if $\Gsupp(x) = \emptyset$ . Next: 14.3 Instantiation and Categories Up: 14 Ontologically Basic Relations Previous: 14.1 Entity and Existential Robert Hoehndorf 2006-10-18

Onto-Med >> Theories >> GFO Part I Basic Principles

14.2 Set and Set-theoretical Relations