[Prev][Next][Index][Thread]
Re: Categorical Models of Linear (and other) logics
* What are categorical models of logics good for?
1. They help us understand term assignment systems for these logics.
2. They help us prove results about our logics, as we can use CT.
3. We can show that our favourite logic corresponds to some
already-found structure in category theory, and hence, our
logic gets brownie-points for being `natural.'
4. The category (or class of categories) we are interested in
is the *intended model* for our logic.
Are any of these answers correct? If so, which of them?
Linear logic is a *resource sensitive* logic: premises may be supplied
only on a need-to-know basis, as with relevance logic. However LL goes
a step beyond R in insisting that premises be supplied *in proportion
to* demand (linearity): a premise used twice must be supplied twice.
I must leave the defense of your 1-3 to others, they are beyond my
ken. My entire interest in LL is via 4. The connection between
resource sensitivity (understood as a purely proof-theoretic
phenomenon) and categorical models is that resource sensitivity is the
proof-theoretic manifestation of algebraic structure, specifically of
the kind compromising cartesian closedness, such as constants (pointed
sets) and binary operations (semigroups). Such structures are the rule
rather than the exception in mathematics, whence logic should by
default be resource sensitive. The exceptional cases, where the
neighborhood of the category is sufficiently pure as to be cartesian
closed, are marked in LL with ! to indicate where accounting for
resources may be turned off.
So why is traditional logic not resource sensitive? It seems to me
that this is primarily the result of a long-standing distinction
between "logical" and "nonlogical." "Logical" has traditionally meant
"pure" in the sense of "prelinguistic:" the pure first order predicate
calculus leaves its relation symbols uninterpreted, whence the
individuals constituting its domain of discourse form merely a set with
no structure or properties. But Set is cartesian closed, and so this
characteristic is inherited by the pure predicate calculus.
One might suppose that the nonlogical symbols and axioms of a theory
would force resource sensitivity. However first order logic does not
respect the structures implicit in those symbols and axioms, in that it
allows n-ary operation symbols on a universe X to be interpreted as
arbitrary functions from X^n to X subject *only* to the theory. There
is no requirement that anything commute with anything. Thus even when
first order logic seems to be describing groups it never really leaves
the category Set.
Linear logic turns straw-sucking stick-at-home traditional logic into a
jet-setting traveler that can move from sets to semilattices, vector
spaces, Boolean algebras, and most other familiar mathematical
objects. This "movement" is on the one hand transformational---one
moves between vector spaces via linear transformations---and on the
other proof theoretic---one moves between propositions via proofs.
The connection between these is made via the Curry-Howard isomorphism,
which interprets objects (types) as propositions and morphisms (which
in normal mathematics are homomorphisms or structure-preserving
operations between objects) as proofs.
For more discussion of categorical models of linear logic, see my
PhysComp'92 paper, Linear Logic for Generalized Quantum Mechanics,
ftp://boole.stanford.edu/pub/DVI/ql.dvi.Z. It treats quantum logic and
compares it with Girard's phase semantics as a nonconstructive model of
linear logic. Next comes a section motivating constructive logics,
taking the defining characteristic of constructivity to be *how* a
theorem follows from its premises in contrast to merely *whether* it
does. Then two categorical models of linear logic are treated,
coherence semantics and event space semantics, and interpreted as
constructive quantum logics. It is then argued that such constructive
logics of quantum mechanics expose certain aspects of quantum
mechanics, such as the measurement process and Heisenberg uncertainty,
in a way that does not seem possible with nonconstructive logics such
as Birkhoff and von Neumann's quantum logic. QL is little more than a
nonconstructive logic of projective geometry, and its place in quantum
mechanics is roughly comparable to the place of Boolean logic in
mathematics.
My forthcoming LICS paper, "The Stone gamut: A coordinatization of
mathematics," paints a rather larger picture of this situation in which
a sizable segment of "concrete mathematics," including but by no means
limited to all models of first order logic, is characterized as a
single homogeneous model of linear logic---homogeneous in the sense
that topological spaces, semilattices, vector spaces, distributive
lattices, locales, and so on are all mingled freely together in the one
large but pleasantly structured categorical model of linear logic. It
seems to me that this esthetically pleasing picture of "math in the
large" offers a more convincing justification of linear logic than
methodological arguments from proof theory. I suppose this makes me
something of a Platonist, my emphatic protestations to the contrary on
sci.logic notwithstanding.
That concurrent behavior and quantum behavior can be simultaneously
linked into the same picture might seem like gilding the lily. However
the concurrent behavior connection was the route by which I arrived at
this view of things, so it would be a bit unfair of me to deny this
connection after the fact.
Vaughan Pratt