SUO: Re: IFF LOT Glossary
Jon,
The base functor could also be called the underlying language functor.
Just like for CM's description of Enderton's sorted language
http://grouper.ieee.org/groups/suo/email/msg01792.html
an IFF language
http://suo.ieee.org/IFF/metalevel/lower/namespace/type-language/version20021
205.pdf
consists of a set of entity types (sorts) and a set of relation types
(predicate symbols) (I will ignore function symbols for simplicity) with
a reference (sort) function
reference : variable --> entity type
that sorts the variables, and an arity function
arity : relation type --> pow(variable)
and a signature function (equivalent to arity)
sign : relation type --> signature(reference)
that type the arguments for relations.
Example: the usual specification notation
marriage(Person: person1, Person: person2)
declares marriage to be a binary relation between two people. Every IFF
language inductively generates a set of expressions in the usual way.
An IFF theory has two components: an IFF language and a subset of
expressions over that language. The language component is called the *base*
language of the theory. This terminology is actually appropriate, since we
picture the set of theories over a language as a fiber on a stalk over the
base. The notion of base extends to morphisms, and hence forms a functor
from the category of theories to the category of languages. This functor is
a bifibration: over any language morphism there is an (inverse image, direct
image) adjoint pair of monotonic functions between the lattices of theories
over the source and target languages. We can use these monotonic functions
to move theories back and forth. In particular, the direct image can be used
to compute the colimit of a diagram of theories, and (as I explain in
another SUO message today) the adjoint pair define the notion of "mapping
closure" that is of some significance for mapping theories.
Robert E. Kent
rekent@ontologos.org
----- Original Message -----
From: "Jon Awbrey" <jawbrey@att.net>
To: "Robert E. Kent" <rekent@ontologos.org>; "SUO"
<standard-upper-ontology@ieee.org>
Sent: Saturday, July 05, 2003 7:20 AM
Subject: Re: IFF LOT Glossary
> o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
>
> Robert,
>
> Still struggling to get an intuitive grasp of this base functor.
> I am used to base functors that take you back from an extension
> to a base, and thus are written like projections !p! : E -> X.
> Is that the right ballpark? Otherwise, I can only figure that
> it is at bottom some kind of inclusion map or forgetful functor.
>
> Can you tell me in more intuitive terms how you think of this thing,
> and how you see the difference between a Theory and a Language?
> John Sowa assures us that ordinary language is universally
> adequate to every res, and since we are talking post hoc
> here, I would be forced to agree.
>
> Jon
>
> > 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.
> >
> > JA: By "theory" I always understand an arbitrary set
> > of "sentences" in some language L.
> >
> > RK: Yes. Actually, in the IFF for convenience I
> > usually extend this to "expressions" = "formulas".
> >
> > Yes, the first "new math" book I had in high school
> > used the term "open sentence" as its generic notion,
> > and so I hardly ever take "closed" as the default.
> >
> > Starting out in the "less refined" formal language context, which I
always do
> > for the very same reason -- it's one of those heuristic slogans that I
follow:
> > "Polya's Paradoxical Power Principle" (P^4), I think, giving you an
amplified
> > inductive leverage by taking a more general case for the antecedent
condition.
> >
> > JA: 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.
> >
> > JA: So any theory T c L c !A!* is just another language?
> >
> > JA: What gives?
> >
> > RK: Your definition of language is that used for formal languages and
automata.
> > My definition of language is an alternate and extended form of an
FOL
> > language. In short, it is a bit more refined than yours; one could
> > reduce the FOL languages of the IFF to subsets of strings if one
> > saw a need to do so, but quite a lot is lost. Sometimes, you
> > just can't reduce.
> >
> > Okay, I'm not trying to reduce anything, merely striving to relate
things.
> > I am preparing for a happier FOL, but when I do get ready to cast it
into
> > a full computational form, it's going to look a bit different, more like
> > a refit of Peirce's "Logic of Relatives" (1870) than anything you've
> > seen on the market lately. At any rate, any logic formalism is
> > just a formal language with added structure, and you know all
> > the reasons for upbuilding character bit by bit, so I'll just
> > leave it at that. Just for (auto-)tutorial purposes, though,
> > I would like to try devising some simple ZOL examples of the
> > corresponding concepts.
> >
> > RK: Here is the definition given in the language namespace document
> >
> >
http://suo.ieee.org/IFF/metalevel/lower/namespace/type-language/version20021
205.pdf.
> >
> > Yikes, more hwk.
> >
> > I said it'd be slow.
> >
> > Jon
> >
> > o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
> >
> > [keep >>>--->>>]
> >
> > > The IFF FOL languages have several components:
> > > (for simplicity, I give this definition without function symbols)
> > >
> > > Definition:
> > > A first order type *language* L = (refer(L), sign(L)) consists of
> > > - a reference function refer(L)
> > > - a signature function sign(L)
> > > that satisfy the pullback constraint
> > > ** tgt(sign(L)) = sign(refer(L)).
> > >
> > > This seems simple -- just two functions that satisfy some simple
constraint.
> > > The symbol "tgt" in ** refers to the target set of a function between
sets.
> > > For more on the axiomatization of set-theoretic functions between
(small)
> > > sets see the axiomatization for Set the category of sets in the IFF
lower
> > > core (meta) ontology
> > >
http://suo.ieee.org/IFF/metalevel/lower/ontology/core/version20020515.pdf
> > > or in the more (up to date) set namespace document
> > >
http://suo.ieee.org/IFF/metalevel/lower/namespace/set/work-in-progress.pdf.
> > > The symbol "refer" in ** refers to the reference function refer(L).
> > > The first occurrence of the symbol "sign" in ** refers to the
signature
> > > function sign(L). However, the second occurrence of the symbol "sign"
in **
> > > refers to a different signature function on classes (not sets)
axiomatized
> > > starting on page 23 of the IFF lower core (meta) ontology.
> > >
> > > Let us look at the axiomatization
> > > ________________________________________
> > >
> > > (1) (SET$class language)
> > >
> > > (2) (SET.FTN$function reference)
> > > (= (SET.FTN$source reference) language)
> > > (= (SET.FTN$target reference) set.ftn$function)
> > >
> > > (3) (SET.FTN$function signature)
> > > (= (SET.FTN$source signature) language)
> > > (= (SET.FTN$target signature) set.ftn$function)
> > >
> > > (4) (= (SET.FTN$composition [reference set.ftn$signature])
> > > (SET.FTN$composition [signature set.ftn$target]))
> > > ________________________________________
> > >
> > > The first thing to note is that there are no quantifiers and no
logical
> > > connectives used in this axiomatization fragment. Hence, this strictly
> > > abides by the *Categorical Principle* as discussed in the current
> > > introduction to the IFF located at
> > > http://suo.ieee.org/IFF/version/20021205.htm.
> > > Axiom (1) states that the term "language" refers to a set-theoretic
class.
> > > Such classes are axiomatized starting on page 7 in the IFF upper core
(meta)
> > > ontology
> > >
http://suo.ieee.org/IFF/metalevel/upper/ontology/core/version20020102.pdf.
> > > Axioms 2 and 3 specify that the terms "reference" and "signature"
refer to
> > > set-theoretic class functions that take a language as a parameter and
return
> > > set-theoretic functions between (small) sets. Finally, axiom (4)
expresses
> > > the constraint **. Now one might ask in this constraint how do we
> > > distinguish between the occurrences of the various terms? When a term
has no
> > > prefix, it refers to a term in the ambient namespace -- the namespace
that
> > > we are operating in at this point. This rule distinguishes the terms
> > > "signature" and "set.ftn$signature"; the first refers to the signature
> > > function for a language being axiomatized in this ambient namespace,
whereas
> > > the second is axiomatized in some external namespace designated by the
> > > prefix "set.ftn". This is the namespace that starts of page 20 of the
IFF
> > > lower core (meta) ontology
> > >
http://suo.ieee.org/IFF/metalevel/lower/ontology/core/version20020515.pdf.
> > >
> > > Now we have begun to dig into the inner parts of the IFF. Feels good,
eh?
> > >
> > > Robert E. Kent
> > > rekent@ontologos.org
> >
> > o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
> o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
>