SUO: Bootstrap Ontology

["Robert E. Kent" <rekent@ontologos.org>]

All,

In the document [Appendix to Classification Metatheory] attached to the
message [http://grouper.ieee.org/groups/ltsc/logs/ontology/msg00469.html]
there is an type error in the socalled core axiom, which asserts "Relative
instantiation-predication represented by '|=' is compatible with the
absolute KIF instantiation-predication.", and is formalized by the KIF
sentence

(forall (?c ?i ?t)
    (and (=> (|= ?c ?i ?t) (?t ?i))
         (=> (not (|= ?c ?i ?t)) (not (?t ?i)))))

In the relative instantiation-predication notation

(|= ?c ?i ?t)

the variables '?c', '?i' and '?t' have the types 'Classification',
'Instance' and 'Type', respectively.

However, in the universal (absolute), and basic KIF,
instantiation-predication notation

(?t ?i)

the variables '?t' and '?i' should have the types 'UnaryRelation' and
'Object', respectively, where the latter denotes the universal type of all
KIF objects.
__________

So two things need to be done here.

First, we need to define a *Bootstrap Ontology*, which will mesh the needs
of the Classification Ontology (and other Information Flow metatheories in
the future) with KIF. Note that this Bootstrap Ontology is NOT the
Structural Ontology, which is being replaced and augmented by a collection
of metatheories that allow one to build ontologies in a principled fashion
from basic ontologies with constructor operations.

Second, we need to correct the core axiom error mentioned above.
__________

The Bootstrap Ontology needs (at least for now) the following categories of
things:

Object -- the universal type
Relation -- the sum of all relation types
UnaryRelation
BinaryRelation
TernaryRelation
Function -- the sum of all function types
UnaryFunction
BinaryFunction

I will assume the following partitions:

Object = Relation + Function + ...
Relation = UnaryRelation + BinaryRelation + TernaryRelation + ...
Function = UnaryFunction + BinaryFunction + ...
__________

The core axiom error is fixed as follows.

Define a binary KIF function 'int' that denotes the intent of an instance
'i' in a classification 'c' defined by
    int(i) = {t in typ(c) | i |= t}.

(BinaryFunction int)
(forall (?c ?i ?p)
    (=> (= (int ?c ?i) ?p)
        (and (Classification ?c) (inst ?c ?i) (UnaryRelation ?p))))
(forall (?c ?i ?t)
    (=> (and (Classification ?c) (Instance ?i) (Type ?t))
        (<=> (int(?c ?i) ?t) (|= ?c ?i ?t))))

Dually, define a binary KIF function 'ext' that denotes the extent of a type
't' in a classification 'c' defined by
    ext(t) = {i in inst(c) | i |= t}.

(BinaryFunction ext) ;; we need to change to name of the extensibility
predicate
(forall (?c ?i ?p)
    (=> (= (ext ?c ?t) ?p)
        (and (Classification ?c) (typ ?c ?t) (UnaryRelation ?p))))
(forall (?c ?i ?t)
    (=> (and (Classification ?c) (Instance ?i) (Type ?t))
        (<=> (ext(?c ?t) ?i) (|= ?c ?i ?t))))

Finally, using the KIF predicate 'ext', the core axiom now becomes the KIF
sentence

(forall (?c ?i ?t)
    (and (=> (|= ?c ?i ?t) (ext(?c ?t) ?i))
         (=> (not (|= ?c ?i ?t)) (not (ext(?c ?t) ?i)))))

But this is redundant by the third axiom above for the KIF predicate 'ext'.
So toss it out.

Robert E. Kent
rekent@ontologos.org