


Overview
General Formal Ontology (GFO)

14.3 Instantiation and Categories
is a predicate that represents the (meta)category of all
categories. We do not consider to be an instance of itself.
The symbol denotes
instantiation.
Its second argument is always a category, the first argument can be
(almost) any
entity. If the second argument is a primitive category, then the first
must be an individual. Individuals  in general  can be
understood as urelements with respect to instantiation. Since we
assume categories of arbitrary (finite) type, there can be arbitrarily
long (finite) chains of iteration of the instantiation relation.
Since sets have no instances (they have elements) they can be
understood as another kind of urlements w.r.t. instantiation. On the
other hand, categories do not have elements, but instances, hence
categories are urlements with respect to the
membership relation.
The definable extension relation, , is a crosscategorial
relation, because it connects categories with sets and is explicitly
defined in the following way:
.
We may stipulate the existence of the set of all instances of a
category by the following axiom (existence axiom):
.
If we assume this axiom then we may define the extensionality
operator
for categories:
.
Note, that the existence axiom contradicts the foundation axiom for
sets, in case of existence of nonwellfounded categories. For this
reason, we do not assume the foundation axiom for sets.
Robert Hoehndorf
20061018

