ONT Re: Higher Order Categorical Logic -- Discussion
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
HOC. Discussion Note 9
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
JA = Jon Awbrey
L&S = Lambek & Scott
MA = Murray Altheim
L&S: | Example C3. The category of 'preordered sets'.
| Its objects are preordered sets, that is, sets
| with a transitive and reflexive relation on them,
| and its morphisms are monotone mappings, that is,
| mappings which preserve this relation.
JA: Say that (D, -<) is a reflexive and transitive order relation on D.
Say that (E, =<) is a reflexive and transitive order relation on E.
JA: A "monotone" (order-preserving) mapping f : D -> E is one such that:
MA: Damn, the choices of words are so
strange. "Monotone" to me has to
do with frequencies of sound.
The ties that bind our Fab Four -- Arithmetic, Geometry, Music, Physics --
into such a tight band go way way back, but hear the musician in them
borrows if not quiet covers the tune of a physical tension, to wit,
the stretch of a singular cord across the redounding monochord,
and though we might vie to re-dub our monotonous theme with
a monoscalar variation, we'd still have to face the music.
JA: x -< y implies f(x) =< f(y),
JA: Again, we can think of f as describing or establishing an analogy or
a metaphor between the ordering (-<) on D and the ordering (=<) on E.
MA: "Analogy" and "metaphor"? Simile? Synonym? I suppose any field
borrows terms from other fields, but the cognitive dissonance
for outsiders is pretty high, sorta like learning Bulgarian.
No, actually, like learning Dutch.
No, and I'm guessing that it's probably become more obvious by now,
the use of the term "analogy" -- what Aristotle called "paradigm",
that's Greek for "side-show" -- is quite precise in describing
a correspondence of formal structure between two domains. But
we'll be seeing lots more examples of that before we're done.
JA: Category theory is really just a study in metaphors.
And, well, metaphors between metaphors (= functors).
And, well, metaphors between functors (= nat.trans).
In one of my first courses in this stuff we got to
do a "creative" final paper, and I wrote an intro
to the main ideas in the form of a science fiction
story. Probably still have it buried in a basement
box somewhere, but don't know if I could find it now.
Incidentally, there's lots of formal recognition of this theme
in the AI literature. A couple of examples that come to mind
would be the joint work of Holland, Holyoak, Nisbett, Thagard
on induction and related inference processes, and also the work
of Forbus, Gentner, Stevens, et al. on analogy and mental models.
MA: And I must say that while the symbols in the book
are difficult, their transformations into ASCII
make it quite a bit harder to deal with.
JA: You get used to it. And it's quick.
MA: I'm guessing you have *somewhere* provided that ASCII mapping.
It helps that I've got Lambek and Scott in front of me, as this
is one of the first times I've seen the equivalents of your ASCII
given full font and glyph printing. Like $A$, I would never have
guessed what it looked like. I can't imagine what some of those
squiggles look like in ASCII.
At the time, I was using bang-bars like !a! for Greek characters
and scrip-bars like $A$ for script (or Fraktur or Gothic) letters.
But these days I try to get by with one level of fanciness, using
bang-bars for both Greek and script, and leaving the resolution of
character to the developing context and the discerning reader's eye.
Most of the other mark-up is pretty standard: carets to mark superscripts,
like X^3, underscores to mark subscripts, like x_2, single quotes to mark
italics, like 'this'. The isomorphism symbol I transcribe like so, ~=~,
otherwise there's a risk that readers would read "~=" as "not equal".
Plus, no sense trying to be too pretty, as it's obviously a book
that everybody will want to buy sooner or later, anyway.
Jon Awbrey
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
http://www.cs.bsu.edu/homepages/mighty/history.html
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o