SUO: Re: IFF LOT Glossary
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
Robert E. Kent wrote:
>
> Jon,
>
> The base functor could also be called the underlying language functor.
Okay, that helps a little. So it does begin to sound like a forgetful functor,
for example, the functor ||...|| : Groups -> Sets, G ~> ||G||, that gives you
the underlying set of a group.
But now I need to get a bit clearer as to how you see
there being 'the' underlying language of a theory.
First question. Do you really mean any theory,
or just the sort of a theory that constitutes
a "finite axiom set" (FAS)?
Jon
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
> 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/version20021205.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/version20021205.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
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o