FOM: extent of agreement with Simpson

[Vaughan R. Pratt]

>From: cxm7 at po.cwru.edu (Colin McLarty)
>Here I agree with Steve in good part--except that you can't ask
>every poster to start from 0 and build every subject they refer to. You have
>to let the list find its level through some give and take.

I fully agree with Colin.  On the one hand there's a mix of cultures on
this list that seems well worth encouraging by having them explain each
other's viewpoints.  On the other there are some pretty wide gaps
between some of those cultures (a big one between set theory and
category theory for example), and blithely asking each contributor to
first bring the other cultures up to speed in his or her area before
saying anything is tantamount to asking them to give an introductory
course in their subject.  Explaining monads to experts on tame
congruence theory or vice versa can take a long time and still only
scratches the surface.

Regarding Harvey's and Steve's insistence that foundations doesn't need
linear logic, bear in mind that for the past century or so logic and
algebra have been evolving along parallel but only loosely connected
paths.

Algebraic logic got off to a good start with Boole, Peirce, and
Schroeder in the latter half of last century, but did not hit its
stride until Birkhoff's 1933 HSP theorem, setting the tone for model
theory.  What model theory does is to reveal algebra as a reflection of
logic, with logic ostensibly residing inside a single structure and
algebra reifying the intrinsic incompleteness of logic by working
outside with multiple structures, transforming and combining them.

Categorical or transformational logic, the subject of the Lambek-Scott
book (Phil Scott, not Dana), takes the algebra-logic connection to a
new level by casting such algebraic concepts as homomorphism,
subalgebra, and direct product as logical concepts with their own rules
of inference.  As such, transformational logic is an
outside-the-structure logic, dual to first order logic's
inside-the-structure viewpoint.  (This is what the Curry-Howard
correspondence between algebra and logic is about, under the slogan
"propositions and types.")  What makes this outside logic look even
remotely like inside logic is a crucial naturality condition
characterizing those few transformations that are "logical," without
which there would be chaotically many transformations and no
recognizable logic thereof.

The transformational logic treated by Lambek and Scott confines itself
to cartesian closed universes, such as sets, posets, and DCPO's.
Beyond these few universes, some of the axioms and rules of that
particular transformational logic start to break down.  Linear logic
consists of those laws of transformational logic that work in *all*
mathematical universes.  Some undersize universes may need to be
completed to a larger universe in order for LL's connectives to be well
defined, but there are theorems guaranteeing the existence of such
completions (not necessarily canonical) for essentially all of what
passes today for mathematical universes.

I promise I won't say any more on linear logic unless people are
interested.  There's only so much one can say by way of motivation
before people go "meta" and start needing to be motivated to listen to
the motivation.

Vaughan