FOM: Reply to Simpson

[Jeremy Avigad]

I'd like to respond to some of Steve Simpson's July 21 responses to my
July 15 FOM posting.

>  > I am trying to use the word "foundations" in a value-neutral way. I
>  > do not mean to suggest that foundational research is better than
>  > non-foundational research, or that all work in logic should be
>  > strictly foundational; ...
> 
> OK, fair enough.  But eventually one has to decide that some research
> projects are more valuable than others.  These value judgements come
> up all the time, every day, in deciding issues such as: what papers to
> read, what topics to teach in courses, which grant proposals to fund,
> which researchers to hire or promote, etc.  Surely you are not
> suggesting that there are no rational criteria here?

Certainly not. But from your postings, one might suppose that your
decision tree looks something like this:

  logic   
     foundations 
       proof theory
         reverse mathematics = GOOD
         combinatorial independences = GOOD
         ordinal analysis = BAD
         functional intepretations = BAD
       not proof theory = BAD
     not foundations = BAD

I am merely trying to make it clear that the criteria I would use to
evaluate a grant proposal or make a hiring decision are much more complex.
There is good work in logic that is not foundational, good work in
foundations that is not in proof theory, and good work in proof theory
that doesn't involve reverse mathematics or independent combinatorial
statements.

You seem to feel that we should all agree on a single programmatic
approach to f.o.m. and support it to the exclusion of all others. This
strikes me as dogmatic and narrow-minded. It's much healthier to entertain
a multiplicity of viewpoints than to try to force all foundational
research into uniform cubbyholes. As much as I love my field (and I do), a
world full of nothing but proof theorists would not be a very interesting
place to live.

>  > I would characterize the second part of the program as
>  > 
>  >   Obtain satisfying constructive analyses of these formal systems
>  > 
>  > The problem with this last characterization is that it is vague.
> 
> I see another problem: You are making the goals of proof theory
> dependent on some prior notion of "constructive analysis".  Is this
> really what you want?

I am trying to give an informal characterization of the field's goals. I
don't understand your objection, i.e. what an "independent" statement of
these goals should look like. Is it that I don't have a formal definition
of the term "constructive"? What, exactly, are you looking for?

>  >   a) Prove the consistency of the theory relative to a constructive
one
> 
> This is foundational if you show that the constructive theories in
> question are of prior foundational interest.  I have my doubts about
> some of them.  For example, why would constructive or intuitionistic
> ID(<omega) have foundational interest prior to classical ID(<omega)?

Again, I'm not sure what you mean by "prior." I am suggesting that some
classical theories are interesting because they formalize aspects of
mathematical reasoning; and that some constructive theories are
interesting for the same reason. And given an interesting classical theory
and an interesting constructive theory, it can be interesting to know that
in fact the two prove the same Pi_2 arithmetic statements. The result is
"foundational" because it clarifies the relationship between two
fundamentally different conceptions of mathematics, by clarifying the
relationship between two fundamentally different forms of mathematical
reasoning.

>  >   b) Find natural characterizations of the theory's proof-theoretic 
>  >      ordinal
>  > 
>  >   c) Find natural characterizations of the theory's provably total 
>  >      recursive functions
> 
> Isn't this begging the question?  Provable ordinals and provable
> recursive functions are fun and interesting, but the question at hand
> is, what do (b) and (c) contribute to our understanding of basic
> mathematical concepts and the logical structure of mathematics?
> 
>  >   d) Find natural combinatorial theorems that lie just beyond the
>  >      theory's capabilities
> 
> Yes, (d)'s foundational contribution is more evident, because clearly
> an important part of the f.o.m. enterprise is to understand the
> mathematical limitations of the formal systems that arise in
> formalizing mathematics.  And (b) and (c) have contributed to (d) via
> Goodstein sequences, Kruskal trees, graph minors, etc.

Do you mean to imply that computable functions, types, ordinals, notation
systems, inductive definitions, etc. are not mathematical objects, but
Goodstein sequences and graph minors are? Your tastes are not universal.
One can argue that forms of higher-type recursion express natural
computational principles, and that ordinals like epsilon_0 and Gamma_0 are
natural mathematical creatures; while many of the combinatorial
independences that come out of proof-theoretic research are forced and
contrived (though also fun and interesting). I do not wish to take this
position; only to point out that what counts as an interesting
"mathematical limitation" is in the eye of the beholder.

>  > we have proof theoretic ordinals that characterize the simplest
>  > forms of impredicativity, with "collapsing" properties that serve
>  > as paradigms of these reflection principles.
> 
> I don't understand.  Let's get explicit.  How do collapsing propeties
> contribute to our understanding of the logical structure of
> (predicative vs impredicative) mathematics, etc?  Please be explicit,
> and please try to say it in terms that can be understood by somebody
> who is not intimately familiar with these very complicated systems of
> ordinal notations.

First, let me ask you to tell me how a combinatorial independence
contributes to our understanding of the logical structure of mathematics
(in a manner in accordance with the terms you've set above). Then replace
"combinatorial independence" everywhere by "ordinal analysis," and tell me
why the result fails to meet your challenge.

>  > Many category theorists ... may feel that proof theorists are
>  > missing the point entirely. ...  Taken alone, neither the
>  > ontological nor the structural account tells the whole story; but
>  > taken together, they complement each other nicely.
>
> My problem with the category theorists, Bourbakians, and other
> structuralists is precisely that they fail to recognize this.  They
> delude themselves into thinking that structure alone is important.
> This has resulted in further fragmentation and isolation of
> mathematics from the rest of human knowledge.  Jeremy, you are trying
> to make friends with the structuralists, but is it worth it?

Certainly-- some of my best friends are structuralists, and many are doing
good research.

Let's be reasonable, Steve. The category theorists I've met so far have
been perfectly willing to discuss the relative merits of various
foundational approaches, and are supportive of the work I am doing even
though my field is is different from theirs. So I can't really share your
sense of gloom and doom. Of course, every field has closed-minded,
obnoxious polemicists, and I don't support that kind of behavior. But I'd
rather work constructively with the remainder to try to understand the
different approaches. The divisive bickering is, I think, bad for the
logic community as a whole.

> I reviewed this anti-foundational trend in my FOM posting 
> 
>      FOM: Tymoczko's book; "quasi-empiricism"; the gold standard
> 
> of 1 Feb 1998 22:17:36.  Hersh seems to have gone off on a strange
> political tangent.  What I find truly bizarre about the self-styled
> "quasi-empiricists" is that they refuse to acknowledge the current
> standards of rigor in mathematics.  Jeremy, do you have any idea what
> is eating these people?  Why are they so bitterly and irrationally
> opposed to f.o.m.?  Are they angry at f.o.m. for disparate reasons, or
> is there a common denominator?

What I find interesting is that you can make comments like the these, and
then wonder why people react negatively to f.o.m. Steve, what's eating
you?

I own a copy of Tymoczko's book, and I enjoyed reading the essays a few
years ago. (As I recall, I particularly liked the essay by Hao Wang.) Now,
my work in proof theory is about as traditional as it gets, so I am
certainly a target of the anti-foundational rhetoric you describe. Does
this bother me? Not really. It seems to me that the thrust of the book is
to counter a foundational stance that asserts that there is nothing
philosophically interesting that one can say about mathematics that is not
adequately captured by the axiomatic-foundational model. Cast in those
terms, this is a rather narrow-minded and unattractive position. Tymoczko
is setting up a straw man, trying to characterize the research program by
emphasizing what it is not. Of course, the opposite extreme is similarly
ridiculous; no one in their right mind will claim that the
axiomatic-foundational model has had *nothing* to contribute to
philosophical inquiry, or that formal proof has nothing to tell us about
rigor in mathematics. I think most people, when not pushed to extremist
rhetoric, are willing to subscribe to more moderate views: the
axiomatic-foundational model is a very fruitful one, but perhaps there are
other interesting things that one can say about mathematics that are not
captured by this model. 

These "anti-foundationalists" you refer to have their work cut out for
them; right now, they have only some vague (though well-motivated)
questions, and they are still groping around for a methodology. So let's
see what they come up with. I want to make it perfectly clear that I am
not advocating that we abandon all standards in evaluating their research:
I'm sure that a lot of flaky, dull, and uninspired research goes on in the
new program, though, of course, the same is true in any field of academe.
It seems to me that the responsible and scholarly way to respond to the
developments is to offer thoughtful and reasoned criticisms of the
approaches that do not seem promising, while supporting ideas that have
more merit. Much of the f.o.m. discussion has gotten a bad rep, because
too many participants have shown up with chains and brass knuckles,
looking for a rumble. What's up with that?

In any event, I am not here to critique a research program that I don't
know much about. I have tried in my initial posting to convey some of my
personal motivations for doing the work I do, in the hopes that some
readers might find among these motivations sufficient reason to support
their local proof theorist; and I have tried to urge a more liberal
conception of f.o.m., which recognizes that different programmatic
approaches may be needed to understand the methodological framework in
which mathematicians practice their art. Having given it my best shot, I
would much prefer to get back to other things. The defense rests.