FOM: FoundationalCompleteness

[Vaughan R. Pratt]

I apologize in advance for continuing to use physics as an example.
Unfortunately it's the only example I have where dualism has succeeded.
I'm hoping that the metamathematical theorems some of us on the
transformational side of things are shooting for will make foundations
a second such example.

>However, it also does not come close to doing everything one might demand
>of a foundation for mathematics. At the present time, there is no full
>blown proposal for scrapping it and replacing it with anything
>substantially different that isn't far more trouble than its worth. Present
>cures are far far far worse than any perceived disease.

No, no, you don't understand.  Think of what happened to last century's
wave theory of light.  No one's replaced it this century, it's just
been rendered more consistent by the addition of a particle theory of
light.

What structuralism is (or should be) proposing is to account for the
proofs and their denotation as transformations, based on a formal
system as rich as that currently used to account for propositions and
their denotation as partitions.  The detailed structure of this system
will be that of linear logic, the formal side of whose multiplicative
fragment, MLL, is comparable in complexity, elegance, and mathematical
relevance to classical propositional calculus.  Just as the basic
semantic entities for propositional calculus are 0 and 1 (the *'s in my
diagram), so is the basic semantic entity for MLL the abstract
transformation or morphism (the edge in my diagram).  Just as 0's and
1's combine under Boolean connectives, so do edges combine under
composition.  A cut-free MLL derivation starts with an untangled set of
edges and derives theorems in which those edges become more or less
tangled up in each other.  The Danos-Regnier theorem gives an elegant
derivation-independent characterization of the derivable such tangles.

If this sounds like meaningless gobbledigook it isn't.  One needs to
work patiently through the material to appreciate it.  It is
unfortunate that the writing style of the current expositors, myself
included, slows this down.

>It just that people should recognize what's involved in
>doing such an overhaul, and not fool themselves into either
>
>	i) embracing something that is either essentially the same as the
					      ^^^^^^^^^^^^^^^^^^^^^^^
>usual set theoretic foundations of mathematics; or

Transformations are "essentially the same as" partitions only in the
sense that waves are essentially the same as photons.  Physicists do
not argue that the equivalence of the photon and wave viewpoints makes
the photon viewpoint irrelevant to physics.  The same reasoning applies
here.

>	ii) embracing something that doesn't even minimally accomplish what
>is so successfully accomplished by the usual set theoretic foundations of
>mathematics.

Replacing truth and sets isn't the goal.  The goal is proof and truth
as equal partners, not proof as the servant of truth.  Hand in hand
with this is the goal of sets and categories as equal partners.

>THEOREM. Sets under membership form the simplest foundationally complete
>system.
...
>Mathematicians do not want to go down that road again, and are comforted by
>the fact that this matter has been resolved by set theory - even if it does
>not provide for a directly faithful formalization of the way they actually
>visualize and think. In summary, there is a danger of the cure being far
>far far worse than the disease.

This is presumably more or less how physicists felt about waves in 1900
as an explanation of light.

>Ex: Let E be a subset of the unit square in the plane, which is symmetric
>about the line y = x. Then E contains or is disjoint from the graph of a
>Borel measurable function.

It is an interesting question whether the interest in such subsets
derives directly from an application of mathematics, as Harvey and
Adrian (and others?) have been arguing, or indirectly from an
unacknowledged pathology of their framework.  My suspicions are with
the latter.

Vaughan Pratt