SUO: Re: IFF LOT Glossary
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
Robert,
The rest of this may be a little slower going for me.
I will need to check and see if we are using certain
words the same way.
RK: 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".
>
JA: Yes, for a small example, let's say we have the following function f : A -> B.
>
> 0 1 2 3 4 5 6 7 8 9
> o o o o o o o o o o A
> | \ | / \ \ | | \ /
> | \ | / \ \ | | \ /
> | \ | / \ \ | | \ f
> | \ | / \ \ | | / \
> v vvv v vv v v v
> o o o o o o o o o o B
> 0 1 2 3 4 5 6 7 8 9
>
> I am used to saying that the inverse relation of f evaluated at b in B,
> brutally asciified as (f^(-1))(b), is the "fiber of f at b", so that's
> familiar enough, "up to idiom-morphisms". Gloss fib(f)(b) as f^(-1)(b).
>
> So fib(f) = f^(-1) is the 2-adic relation that is inverse or converse to f.
> Well, not exactly, but via the obvious isomorphism, f^(-1) c B x A being
> the "same information" as fib(f) : B -> Pow(A). Reading f backupwards:
>
> 0 1 2 3 4 5 6 7 8 9
> o o o o o o o o o o A
> ^ ^ ^ ^ ^ ^ ^ ^ ^ ^
> | \ | / \ \ | | \ /
> | \ | / \ \ | | \ f^(-1)
> | \ | / \ \ | | / \
> | \|/ \ \| | / \
> o o o o o o o o o o B
> 0 1 2 3 4 5 6 7 8 9
>
> This becomes fib(f) : B -> Pow(A), which looks like this:
>
> {0} { } {1,2,3} { } { } {4} {5,6} {7} {9} {8}
> o o o o o o o o o o Pow(A)
> ^ ^ ^ ^ ^ ^ ^ ^ ^ ^
> | | | | | | | | | |
> | | | | | | | | | | fib(f)
> | | | | | | | | | |
> | | | | | | | | | |
> o o o o o o o o o o B
> 0 1 2 3 4 5 6 7 8 9
>
RK: 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.
By "theory" I always understand an arbitrary set of "sentences" in some language L.
By "language" I always understand some L c !A!* for some alphabet !A!, and many
of my applications require me to keep in mind fairly arbitrary formal languages,
not just FOL or even especially intended to be interpreted as logical calculi.
So any theory T c L c !A!* is just another language?
What gives?
Jon
> > 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
> o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o