


Overview
General Formal Ontology (GFO)

14.2 Set and Settheoretical Relations
The membership relation is the
basic relation of set theory. denotes the category of all
sets, represented as
a unary predicate. Usually, the notation is used for typefree systems
(e.g. ZF), but it may be adapted for typed languages.
implies that either and are both sets, or is a socalled
classurelement and is a set. The
subset relationship is defined in terms of
membership:
.
We include in the ontology of sets an axiomatic fragment of formal set theory,
say of ZF, in particular, the axiom of extensionality:
As sets can be nested, we can consider all
seturelements that occur in a set. First,
there is the least flattened set
, which extends the
nested set on the first level of nesting with all classurelements
contained in any depth of nesting. That means, satisfies the
conditions , and for every holds that
. Then the class
is a classurelement and
,
called the support of , contains
all classurelements of and only them. A class is said to be pure
if
.
Robert Hoehndorf
20061018

