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
Its second argument is always a category, the first argument can be
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
The definable extension relation, , is a cross-categorial
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
Note, that the existence axiom contradicts the foundation axiom for
sets, in case of existence of non-wellfounded categories. For this
reason, we do not assume the foundation axiom for sets.