FOM: ReplyToPratt

[Vaughan R. Pratt]

Two things.  First, in

 Such a dual point (as a function from
 chain B to 2) when composed with any monotone map f:A->B between two
 chains yields a dual point of  B;
				^

That should have been an A.

Second, I neglected to respond to Harvey's opening point:

>The Brouwer track is well formulated in traditional f.o.m. terms. The
>intuitionistic systems are well formulated and well studied, with
>appropriate striking results of the usual f.o.m. kind. However, LL has not
>had the same attention. You can do us a great service by presenting LL in a
>basic way so that the point of it for foundations of mathematics is made
>crystal clear. How about it?

As promised earlier I will give the details of LL proof theory later on
(at least for the multiplicative fragment, which I know best).  However
I think I can usefully say a little here about Brouwer-Heyting-Girard.

The relationship between Girard and Heyting (as formalizer of Brouwer)
can be understood in terms of the relationship between Heyting and
Boole, in all cases phrased in terms of the structure of the universe
of individuals.

For Boolean logic, individuals form a set.  For intuitionistic logic
they band together as a poset, which might be a set, or a chain, or
anything in between such as the underlying poset of a Boolean algebra.
For linear logic they organize themselves into an arbitrary structure,
which might be a set, or a Boolean algebra (transforming as such, i.e.
not merely its underlying poset), or anything in between such as a
vector space or group or manifold etc.

The slogan of Boolean logic might be, everything is the sum of its
parts.  A poset is not the sum of its parts, you have to specify the
glue as well.  Intuitionistic logic gingerly eases the logician into
the brave new world of sticky universes, with just enough structure to
make things visibly different from Boolean logic but not so much as to
make it bizarrely different.  Not even Brouwer or Heyting imagined
logic changing to something as different as linear logic while still
meaning something.

The logic of sets is Boolean because you can carve up a set with
predicates any way you like, and the result is a Boolean algebra.  With
a poset the rule is that a predicate must be an order filter (aka a
monotone function to the two-element chain), and such predicates while
forming a complete completely distributive lattice (and hence a Heyting
algebra) do not necessarily form a Boolean algebra.  In particular they
need not be complemented in the sense of having for every x an element
y such that x+y=1 and xy=0.

What you do get in a Heyting algebra however is the Galois connection

		ab |- c  iff  a |- b->c

(read |- equivalently as <=, less or equal, if you prefer) defining
intuitionistic implication in terms of conjunction (which in turn is
defined in the usual way for lattices, namely greatest lower bound).

>From this one can define ~a = a->0, which while not a complement
retracts the Heyting algebra H to a sublattice of H that happens to be
a Boolean algebra (or in operational terms, ~ *is* complement for those
propositions of the form ~a, making ~a+~~a=1, and ~a~~a=0, and ~~~a =
~~a).  This retraction is antimonotone, if you need a monotone
retraction just use ~~, the second one flips you back the right way up
while not losing any further information, this is the one that is most
widely used, as e.g. in forcing.

Now equipping a set with a partial order is not very much structure, in
fact so little that the category of posets is just as cartesian closed
as that of sets, meaning basically that the laws ab |- a and ab |- b
(and hence aa |- a) still hold, as does a |- aa.  So conjunction
remains idempotent and weakening ab |- a (projection from the
transformational perspective) is still allowed.  (In the Gentzen
setting the important direction of idempotence becomes contraction,
weakening is still weakening but just moved around a bit.)

But linear logic's passage to *arbitrary* structure makes a much bigger
difference.  Now at this point I need to switch to linear logic
notation to avoid confusion, since LL has two sets of conjunction and
disjunction operations and it is important to keep them straight.

I'll talk just about multiplicative linear logic, MLL, the additives
are support for the passage back to intuitionism and needn't concern us
in an introduction to LL.  I'll write conjunction as A at B, called tensor
product.  Shockingly there is an involutory negation A' (I'll explain
where that came from in a minute), with respect to which it makes sense
to talk of a De Morgan dual A#B of A at B, MLL's disjunction, which Girard
calls par for "parallel".  Even more shocking is that implication is
defined as A -o B = (A at B')', as though we were back in Boolean logic!

Arbitrary structure kills off both A at B |- A and A |- A at A, and also the
distributivity of conjunction and disjunction over each other.  What
survives is a weak or linear distributivity law that is at the heart of
linear logic:

	A @ (B#C) |- (A at B) # C

(This law will be familiar to fans of relation algebra, reading @ as
composition or relative product and # as its De Morgan dual, Peirce's
relative sum.  Composition being noncommutative, unlike tensor product,
Peirce needed two such---he wrote that these laws are "so constantly
used that hardly anything can be done without them".)

Ok, so which laws hold and which don't?  Well, the above is a good start
on the general shape of things, and I wont go into any more detail as to
the exact set of laws that hold in linear logic.  Instead I'll focus on
the methodology for deciding which to keep and which to toss.

First we need to address the question, where the heck did this
involutory negation come from?  Well, in linear logic negation means
something entirely different from Boolean logic.  The Boolean negation
of a proposition switches the two sides of the partition denoted by
that proposition.  Linear negation takes place on a completely
different plane, that of transformations between two entire universes,
not partitions within a single universe.  Instead of flipping a
partition it flips a transformation.

For this to make sense the propositions themselves have to denote
differently.  A Boolean proposition denotes one of many possible
partitions of a single universe, and therefore Boolean logic is
appropriate for reasoning internally about a single universe.  A linear
proposition denotes a whole universe, and A at B combines two universes
into a bigger one, their tensor product.  Linear logic is appropriate
for reasoning externally about multiple universes, transforming between
them and combining them.  This is completely dual to Boolean logic,
outside instead of inside!

Just as partitions and transformations are duals of each other, linear
negation is the dual of Boolean negation.  (Recall what I said about
Stirling numbers of the 1st and 2nd kinds being duals or mutual
inverses of each other, and being about respectively transformations
and partitions.  While this might not strike a logician as terribly
significant, Stirling numbers are at the heart of combinatorics.)

The reason linear negation does not appear in Boolean and
intuitionistic logic is because neither sets nor posets form a
self-dual category.  The linear negation of a set would be a (complete
atomic) Boolean algebra, which Boolean logic would be completely unable
to deal with as a universe of sets, since it couldn't carve it up.
Essentially the same happens with posets, whose linear negation would
be a complete completely distributive lattice, also uncarvable.

But when one passes to the larger universe of arbitrarily structured
objects, transformations of A into B can always be flipped because they
now run from B' to A', the duals of B and A, which are no more or less
arbitrary than A and B and make just as much sense to linear logic as A
and B did.   Yet again we see shades of Boolean logic, in this case
modus tollens, yet in meaning this is nothing like Boolean logic!

The reason Boolean negation does not appear in linear logic is because
as soon as structure appears it compromises carving in an asymmetric
way: if a<b then you can cut between a and b one way but not the
reverse way called for by complement.  Linear logic goes way beyond
intuitionistic logic in amount of structure that can compromise Boolean
negation.

So now the question arises, what laws hold and what don't in the
universe of arbitrary structure?  The first step here is to even define
"arbitrary structure".  Actually this is the part that the French
school does worst.  They settle for Hilbert spaces and Banach spaces
and coherent spaces but these aren't terribly convincingly arbitrary.
Girard *postulates* laws, and then checks them against these structures
to verify that they hold.  This establishes soundness at least for
these structures, but it doesn't establish completeness for them since
it isn't true.  And the question of soundness returns again as soon as
one goes outside these structures.

The way I've been going about defining "arbitrary" is to use Chu
spaces.  These nicely interpret all the linear logic connectives.  And
they model "arbitrary" structure in several senses.  One is that every
category with a set of at most K morphisms embeds fully, faithfully,
and concretely in the category of Chu spaces over the set K.  And there
are other such full embedding results that you can dig up by browsing
around in http://boole.stanford.edu/chuguide.html, let me know if you
need help.

What we now believe to be the case is that Girard's laws are spot on
for this notion of arbitrary structure.  Not only does he have the laws
right, he even has the exact proofs in his proof system corresponding
to what takes place within the semantics in the form of robust or
logical transformations!

To summarize: Boolean logic and linear logic are duals of each other,
with the former concerning the logic of partition or truth and the
latter the logic of transformation or construction.  In terms of the
structures equipping their respective domains, Boolean logic sees no
structure while linear logic sees all conceivable structures.  The
respective negations of these logics are both involutory because both
reverse things, partitions within a universe in the Boolean case,
transformations between universes in the linear case.  The former is
the logic of changing sides in an argument, the latter is the logic of
passing from proof to refutation.  The two are tantalizingly like each
other, yet we know from the failure of idempotence and weakening for
linear logic (which hold for Boolean and intuitionistic logic as a
corollary of Set and Poset being cartesian closed) that they are not
the same logics!

Intuitionistic logic takes a small step towards the full-blown
structure of linear logic by introducing just enough structure to break
Boolean negation but nowhere near enough to kick-start linear
negation.  Intuitionistic logic is like the Canary Islands, a small
step from Europe along the way to America.  I think once people start
to see intuitionistic logic in the light of its relationship to the
more important Boolean and linear logics its importance to foundations
will become largely historical.  Very few papers are written about
ordered structures (posets and lattices) compared even to homological
algebra and category theory, and those in turn are very sparsely
populated compared to quantum mechanics and theoretical computer
science.  Intuitionistic logic as the logic of ordered structures
should therefore not expect to remain center stage in the foundations
of mathematics.  Boolean logic has been dominant to date, but I foresee
linear logic emerging as an equal partner with Boolean logic for the
same structural reasons that intuitionistic logic should not be (not
that it ever really was).

Why is linear logic so like Boolean logic, yet differing from it in
certain crucial details?  This I find remarkable.  While I can't
explain it, I'll replace it with another question.  Why are abelian
categories so similar to toposes?  (Those of you following the
categories mailing list this week should recognize what I'm getting
at.)  By rights abelian categories should look nothing like toposes.
Abelian categories are the quasivariety generated by the category of
abelian groups, for a suitable signature.  (Pre)toposes are the
corresponding quasivariety generated by the category of sets.  Even
though the categories of sets and abelian groups (which you *have* to
have heard of even if you hardly know any other categories) look
dramatically different, the respective quasivarieties they generate
differ only by a couple of succinct axioms.  This remarkable fact was
discovered just last week by Peter Freyd.  I'm not sure yet just how
close this connection is to the strong resemblance of linear to Boolean
logic, but I bet there's a connection in there somewhere.

It's all very well for Harvey to say that none of this is relevant to
foundations, but to me it seems *very* relevant, not to mention
fascinating.  Linear logic is a giant breakthrough for foundations.

Vaughan