SUO: inferencing relevance of the IFF (was: Re: Re: SUMO motion, and merging)
John, Adam and others,
On behalf of the IFF developers, here is a reply to the request for IFF
inferencing relevance.
Robert E. Kent
rekent@ontologos.org
----- Original Message -----
From: "John F. Sowa" <sowa@bestweb.net>
To: "Adam Pease" <apease@ks.teknowledge.com>
Cc: <standard-upper-ontology@ieee.org>
Sent: Monday, April 21, 2003 10:02 AM
Subject: SUO: Re: SUMO motion, and merging
[snip]
> I extracted the following two conditions from your
> note, which I agree with and which I believe should
> be addressed in the joint motion:
>
> > Without at least one formal proof of IFF supporting
> > a useful inference, I don't see the value in its inclusion.
>
> > Without the rules being released for Cyc and language
> > definition addressed, I don't think it's a suitable proposal
> > for SUO, nor would it add value to SUMO.
>
> I would ask the IFF and OpenCyc developers to comment on
> these two points and to suggest ways in which they can be
> addressed in the joint proposal.
The IFF is a framework for object-level ontologies. In this sense it is
content-free. Hence, the "useful inference" that you request support for
cannot be directly about any content of the kind that SUMO or CYC provides.
In fact, IFF complements SUMO in this regard, with IFF supporting inferences
in Category Theory (CT), Formal Concept Analysis (FCA), and Information Flow
(IF) that can be used to apply to _any_ content, for example, the kind that
SUMO or CYC supplies.
The IFF (with possibly extensions to its base-line axiomatisations) can
support inferences for the usual theorems in the theories of CT,
FCA and IF. These could be simple, such as the CT theorems that "all limits
for a diagram are isomorphic" and "the power set and inverse image function
form a functor on sets and functions" or more complex and interesting
theorems, such as the FCA basic theorem characterizing concept lattices.
The basic theorem of the FCA is provable in the IFF in its full
category-theoretic generality as a category equivalence between the category
of classifications and the category of concept lattices.
Some of these theorems are only indirectly relevant to the lattice of
theories application of the IFF, and some are quite relevant. And the
relevancy may not be apparent at first.
For one example, one simple but important theorem for moving between concept
lattices is the theorem that "the composition of infomorphisms is
well-defined; that is, the composition of infomorphisms satisfies the
fundamental property (of an infomorphism)". Why is this important to the
lattice of theories? The answer is that the lattice of theories is
parametric in the sense that there is a lattice of theories for every first
order language, and the natural way to connect these various lattices of
theories together is via concept lattice morphisms defined from language
morphisms between the base languages. This is just one example -- there are
many others.
For another example, the basic theorem FCA is very important in the
transformation on objects from the truth classification over a 1st order
language to the truth concept lattice of theories over the 1st order
language, and on morphisms from the truth infomorphisms over a 1st order
language morphism (or more generally, a 1st order interpretation) to the
truth concept lattice of theories morphisms over a 1st order language
morphism (or 1st order interpretation).
So, in summary, the kinds of inferences supported by the IFF do not deal
directly with the kind of content provided by SUMO or CYC, but rather with
the framework itself that provides for systematic metalevel techniques for
manipulation of an open-ended number of different theories ("moving from one
theory to another theory, and for mixing, matching, combining, and
transforming theories to whatever form is appropriate for whatever problem
anyone is trying to solve") within a lattice of theories, or more generally
within the category of theories.