KIF Re: the Heraclitus distinction metatheory

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

All,

The sorted version of the theory of the Heraclitus distinction may be seen
as a little clearer than the unsorted (one-sorted) version. Here there are
three sorts of things: entities, individuals and classes. Let us denote the
sorts by $ent, $ind and $cls, respectively.

    SUO[$ent] denotes the ENTITY metaclass
    SUO[$ind] denotes the INDIVIDUAL metaclass
    SUO[$cls] denotes the CLASS metaclass

So we do not need the corresponding 1-place metapredicate symbols.

Sequent constraints on sorts are specified as follows.

    [necessity:]   |- $ent
    [subtype:]   $ind |- $ent   and   $cls |- $ent
    [disjointness:]   $ind, $cls |-
    [covering:]   $ent |- $ind, $cls

This automatically induces the required partition

    SUO[*] = SUO[$ent] = SUO[$ind] + SUO[$cls]

Finally, the sort of the INSTANCE-OF metapredicate symbol is specified as
follows.

    sort[INSTANCE-OF] = <$ent, $cls>

This automatically induces the required typing

    SUO[INSTANCE-OF] \subset SUO[$ent] x SUO[$cls]

No axioms are necessary.

Robert E. Kent
rekent@ontologos.org

----- Original Message -----
From: "Robert E. Kent" <rekent@ontologos.org>
To: "SUO-KIF" <suo-kif@ieee.org>; "SUO" <standard-upper-ontology@ieee.org>
Sent: Tuesday, December 05, 2000 4:12 PM
Subject: SUO: the Heraclitus distinction metatheory


> All,
>
> Attached is the SUO-KIF metatheory of the Heraclitus distinction conceived
> as a formal context.
>
> Robert E. Kent
> rekent@ontologos.org
>