FOM: proof theory and foundations

[Stephen G Simpson]

I'd like to thank Jeremy Avigad for a very interesting post (15 Jul
1998 16:05:39).  It touches, however lightly, on a lot of important
issues.  There is much food for thought here.  Let me start by
reacting very quickly to some of Jeremy's points about proof theory.

 > my notion of "foundational" may differ from ones that have come up
 > in past discussions (especially those which made reference to
 > "general intellectual interest" and the "average man on the
 > street").

Why the disclaimers?  I was a rather prominent participant in the
discussion of general intellectual interest and men in the street,
a.k.a. barbers, and it seems to me that your notion of "foundational"
is in perfect agreement with mine.  I formulated it as follows:

   Foundations of mathematics (f.o.m.) is the study of the most basic
   concepts and logical structure of mathematics, with an eye to the
   unity of human knowledge.

This is my definition of f.o.m.  It's interesting to note that nobody
on the FOM list has presented an alternative definition of f.o.m.

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

At any rate, we agree on the fact that there is a distinction between
foundational and non-foundational.  That's a very important
distinction.  Some months ago the "list 2" crowd tried to obliterate
that distinction, but I prevented them from doing so.

 > ... proof theory ... is limited in many ways, and doesn't hold all
 > the answers. ...

Why the apology?  *Every* subject is limited, and *no* subject holds
all the answers to everything.  That's why human knowledge is divided
into subjects in the first place: to break down the project of
understanding the whole into manageable parts.  The question that we
are discussing is, what foundational questions are addressed by proof
theory.

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

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

 >   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.  So this seems
to justify at least some of (b) and (c) from the foundational
standpoint.  But what is the foundational significance of, for
example, Rathjen's work on (b) and (c) for Pi^1_2 comprehension?  So
far as I know, Rathjen's work has not yet been applied to the
discovery of finite combinatorial independence results.

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

Jeremy went on to comment on various anti-foundational trends,
including category theory and the Tymoczko/Hersh crowd.  I'll respond
to that in a separate posting.

-- Steve