Re: SUO: RE: Criteria that an ontology must satisfy

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

John, Chris M, Pat, et al,

----- Original Message -----
From: "John F. Sowa" <sowa@bestweb.net>
To: "Jay Halcomb" <jhalcomb@teknowledge.com>;
<standard-upper-ontology@IEEE.ORG>
Sent: Friday, March 09, 2001 11:49 AM
Subject: Re: SUO: RE: Criteria that an ontology must satisfy


> The language of core KIF is pure first-order.  But we have been
> talking about extending KIF to a sorted language, which can be
> used as a metalanguage for arbitrary many metalevels.  A sorted
> first-order language can indeed support true HOL, if you allow
> sorts that have uncountably many members.

I have been meaning to comment about the sorted extension to KIF for some
time. John's comment gives me a little push to do so.

I had thought previously (see message
[http://suo.ieee.org/ontology/msg00983.html]) that I needed a sorted
extension of KIF for the Information Flow Framework (IFF) metalevel. But
now, with the IFF Foundation Ontology, it seems that I do not need this.
What I really need is semantic type restrictions, and these have been
provided in the IFF Foundation Ontology
[http://www.ontologos.org/IFF/Metalevel/Metalevel.html].

To show a picture of both before and after, consider the KIF example for the
"source" operator for category theory that was used in the message
[http://suo.ieee.org/ontology/msg00983.html]. The goal is to define the
"source" or "domain" of a morphism in a category.
__________

Previously I had defined 'source' to be a unary KIF function

1.    (KIF$UnaryFunction source)

that maps a category '?c' to a unary KIF function '(source ?c)'.

2.    (forall (?c ?s)
          (=> (= (source ?c) ?s)
              (and (Category ?c) (KIF$UnaryFunction ?s))))

Here 'Category' was a previously defined KIF class (I was using 'Class' as a
synonym for 'UnaryRelation').

The KIF function '(source ?c)' should only be applied to morphisms of the
category '?c' and should only return objects of the category '?c'.

3.    (forall (?c ?m ?o)
          (=> (= ((source ?c) ?m) ?o)
              (and ((morphism ?c) ?m) ((object ?c) ?o))))

Here '(morphism ?c)' and '(object ?c)' were a previously defined KIF
classes.
__________

Now I still define 'source' to be a unary KIF function

1*.     (KIF$UnaryFunction source)

but this maps a category '?c' to an IFF function '(source ?c)'.

This 'source' is a unary KIF function, since it takes a category as a
parameter -- the term '(source ?r)' is the actual IFF function that
represents the "source" operator inside of a category. This parametric
technique is used throughout the KIF formulation of IFF. An IFF function is
the notion of function defined in the IFF Foundation Ontology
[http://www.ontologos.org/IFF/Metalevel/Metalevel.html]. The string 'IFF' is
the namespace prefix for this foundation ontology.

2*.    (forall (?c ?f)
            (=> (= (source ?c) ?f)
                (and (Category ?c) (IFF$Function ?f))))

Here 'Category' is the IFF conglomerate previously defined as

        (IFF$Conglomerate Category)

An IFF class is the set-theoretic notion of class defined in the IFF
Foundation Ontology. This is not the same as a KIF 'UnaryRelation'. However,
in the IFF Foundation Ontology there are mechanisms for mapping from the
foundation ontology to KIF. An IFF conglomerate is larger set-theoretically.
The IFF Foundation Ontology uses the three-level set-theoretic hierarchy of
sets - classes - conglomerates, from smallest to largest -- but only needs
to axiomatize the first two.  For example, the collection of all sets is a
class, and the collection of all classes and the collection of all
categories are conglomerates. At the conglomerate level, I use KIF functions
and relations. However, the levels of classes and sets are axiomatized and
more abstract. For more on this, see the first footnote in the PDF document
for the IFF Foundation Ontology
[http://www.ontologos.org/IFF/Metalevel/Metalevel.html].

Now the IFF function '(source ?c)' should only be applied to morphisms of
the category '?c' and should only return objects of the category '?c'. These
type constraints are declared by using the IFF 'source' and IFF 'target' KIF
functions in the IFF Foundation Ontology.

3*.    (forall (?c)
            (=> (Category ?c)
                (and (= (IFF$source (source ?c)) (Morphism ?c))
                        (= (IFF$target (source ?c)) (Object ?c)))))

Here '(Morphism ?c)' and '(Object ?c)' are IFF classes previously defined as

4*. (KIF$UnaryFunction Object)

      (forall (?c ?p)
        (=> (= (Object ?c) ?p)
            (and (Category ?c) (IFF$Class ?p))))

     (KIF$UnaryFunction Morphism)

     (forall (?c ?p)
         (=> (= (Morphism ?c) ?p)
            (and (Category ?c) (IFF$Class ?p))))

Bottom line: in IFF I do not need a sorted extension of KIF for this kind of
type restriction.

BTW, the IFF Foundation Ontology now goes beyond the approach to foundations
outlined in chapter 2 of the book "Abstract and Concrete Categories (1990)"
by Jirí Adámek, Horst Herrlich and George E. Strecker. It seems natural that
this ontology should contain axioms for an topos. However, the architecture
for this is somewhat split -- at the level of classes I have only
Cartesian-closure; however, at the level of sets I have the remaining topos
axioms.

Robert E. Kent
rekent@ontologos.org