SUO: Re: IFF LOT Glossary
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
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