FOM: proof-theoretic ordinals; core mathematics; Tymoczko

[Stephen G Simpson]

Jeremy Avigad writes:
 > 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.

Not at all.  On the contrary, I want to explore in *explicit* detail
the following question:

   How do the various contemporary directions of research in
   mathematical logic contribute to f.o.m.?

I don't think that only proof theory or only certain branches of proof
theory have something to contribute, as you imputed to me.  We were
discussing a particular instance:

   What do proof-theoretic ordinals contribute to f.o.m.?

That was intended as a question, not a threat to your way of life.

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

Yes, that's roughly what I'm saying.  I would put it this way:
Ordinals such as epsilon_0, Gamma_0, types, recursion theory, etc. are
far from what is called "core mathematics".  Goodstein sequences and
graph minors are much, much closer.  This is an important distinction
for f.o.m.  People who don't understand this distinction can't grasp
the significance of a lot of contemporary f.o.m. research.  You are
not one of those people; you understand this distinction in some form
or another.

 > Your tastes are not universal.

This isn't a matter of taste.  It's a fact.  Core mathematics consists
of algebra, analysis, geometry, differential equations, ..., not
higher-type recursion, ordinal notations, r.e. degrees, etc.  The
latter are studied by logicians, not core mathematicians.  Try
explaining Dialectica to a core mathematician.

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

I agree with this general point.  But I'm not convinced that some of
the particular constructive theories such as intuitionistic ID(<omega)
are *mathematicially* interesting or natural.  On the other hand, the
proof-theoretically equivalent theory Pi^1_1-CA_0 is *known* to be
mathematically natural.  This has been shown by reverse mathematics.

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

Well, for example, a combinatorial independence result shows that a
mathematically natural and therefore foundationally important formal
system, Pi^1_1-CA_0, although very strong from the viewpoint of
mathematical practice, does not suffice to prove a certain
mathematically natural theorem, the graph minor theorem.  This is
clearly, obviously, a striking contribution to f.o.m.

 > Then replace "combinatorial independence" everywhere by "ordinal
 > analysis," and tell me why the result fails to meet your challenge.

It's not clear that we *can* substitute "ordinal analysis" here.
That's my point.  If you know how to make this substitution, please
explain how.  It's true that ordinal analysis contributes as a
technical tool in proving the combinatorial independence result.
That's also part of my point.

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

Yes, that's right.  "Quasi-empiricism" in a very unformed or
undeveloped state, as compared to f.o.m.

What I don't understand about these people is, why are they so angry
at f.o.m.?  For example, Tymoczko's lead essay is entitled "Against
Foundations" and goes out of it's way to dump all over
"foundationalism", without ever defining that term.  Why the
hostility?

-- Steve