Higher Order Categorical Logic -- Discussion

o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o

HOC.  Discussion Note 1

o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o

MA  = Murray Altheim
L&S = Lambek & Scott

MA: You recommended I read Lambek and Scott's "Introduction to
    Higher Order Categorical Logic", so I ordered a copy from
    Cambridge University Press.  It came over the holidays.
    I suppose I should have heeded the series title:
    "Cambridge Studies in *Advanced* Mathematics",
    because I feel completely stupid.  I can't claim
    to understand more than the first page or two,
    which I wouldn't want to be quizzed on either.
    The stuff I can understand leads me to believe
    it's very interesting domain, but it also makes
    me think that  sometimes I'm just not cut out
    for certain types of thinking, or have received
    literally no training necessary to grok this:

L&S: | Let [squiggle] be the category of Abelian groups and [another_squiggle]
     | the opposite of the category of topological Abelian groups.  Let K be the
     | compact group of the reals modulo the integers: K [equal sign with three
     | lines] ['R' in an outline font]/['Z' in an outline font].  For any abstract
     | Abelian group A, define F(A) as the group of all homomorphisms of A into K,
     | with the topology induced by K.  For any topological Abelian group B, define
     | U(B) as the group of all continuous homomorphisms of B into K.  Then U and F
     | can easily (!!!) be seen to be the object parts of a pair of adjoint functors.
     | Here [squirrelly-A sub 0] is [squirrely-A], while [squirrelly-B sub 0] is the
     | opposite of the category of compact Abelian groups.  The 'unity of opposites'
     | asserts the well-known (!!!) Pontrjagin (no, I did not misspell that) duality
     | between abstract and compact Abelian groups.  The last statement of Proposition
     | 4.2 tells us that the compact Abelian groups form a reflective subcategory of
     | the category of all topological Abelian groups.

MA: This is on page 18.  By page 137 it's pretty much all formulae composed
    of symbols I've never even seen before. *sigh*   This is pretty much
    completely opaque to me, and I can't imagine being able to spend
    the time in the next five years to understand it well enough
    to make any use of it.

Murray,

I am copying Jack Park because we were just talking about this very issue.

Actually, if could you get as far as understanding the definition
of a natural transformation on page 8, that would be a lot.  But
there's no reason to expect that you could do that on your own.
I spent a lot of time on the SUO list trying to get across basic
category-theoretic ways of thinking in concrete contexts without
ever mentioning the legion of officious titles, ideas which folks
would need to grasp before they could understand 1/10 of what RK
is talking about, but they seem to prefer the razzle-dazzle to
the nitty-gritty.

What you ran into is the sort of place where the authors try
to impress people who have had a couple of years of graduate
courses in algebra and topology with the fact that they can
sum up those two years of study in a single paragraph.  But
that is just a side-show bit, and you can ignore all of it.
In my notes to the Ontology List I skipped from page 11 to
page 41 just by way of getting to the logical motivations
a little quicker.

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.

The stuff that I append here could provide us with a good couple
of months of study, but then you'd have the most essential bits.

Jon Awbrey

[HOC.  Higher Order Categorical Logic.  Notes 01-07]

HOC.  Higher Order Categorical Logic

Part 0.  Introduction to Category Theory

1.  Categories and Functors

01.  http://suo.ieee.org/ontology/msg03373.html
02.  http://suo.ieee.org/ontology/msg03375.html
03.  http://suo.ieee.org/ontology/msg03376.html
04.  http://suo.ieee.org/ontology/msg03377.html
05.  http://suo.ieee.org/ontology/msg03378.html
06.  http://suo.ieee.org/ontology/msg03381.html

2.  Natural Transformations

07.  http://suo.ieee.org/ontology/msg03383.html
08.  http://suo.ieee.org/ontology/msg03384.html
09.  http://suo.ieee.org/ontology/msg03392.html
10.  http://suo.ieee.org/ontology/msg03393.html
11.  http://suo.ieee.org/ontology/msg03394.html
12.  http://suo.ieee.org/ontology/msg03395.html

Part 1.  Cartesian Closed Categories & Lambda Calculus

Introduction to Part 1

13.  http://suo.ieee.org/ontology/msg03396.html

Historical Perspective on Part 1

14.  http://suo.ieee.org/ontology/msg03398.html
15.  http://suo.ieee.org/ontology/msg03399.html
16.  http://suo.ieee.org/ontology/msg03400.html
17.  http://suo.ieee.org/ontology/msg03401.html
18.  http://suo.ieee.org/ontology/msg03402.html

1.  Propositional Calculus as a Deductive System

19.  http://suo.ieee.org/ontology/msg03403.html
20.  http://suo.ieee.org/ontology/msg03404.html
21.  http://suo.ieee.org/ontology/msg03405.html
22.  http://suo.ieee.org/ontology/msg03406.html

2.  The Deduction Theorem

23.  http://suo.ieee.org/ontology/msg03409.html

3.  Cartesian Closed Categories Equationally Presented

24.  http://suo.ieee.org/ontology/msg03410.html
25.  http://suo.ieee.org/ontology/msg03411.html
26.  http://suo.ieee.org/ontology/msg03412.html

Back to Part 0

3.  Adjoint Functors

27.  http://suo.ieee.org/ontology/msg03415.html
28.  http://suo.ieee.org/ontology/msg03416.html
29.  http://suo.ieee.org/ontology/msg03417.html
30.  http://suo.ieee.org/ontology/msg03418.html

The above material is excerpted from:

| Lambek, J. & Scott, P.J.,
|'Introduction To Higher Order Categorical Logic',
| Cambridge University Press, Cambridge, UK, 1986.
|
| http://uk.cambridge.org/mathematics/catalogue/0521356539/

o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
http://www.cs.bsu.edu/homepages/mighty/history.html
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o