FOM: ReplyToPratt

[Harvey Friedman]

Here is a general comment on Pratt's postings: they suggest an alternative
view of the foundations of mathematics that somehow is going to incorporate
both structuralist ideas (e.g., category theory and topos theory) and
traditional f.o.m. (set theory, predicate calculus, etc) into one combined
theory side by side. One of the pieces of glue is to be linear logic.
However, as far as I am concerned, I don't see (in these postings) a single
simple, cogent idea of how this is to be done. In particular, many people
on this e-mail list don't know what linear logic, and many of the people
who do, don't have a positive impression of it. At least they don't see why
it is important or useful in foundations of mathematics, and in particular
what it has to do with any substantive concept of mathematical proof. Until
this is made clear for the group in simple, basic terms, with simple, basic
examples, I suspect that such postings serve no useful purpose.

>I'd like to propose the following as a suitable program of research for
>anyone interested in making the sort of sense of structuralism that
>Harvey has been quite rightly demanding.  The general idea is to unify
>the propositional and constructive views on foundations as a single
>coherent framework.

How?

>First, with suitable care this program has the potential to inherit
>essentially intact the entire tradition and technology of two important
>tracks in foundations.  The first is the conservative track defending
>FOL, more than adequately represented on FOM.  The second is the
>constructive track originating with Brouwer (on whose life btw Dirk van
>Dalen will speak at LICS this year).  More specifically it focuses on
>the path through Gentzen culminating in Girard's linear logic (LL).

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 a grue critter, so to speak, I find the FOM view of mathematics just
>as extraterrestrial.  A lot of you seem to believe that everything is a
>set, and claim not to understand the point of view of those who deny
>this.  As an interesting corollary, size (the only property a set can
>have up to isomorphism) looms large among what you regard as the most
>important questions of foundations.

Size does not loom large in the kind of state of the art foundations of
mathematics that I do. "Everything is a set" is a gross oversimplification
of the usual f.o.m. viewpoint. The size thing is not a corollary.

>The corresponding point of view in mathematics *should* be that
>everything can be understood equally well as consisting of sets or
>Boolean algebras, and optimally as a blend thereof.

I do not believe that any significant amount of anything can be equally
well understood solely in terms of Boolean algebras. I stated the "Theorem"
that asserts that sets are the simplest foundationally complete system - as
you recall, unfortunately I don't quite know what this assertion means. But
it is clearly true.

Exercise for Pratt: write some basic real analysis solely in terms of
Boolean algebras.

>In reducing
>mathematics to sets you commit the same error a physicist would make in
>reducing physics to particles.  Interestingly, both errors can be
>documented by essentially the same underlying machinery.

The mathematicians have a trivial translation of all of mathematics into
sets that is sufficiently powerful so as to obtain crucial nonderivability
results. A forced reduction of physics to particles is comparatively very
crippled.

Please document for us, in the clearest possible basic terms, this "same
underlying machinery."

>Everything changes in
>mathematics, some faster than others.

Basic classical mathematics is relatively unchanged. The classical number
systems are unchanged. So what do you mean by this?

>A proof denotes a transformation of the givens into the result(s).

Attempts to illuminate proofs as transformations have been uninspiring,
leading to uninformative messes. Do you have any better ideas?

> 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.

In what sense is linear logic "the appropriate logic of proof?" State at
least two examples in the clearest most basic terms. Do you think that no
serious mathematical proof is cut-free, and if so, does this indicate that
what you are talking about may be unimportant for the foundations of
mathematics?

>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 [of duality].

Can you state some metamathematical theorems you are shooting for and why
they would have any impact on foundations of mathematics?

>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.

As I said above, it is not generally believed that anything significant is
going to come of genuine mathematical proofs as transformations. That
doesn't mean that nothing significant will ever come of this. It's just
that you are on the spot to say something basic and intelligible that lends
credence to this idea.

>  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.

Show us this in the clearest basic terms, so that we can evaluate it.

 > 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.

Sounds like an algebraic trick, and not something fundamental; perhaps not
a fundamental explanation of anything.

> 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.

In the usual foundational setups, as I said earlier, no really interesting
mathematical proof is cut-free. How does this effect the significance of
what you are saying?

I wrote:

>>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

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

Pratt wrote:

>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.

I meant things like: using (set theoretic) functions as primitive instead
of sets. I reject the analogy with photon/wave. The sense of translation
between functions and sets is different than the relationship between
photon and wave.

>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.

"Equal partners" is much too vague. You need to give some sort of
indication as to how you are going to combine these. Set theory is already
a spectacular success on many many levels, whereas category theory is not
(as a foundation). Therefore "equal" needs considerable justification.

Friedman wrote:

>>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.

Pratt wrote:

>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.

I am assuming for the moment that this was not intended as a gratuitous
insult. So what does "an unacknowledged pathology of their framework" mean?
There are over 10000 papers in which Borel measurable subsets of Euclidean
spaces are mentioned.

>I would claim that linear logic is, in the loose sense of this analogy,
>the "Fourier transform" of first order logic, preserving its content
>while reorganizing its structure to give the dual perspective.

In order for comments like this to be useful to the e-mail list, there has
to be a great deal more explanation at a very basic level. You haven't even
told us what linear logic is and why it is interesting.