SUO: Re: Building the hierarchy
John and others,
This note concerns the IFF approach to building the SUO hierarchy.
SUMS
Distinguishing names as concatenated strings such as "moduleID.localID"
corresponds to the mathematical process of forming the *sum* (disjoint union
or coproduct) of the sets of names in the modules. This is represented by
the process of forming the sum in the IFF category of theories and the
underlying IFF category of type languages. See the coproduct axiomatization
starting on page 64 in the language document
http://suo.ieee.org/IFF/metalevel/lower/namespace/type-language/version20021
205.pdf
See the coproduct axiomatization starting on page 18 in the theory document
http://suo.ieee.org/IFF/metalevel/lower/namespace/theory/version20021205.pdf
QUOTIENTS
The identification of any pair of names, such as the case when "two names
with the same spelling in two modules that had been extracted from some
larger module would have the same intended referents", corresponds to the
mathematical process of forming the *quotient* of the sets of names in the
modules via a suitable *endorelation*. This is represented by the process of
forming the quotient in the IFF category of theories and the underlying IFF
category of type languages. See the endorelation/quotient axiomatization
starting on page 69 in the
language document
http://suo.ieee.org/IFF/metalevel/lower/namespace/type-language/version20021
205.pdf
See the endorelation/quotient axiomatization starting on page 21 in the
theory document
http://suo.ieee.org/IFF/metalevel/lower/namespace/theory/version20021205.pdf
So initially we are not operating in the lattice of theories but in the
"wider" context of the category of theories. Once we have formed the various
sums and quotients, then we can operate in the lattice of theories. This is
because each lattice of theories is based upon an underlying first order
language L.
STRUCTURES
Associated with the SUO hierarchy are actually three constructs.
1. The *truth concept lattice of closed theories*
denoted by "truth-concept-lattice(L)",
2. The *complete pre-lattice of theories*
denoted by "lattice-theories(L)",
which is induced by the truth concept lattice and the closure operator. I
call this a pre-lattice, since its underlying order is not a partial order
but just a preorder: for example, any theory is below or equal to its
closure theory and that closure is less than of equal to it; that is, they
are equivalent elements, but not equal elements.
3. The *hierarchy of modules (theories)*
denoted by "module(L)",
whose elements are a subcollection of the theories of L, and whose links are
true lattice orderings.
TRUTH
The following related discussion concerns the IFF truth axiomatization.
See the truth axiomatization starting on page 86 in the language document
http://suo.ieee.org/IFF/metalevel/lower/namespace/type-language/version20021
205.pdf
See the truth axiomatization starting on page 33 in the theory document
http://suo.ieee.org/IFF/metalevel/lower/namespace/theory/version20021205.pdf
---Discussion---
The IFF is a semantic framework, and so far at least not directly a
proof-theoretic framework. Here we discuss in more detail the lattice of
theories (LOT). This is distinct from, but indirectly related to, the
category of theories (COT).
The lattice of theories is based upon a fixed first order langauge L, and in
most of the discussion below we can ignore the language L since it is fixed
and does not vary. When the language does vary, we are most likely talking
in the context of the category of theories.
In the IFF we use the term "expression" of a first order language where
others use the term "formula". We generalize theories form sentences to
expressions: sentences are quantifier-closed expressions; any expression has
an associated universally-closed sentence; a model satisfies an expression M
|= e iff it satisfies the universal closure; sentences are a special case of
sartisfaction.
Strictly speaking the lattice of theories is not exactly from the truth
concept lattice (TCL). The *truth concept lattice* is a true lattice whose
elements are the _closed_ theories of L, and whose order <=tcl is reverse
subset inclusion:
T1 <=tcl T2 iff T2 is a subset of T1.
The *lattice if theories* is somewhat derivative via the closure operator.
The lattice of theories is a preordered set (antisymmetry does not
necessarily hold) that is "complete" and has a meet dense set of meet
irreducible elements, namely the singleton expressons. The elements of the
lattice of theories are the (not necessarily closed) theories, and the order
is entailment order:
T1 <=lot T2 iff clo(T1) <=tcl clo(T2)
iff clo(T2) is a subset of clo(T1)
iff T1 |- e2 for all expressions e2 in T2
The "top" of the lattice of theories is the empty set of expressions
"nothing"; the "bottom" of the lattice of theories is the full set of
expressions "everything". The "meet" of the lattice of thoeries is the
union; the "join" of the lattice of theories is the intersection.
Two theories are equivalent when each entails the other:
T1 == T2 iff T1 <=lot T2 and T2 <=lot T1.
Clearly, T1 = T2 implies T1 == T2. But T1 == T2 does not necessarily imply
T1 = T2.
The IFF is not a proof-theoretic silver bullet: it does not make it any
easier to compute entailment.
In general, to move upward in the lattice of theories, just delete some
expressions from the starting theory. Trivially, T <=lot T-{e} for any e in
T. However, it is nontrivial to determine whether T == T-{e} or not; that is
whether T |- e or not. Dual comments for moving downward in the lattice of
theories.
A theory T is *inconsistent* when it is equivalent to the set-theoretically
largest theory:
T == everything.
A collection of theories is *mutually inconsistent* when the meet (union) is
inconsistent.
---a few LOT & TCL Operators---
entailment relation
T |-L e
iff any model of theory T is also a model of expression e
closure function
clo(L) : th(L) --> clo-th(L)
maps a theory T to the super-theory of all expressions entailed by T: clo(T)
= {e in expr(L) | T |-L e}
installation function
install(L) : pow(L) --> th(L)
____________________________________
____________________________________
----- Original Message -----
From: "sowa" <sowa@bestweb.net>
To: "Jon Awbrey" <jawbrey@oakland.edu>
Cc: "Adam Pease" <apease@ks.teknowledge.com>; "Robert E. Kent"
<rekent@ontologos.org>; "SUO" <standard-upper-ontology@ieee.org>;
<cg@cs.bestweb.net>; <uah.edu@bestweb.net>
Sent: Friday, May 16, 2003 10:35 AM
Subject: Building the hierarchy
> Jon,
>
> Some strategy for distintuishing the identifiers
> used in different modules and relating them to
> one another is essential. I'm renaming this
> thread "Building the hierarchy" because it
> addresses some important general principles.
>
> The first point to note is that every module in
> the hierarchy should have a unique identifier.
> Therefore, all names could be distinguished by
> a concatenated string such as "moduleID.localId".
>
> Keeping the names distinct is not a problem.
> The real problem is to have a systematic way
> of specifying the conditions for determining
> how and whether identifiers in different
> modules could be assumed to be "the same".
>
> As you noted in your email, one might assume
> that the SUMO names or the OpenCyc names had
> been coordinated with one another so that
> we could assume:
>
> 1. Two names with the same spelling in two
> modules that had been extracted from
> some larger module would have the same
> intended referents.
>
> 2. Two names, even with the same spelling, in
> indepedently developed modules could not be
> assumed to have the same intended referents.
>
> The purpose of the lattice of theories (or at least
> a generalization hierarchy that represents some
> finite excerpt from or some finite step toward
> such a lattice) is to relate the names in
> different modules.
>
> At the start of the joint project, we begin with
> a one-node hierarchy: just the universal theory
> T at the top (the one with no axioms at all).
> Then we would put two big nodes on two separate
> branches under T: for example, OpenCyc on the
> right branch and SUMO on the left branch.
>
> The next step would be to extract smaller modules
> (or microtheories) from the two big theories.
> Each of the smaller modules would be more general
> than the larger module from which it was extracted.
> Therefore, all the SUMO modules would lie on some
> branch between T and SUMO, and all the OpenCyc
> modules would lie on some branch between T and
> OpenCyc. The hierarchy at this step is shown in
> the attached file, which I also put on my web site:
>
> http://www.jfsowa.com/figs/suohier.gif
>
> Following are some general principles, which apply
> to this hierarchy and any others that are organized
> as a generalization-specialization hierarchy:
>
> 1. Every module is consistent with all its
> generalizations (i.e., those that lie on
> any upward path between it and the top).
>
> 2. Every module is consistent with all its
> non-absurd specializations (i.e., those that
> lie on any downward path between it and the
> absurd theory at the bottom).
>
> 3. Any two modules whose only common specialization
> is the absurd theory at the bottom are assumed
> to be inconsistent (unless proven otherwise,
> in which case their merger could be added to
> the hierarchy on a branch below each of them).
>
> 4. Any two modules whose only common generalization
> is the universal (or empty) theory at the top
> are assumed to have nothing in common (unless
> proven otherwise, in which case their common
> generalization could be added to the hierarchy
> on a branch above each of them).
>
> Constructing a hierarchy similar to suohier.gif
> would be fairly straightforward, and even at the
> beginning stage it would be a useful thing to have
>
> Even more useful, however, would be a refinement
> of suohier.gif to find commonalities between SUMO
> and OpenCyc and to find features of each that could
> be used to enrich the other (i.e., to fill in the
> "no man's land" between the two branches).
>
> The purpose of the lattice operators is to provide
> guidelines that show where to look for the
> commonalities and missing information and where
> to put the results when they have been derived.
>
> Bottom line: Building the hierarchy can be done in
> a step-by-step fashion, and even the early stages
> can be useful to the SUMO and OpenCyc developers
> and anyone else who needs ontology building blocks.
>
> John Sowa
>
>