SUO: Re: IFF LOT Glossary
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
RK: The base functor could also be called the underlying language functor.
JA: 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.
RK: It is exactly a forgetful functor in the same manner.
Check. That's one down.
JA: But now I need to get a bit clearer as to how you see
there being 'the' underlying language of a theory.
JA: First question. Do you really mean any theory,
or just the sort of a theory that constitutes
a "finite axiom set" (FAS)?
RK: I mean a theory as in (page 12 of Chang & Keisler, Model Theory 1977).
Check. That puts us on the same page.
RK: I have made no use (so far!) of finiteness. In fact, I have gone out
of my way to find the exactly correct generality, avoiding finiteness
and natural numbers objects (NNO). Eventually I know that I will need
to have an NNO, but then we become more specific, heading toward a topos.
Okay, sounds good.
Jon Awbrey
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o