FOM: thinking linearly?

[Vaughan Pratt]

Feferman 3/10 2:42Pm
>It's easier to think in classical logic than in more restrictive logics
>(and thank god no one is asking us to actually think in linear logic),...

From: Harvey Friedman 3/10 8:14PM
>This is an important point. But is *no one* really true, Vaughn?

Thinking about Harvey's question just now, I realize that I had
underestimated the impact of the "epiphany" I mentioned having in 1979
when I was able to shorten a long proof by judicious use of algebra.

Before then my tendency was to regard reasoning as symbolic computation
and to treat metamathematics the same way I treated Turing machines (which
I was very good at thanks to years of research and teaching in that area).
Furthermore I understood my own reasoning as being just such a formal
system, modulo the mysterious oracle we all seem to be equipped with.

After then however my focus shiftly abruptly from the operational or
formalist side to the denotational or platonic side and I found myself
restating the very same theorems as facts about mathematical objects
instead of about symbol manipulation.  Actually *seeing* that they
were the same theorems was not at all obvious to me at first, but with
time it has become clearer.  FOM readers will be familiar with these
notions from their experiences with model theory, ultraproducts, etc.,
but the basic ideas can be found in many institutions besides that of
the elementary classes, including those too simple to qualify as a logic
in any reasonable sense.

In retrospect, the surprising thing is that my own mathematical thinking
seems to have tracked how I thought about thinking.  Maybe it didn't
actually change, although it certainly now seems that way to me.

This in turn has greatly colored my impression of what logic is or at
least can be, although admittedly very slowly.  Around 1989, ten years
after my (re)introduction to algebra (which I had learned as a pure
maths honours student at Sydney University but had long since abandoned
as irrelevant) it seemed to me that the basic type of reasoning I wanted
to perform (or rather that I wanted computers to perform) on concurrent
processes was not manipulation of formal statements about them but
manipulation of the processes themselves, viewed as mathematical objects
in the same sense that a poset or manifold is an object.  The most
basic manipulations I found myself focusing on were a small library of
transformations that matched up very well with propositional entailments
and whose laws for manipulating those transformations (so we're back
to symbol pushing but now the symbols denote transformations *of*
objects instead of individuals *within* objects) also matched up well
(but seemingly not exactly) with derivations in classical logic.

Back then I regarded linear logic as analogous to what I was doing but
different in crucial respects that (I assumed) made concurrency theory
different from proof theory (my take then on what linear logic was about).

But these differences gradually evaporated between 1989 and 1993, which
had the advantage of persuading me that I was on the right track and
the disadvantage of lessening my own contribution.  Today I find myself
working on completeness questions for the linear logic of what I work
on, originally computational objects, specifically concurrent processes,
but now broadened to include mathematical objects.  The new insight here
is to view both on the common ground of the interaction of points and
states.

The cocktail party formulation of this principle is the interaction of
Across and Down in crosswords.  Not everyone can be relied on to know
both ZFC and category theory at a cocktail party, or even one of them.
But *everyone* knows how crosswords work.  The key to starting a new
religion is to have a simple message.

Apropos of this (but not yet benefiting from the crossword metaphor),
surfers of the web may find the following of interest.

	http://boole.stanford.edu/parikh

This is the HTML version (courtesy of latex2html) of an invited paper
on the occasion of Parikh's 60th birthday.  If you prefer hard copy,
download and print

	http://boole.stanford.edu/pub/parikh.ps.gz


Vaughan Pratt
Interests: Foundations of computation and mathematics
URL: http://boole.stanford.edu/chuguide.html