SUO: 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