SUO: Re: Building the Hierarchy
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
Robert,
This problem is as old as Solomon -- no the other Solomon --
you see, there was this one baby, and then there were these
two mothers laying claim to it. Now if there were twins,
or if a half a baby were better than none, then maybe the
problem would have been easier, but no. So we can split
signs and even whole frames of reference as much as we
like, but we can't split objects, as every good-enough
analyst will tell you, without a certain pathology
that no x-pathology will resolve. So I think that
this issue must take some brand of amalgamation or
fiber product to do it up right, like they use in
manifold theory, which I am trying to refresh my
memory and upgrade my knowledge base about,
for example:
DARM. Differential And Riemannian Manifolds -- Ontology List
01. http://suo.ieee.org/ontology/msg04770.html
02. http://suo.ieee.org/ontology/msg04771.html
03. http://suo.ieee.org/ontology/msg04772.html
04. http://suo.ieee.org/ontology/msg04773.html
05. http://suo.ieee.org/ontology/msg04774.html
06. http://suo.ieee.org/ontology/msg04775.html
07. http://suo.ieee.org/ontology/msg04776.html
08. http://suo.ieee.org/ontology/msg04777.html
09. http://suo.ieee.org/ontology/msg04778.html
10. http://suo.ieee.org/ontology/msg04779.html
11. http://suo.ieee.org/ontology/msg04780.html
12. http://suo.ieee.org/ontology/msg04781.html
13. http://suo.ieee.org/ontology/msg04783.html
14. http://suo.ieee.org/ontology/msg04784.html
15. http://suo.ieee.org/ontology/msg04785.html
16. http://suo.ieee.org/ontology/msg04786.html
17. http://suo.ieee.org/ontology/msg04787.html
18. http://suo.ieee.org/ontology/msg04788.html
DARM. Differential And Riemannian Manifolds -- Commentary Notes
01. http://suo.ieee.org/ontology/msg04782.html
On second thought, maybe this covered by
a general enough notion of quotients ...
Jon
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
Robert E. Kent wrote:
>
> 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
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o