FOM: High aspirations for FOM - A Modest Proposal*

[Vaughan R. Pratt]

	Another candidate for the subject line was: "It's how they do
	it, not what they do, stupid", a takeoff on a slogan of the
	1992 Clinton campaign for President.  No personal aspersions
	intended! It's a way of suggesting a change of focus toward
	more consideration of how mathematics is practiced as opposed
	to the collection of theorems that result. Close to but not
	quite what Pratt is suggesting.

If there's a difference it's in the asymmetry.  "How" and "what" is
exactly the distinction I've been focusing on, but I wouldn't place
either ahead of the other intrinsically.  I know I seem to be favoring
"how" over "what", but that's because I'm of the "if it's not broken
don't fix it" school of thought, and I think we're all in agreement
that the foundations of "how" in mathematics are in worse shape at
present than of "what".

Here's a bit more on my position.  It's long on form and short on
content, sorry about that.

In at least two senses the shape of mathematics to me is

			* ======== *

One sense is that this is the Stone gamut, with sets on the left (the
discrete or geometric end of math) and Boolean algebras or dual sets on
the right (the coherent or algebraic end), with "the rest of
mathematics" spread out in between.  Far from a finite universe, at
least if we count objects, but one with a clearly visible boundary
consisting of familiar objects.

For the second sense I'll tabulate the what and how of mathematics (one
of the two dimensions I mentioned in my previous message) into the
symbolic (I think this is what people have in mind by idealism, yes?)
vs. the Platonic, the other dimension.  (So the lower right 2x2 square
of the table, the all-caps part, are the four corners of my 2D view of
math.)

                      |    Shape      |   Symbolic  |   Platonic
   	    ----------+---------------+-------------+------------
             What:    | * :::::::: *  | PROPOSITION |   PARTITION
                      |               |             |
             How:     | . ======== .  |    PROOF    | TRANSFORMATION

Propositions and proofs denote respectively partitions and
transformations.  What makes them symbolic is not that they are
physical ink on paper or entities in the mind but that they denote.
Even abstractions can denote, a sine qua non of metamathematics.

A proposition denotes a partition of the domain of that proposition.
The domain might be worlds (as in Kripke structures, the domain of
propositional modal logic), individuals (the domain of a predicate), or
n-tuples of individuals (the domain of an n-ary relation).  Here the
two *'s symbolize the most popular partitioning, into two blocks, but I
am very much in favor of small refinements in the range of three to
eight blocks, much more than that raises interesting questions.  The
edge as the dividing agent of partition is dotted to indicate
inaccessibility, a gulf between the partitions.  As such it is a
negative or "box" edge, imposing a constraint.

The characteristic operation of logic is negation: a logician is an
algebraist who can say no.  In that respect the integers (and more
generally groups) make the natural numbers (and more generally monoids)
more logical, while fields do the same for rings.  However the kind of
negation there is cancellative with respect to accumulation: you can
add 1 and then take it back.  Negation for propositions, at least in
the two-* case, interchanges the *'s.  It resembles arithmetic negation
in being involutary, but differs from it in not being cancellative with
respect to accumulation (if you falsify a proposition by conjoining
"false" to it, you cannot undo this by conjoining another
proposition).

A proof denotes a transformation of the givens into the result(s).  The
edge denotes the passage from input to output.  The edge as the joining
agent of connection is solid to indicate flow, a bridge or road between
stations.  As such it is a positive or "diamond" edge, enabling
passage.  The *'s are reduced to dots to indicate the ongoingness of
proof, as with a long train trip where you don't see the stations for
most of the trip.  They also change character: instead of being the
opposite sides of a canyon they become source and sink for a flow.

As for propositions, negation for proofs still interchanges the *'s.
However the meaning of the interchange is now to replace proof by
refutation, in the process negating the propositions at each and
reversing their roles as source and sink.

Readers of Barwise and Seligman's "Information Flow" (CUP 1997) should
find this flow view of proofs very compatible with their point of
view.

The basic difficulty I have with their point of view is that when they
pass from the symbolic to the Platonic, from operational to
denotational semantics if you will, their entire viewpoint narrows to
just the What line, treating the denotation of proof in terms of
partition rather than transformation.  To the extent that proofs
connect propositions and propositions denote partitions, a link from
proofs to partitions indeed exists.  But B&S make partition the
semantic *basis* for proof.  This is quite wrong.  The semantic basis
for proof is not partition but transformation.

The correspondence between the two is made by identifying sound proof
with natural or robust transformation.  Just as most random proofs are
unsound, most random transformations are unnatural.  The full
completeness proofs now starting to appear for linear logic (the
appropriate logic of proof) take the form of a bijection between
cut-free proofs and natural transformations, just as completeness for
propositional logic puts theorems in correspondence with tautologies.

That will have to do for now, if I said any more I might inadvertently
break my promise and say something contentful.

Incidentally it just struck me that the Stirling numbers of the first
and second kind, which are duals (more precisely, infinite-dimensional
inverses) of each other, count respectively permutations of n things
having k cycles, and partitions of n things into k blocks.  So
partition and permutation (as invertible transformation) are as dual in
combinatorics as they are (or should be) in logic!

Vaughan