Re: SUO: Vote 2001-02: IFF Foundation Ontology
John,
I more or less agree with you (see comments below).
> I am sympathetic to the use of category theory as a framework for
> supporting the multiple mappings between various theories in the
> infinite lattice. However, I agree with you that the terminology
> of category theory is unfamiliar even to most mathematicians and
> logicians, and it generally strikes terror in the hearts of everyone
> else.
See the brief technical discussion below on truth concept lattices (the
"infinite lattice") and 1st-order interpretations (the "multiple mappings
between various theories").
> I believe that the appropriate place for category theory is under
> the rug where no one will ever see it.
The "no one" here is too strong.
In the programming language analogy that I made in the document
[http://suo.ieee.org/Kent-IFF.pdf], users of software applications should
not
see the source code, but the programmers of those applications need to have
it visible in front of them. In the IFF approach certain people working in
certain roles will need to see and use the IFF Category Theory Ontology,
whereas others will want it to be invisible. See the further comments below
on role types and visibility.
> It would be useful to have
> a white paper that shows how all the mappings from theory to theory
> can be untangled in category land, but then present the results
> without using any of the terminology of category theory.
Thanks for the suggestion. I volunteer to help write such a white paper. See
further comments below on the truth concept lattices and maps between them.
> No one
> who uses the ontology (even with the lattice of theories is shown
> right up front) should ever see any of the terminology or machinery
> of category theory.
I agree. Note the word "uses". See further comments below on role types and
visibility.
____________________________________________________________
____________________________________________________________
I. Discussion of role types and visibility of IFF terminology and
axiomatizations:
As I mention in a previous message
[http://suo.ieee.org/email/msg05907.html], the IFF is partitioned into three
levels (object level, lower metalevel, upper metalevel), and the visibility
of these levels depends upon the role that people play with respect to the
IFF:
__________
There were comments and concerns at the SUO workshop about intimidating
users with category theory terminology. But as I commented at the workshop,
and have repeated above, the terminology visible to the user is that
introduced in the domain ontologies, and the foundation terminology visible
to the content ontology developer is that terminology introduced in the
lower metalevel -- terms such as 'subtype', 'expression', 'model',
'1st-order interpretation', etc. This is normal semantic terminology, but
not category theory terminology. The category terminology is introduced in
the upper metalevel, and this is seen only by the lower metalevel. Compare
the dependencies in Figure 1 "IFF Foundation Ontology (with dependencies)"
of the document [http://suo.ieee.org/Kent-IFF.pdf].
__________
Here I expand on that discussion of role types and ontological visibility.
There are two distinctions concerned:
A. designer versus user
B. 3 levels of terminology:
object level, lower metalevel, upper metalevel
Note: a designer must do some reasoning about the module being developed.
These two distinctions are combined into six possible role types, of which
we identify two pairs, ending up with four possible distinct role types. The
first two role types do not want to see category theory terminology -- they
want it swept under the rug. However, the second two role types need to
use category theory terminology.
1. object level user
A person in this role (with respect to the IFF) sees only object level
terminology, that is, they see only domain/middle/upper ontology
terminology.
Example terminology:
a. From a Movie domain ontology:
'movie', 'actor', 'rating' ...
b. From an upper object level ontology
'3D', '4D', 'object', 'event', 'continuant', 'occurrent', ...
2. object level module designer = lower metalevel user
A person in this role (with respect to the IFF) sees both object level and
lower metalevel (model theory) terminology.
Example terminology:
a. From the IFF Model Theory Ontology:
'instance', 'type', 'classification', 'expression', 'arity', 'sentence',
'language', 'model', 'satisfies', '1st-order interpretation' ...
===========================================
visibility boundary for category theory terminology (John's "rug")
===========================================
3. metalevel module designer = upper metalevel user
A person in this role (with respect to the IFF) sees both lower metalevel
(model theory) and upper metalevel (core and category theory) terminology.
Example terminology:
a. From the IFF Model Theory Ontology:
'instance', 'type', 'classification', 'expression', 'arity', 'sentence',
'language', 'model', 'satisfies', '1st-order interpretation' ...
b. From the IFF Core Ontology:
'class', 'function', 'relation', 'complete-lattice', 'concept-lattice', ...
c. From the IFF Category Theory Ontology:
'category', 'functor', 'pullback', 'colimit', 'monad', ...
4. upper metalevel designer
(myself, as designer of the IFF upper metalevel, and other
category-theorists that might help in the future)
A person in this role (with respect to the IFF) sees only the upper
metalevel (core and category theory) terminology.
Example terminology:
a. From the IFF Core Ontology:
'class', 'function', 'relation', 'complete-lattice', 'concept-lattice', ...
b. From the IFF Category Theory Ontology:
'category', 'functor', 'pullback', 'colimit', 'monad', ...
____________________________________________________________
____________________________________________________________
II. Discussion of truth concept lattices and 1st-order interpretations
(somewhat technical!).
The *truth classification* was discussed as example 4.6 on page 71 of the
book "Information Flow: The Logic of Distributed Systems" by Jon Barwise and
Jerry Seligman. I have introduced its concept lattice which I call the
*truth concept lattice*, and illustrated this on slides 5 and 6 of my SUO
Workshop PowerPoint presentation
[http://reliant.teknowledge.com/IJCAI01/Kent.ppt]. The truth classification
and truth concept lattice occur as examples within the IFF Core
(sub)Ontology of version 2.0 of the IFF Foundation Ontology (to be submitted
to SUO next month). Amongst other things, the axiomatization of large
concept lattices in version 2.0 answers Chris Menzel's foundational concerns
about a "reasonable class theory" mentioned in the message
[http://grouper.ieee.org/groups/suo/email/msg01759.html].
The first thing to note is that we are dealing with a fibered structure
here. I have proposed that the truth concept lattice be used in SUO as John
Sowa's potentially infinite open-ended lattice of theories. However, there
is no single lattice here but an infinite collection of lattices, where each
truth classification "truth-classification(L)" and each truth concept
lattice "truth-lattice(L)" is based upon (indexed by) a particular 1st-order
language L. So a particular object level ontology -- be it a domain
ontology, a middle level ontology, or an upper level ontology -- will be an
element of a lattice based on its 1st-order language. Internally, the
various ontologies (theories) are connected by generalization/specialization
and sideways jumping. Externally, the lattices in the IFF framework are
connected in many different ways, such as by the FCA notions of apposition
and subposition, etc. But a very special and especially interesting
connection is through 1st-order interpretations.
The notion of a *1st-order interpretation* was discussed as example 4.11 on
page 74 of the book by Jon Barwise and Jerry Seligman [op. cit.]. 1st-order
interpretations are axiomatized in the IFF Model Theory Ontology module of
the IFF Foundation Ontology (to be submitted to SUO sometime later this
fall). A 1st-order interpretation I : L1 -> L2 from one 1st-order language
L1 to a second 1st-order language L2 maps the relations of L1 to the
formulas of L2. For us here, there are two relevant passages:
1st order interpretation
|=> infomorphism between truth classifications
|=> adjoint pair between truth concept lattices
Each 1st-order interpretation
I : L1 -> L2
defines a "truth infomorphism" between the associated truth classifications,
truth-classification(I) : truth-classification(L1) ->
truth-classification(L2)
(see Barwise and Seligman [op. cit.]). And this infomorphism defines an
"truth adjoint-pair" (of monotonic functions) between the associated
truth concept lattices,
truth-adjoint-pair(I) : truth-lattice(L1) -> truth-lattice(L2)
(axiomatized in the IFF Model Theory Ontology). Now, these monotonic
functions map between formal truth concepts (that is, ontologies) in a very
semantic way.
____________________________________________________________
____________________________________________________________
Robert E. Kent
rekent@ontologos.org