Jon,
Recall that for any function
f : A --> B
from set A to set B, there is a function
fib(f) : B --> pow(A)
called the "fiber of f" which given any element b in B returns the subset
fib(f) = {a in A | f(a) = b}
of all elements of A that map to b. Here, fib(f)(b) is called "the f-fiber
over b".
We extend this terminology to categories in place of sets and functors in
place of functions. There is a functor
base : Theory --> Language
from the category of theories to the category of languages.
Consider the object function
obj(base) : obj(Language) --> obj(Theory)
of the base functor. Given any theory, this returns the underlying base FOL
language consisting of the sets of relation, function and sort symbols used
in the axioms and relational arities of the theory. The "base language
fiber" refers to the "fiber of obj(base)"; that is, to the fiber of the
function fib(obj(base)). For any language L in obj(Language), this returns
the subclass
fib(obj(base))(L) = {T in obj(Theory) | obj(base)(T) = L}
of all theories of whose underlying base language is L. Here,
fib(obj(base))(L), or fib(base)(L) for short, is called "the base fiber over
L". This is the underlying set of the lattice of theories over L: LOT(L) =
fib(base)(L).
The morphic aspect of the base functor also comes into this picture. First
of all, when the lattice of theories LOT(L) is regarded as part of the
category of theories, there is a morphism g : T1 --> T2 between two theories
in LOT(L) precisely when base(g) L --> L is the identity and T1 >= T2 in the
lattice entailment order (T2 entails any axiom of T1). Secondly, for any
morphism of languages f : L1 --> L2 in the category of languages, there are
direct and inverse image functions
dir(f) : LOT(L1) --> LOT(L2)
inv(f) : LOT(L2) --> LOT(L1)
that are adjoint monotonic functions. These are important for moving
theories around, as the following paragraph indicates.
A *diagram of theories* is the IFF representation for either an "unpopulated
modular object-level ontology" or a "library of modules". Using the base
functor, every diagram of theories T has an underlying base diagram of
languages L = base(T). Take the colimit col(L) of this base diagram. Then
the colimit of the diagram of theories col(T) is the direct image (flow)
dir(inj_n) along the base diagram colimit injections followed by the meet in
LOT(col(L)), the lattice of theories over col(L). Moreover, using the direct
image (flow) dir(inj_n) moves the theories in T to the lattice of theories
LOT(col(L)). Also, recall that we defined the notions of "monocosmic" and
"polycosmic" in terms of the colimit of theories.
Robert E. Kent
rekent@ontologos.org
----- Original Message -----
From: "Jon Awbrey" <jawbrey@oakland.edu>
To: "Robert E. Kent" <rekent@ontologos.org>
Cc: "SUO" <standard-upper-ontology@ieee.org>
Sent: Thursday, June 26, 2003 12:45 PM
Subject: Re: IFF LOT Glossary
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
hi robert,
could you explain what you mean by "base language fiber".
i kind of know what a fiber is in simple situations.
thanks,
jon
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
Robert E. Kent wrote:
All,
I have posted the PDF document "The IFF Glossary for the Lattice of
Theories"
at the address:
http://suo.ieee.org/IFF/LOT-glossary.pdf.
This graphically illustrates and briefly discusses the core
functionality for both the truth concept lattice and the
lattice of theories, two notions that are equivalent
from the order-theoretic viewpoint. The lattice of
theories is the base language fiber in the category
of theories, whereas the truth concept lattice is
the base language fiber in the category of
closed theories.
Please regard this as a mid-range report -- I am
developing a new version of the theory namespace
axiomatization that contains all of this. This
will offer a baseline axiomatization in the IFF
for the notions of a "lattice of theories" and
a "library of modules".
As always, all constructive comments are welcomed.
Robert E. Kent
rekent@ontologos.org
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o