FOM: proof theory and foundations

[Jeremy Avigad]

Recently Steve Simpson asked proof theorists on the FOM list for a
discussion of ordinal analysis, and how it fits in with proof theory's
general foundational goals. Having laid low for a while, now I'd like to
throw in my two cents, and discuss the value of proof theory more
generally. What follows is a personal account of why I find proof theory
worthwhile. These are just my own views; I do not claim to represent the
larger proof theory community. 

I am looking forward to hearing people's reactions. I will be away for
much of the next few weeks, however, so I may not be able to respond until
late August.

Let me start by noting that I consider proof theory to be foundational,
but 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"). In the sense
I wish to use the term, studying the foundations of any practice involves
analyzing the basic concepts and methodological assumptions of that
practice. The foundations of mathematics, on this account, involves trying
to identify and understand the basic components of mathematical activity.

Realizing that I am sailing into dangerous waters, let me add some
clarifications. According to my definition, some lines of research in
mathematical logic are more foundational than others, whose motivations
are more mathematical in nature; and there is no sharp line dividing the
two. 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; indeed, one can reasonably take the view that engaging in
fom is like playing "armchair quarterback" to more worthy mathematical
pursuits. When I use the word "foundational" I am trying to characterize a
class of attitudes and goals; I certainly do *not* wish to imply that they
are the only valuable attitudes and goals in mathematical logic.

Second of all, when I discuss proof theory it will be clear that the field
takes a certain, rigidly-defined approach to dealing with foundational
issues. I feel that this particular approach is a good one, and that it
yields important insights. But at the same time it is limited in many
ways, and doesn't hold all the answers. At the end of this note I will
discuss some of these limitations; for now, let me make it clear that when
I discuss proof theory and its methods I do not mean to imply that they
represent the only approach to fom.

Proof theory, roughly speaking, adopts the following view: mathematics
consists of proving theorems about mathematical objects. That is,
mathematicians make assumptions about the universe of mathematical
objects, and investigate the consequences of these assumptions. To study
the foundations of mathematics, one should try to determine out what these
assumptions are, and what constitutes a legitimate proof.

This translates into the following program:

  1) Develop formal systems, based on axioms and rules, that model 
   various aspects of mathematical practice

  2) Study these formal systems, using mathematical techniques and 
     methods

Hilbert's original program was even more narrowly defined; it replaced the
second part by 

  Use finitary reasoning to prove these formal systems consistent

Of course, Goedel's incompleteness theorems showed this to be
impracticable. In its place,

  Use constructive reasoning to prove these formal systems  
    consistent

represents a "modified Hilbert's program," and

  Extract constructive information from these formal systems

is sometimes known as "Kreisel's program." Most broadly speaking, 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. This is
proof theory's curse; it invites the criticism that the field's goals are
not well-defined, or non-mathematical. Despite this weakness, however, the
general aim as I've described it has been realized in a number of
interesting ways. Given a theory that represents some fragment of
classical mathematics, we can try to
 
  a) Prove the consistency of the theory relative to a constructive one

  b) Find natural characterizations of the theory's proof-theoretic 
     ordinal

  c) Find natural characterizations of the theory's provably total 
     recursive functions

  d) Find natural combinatorial theorems that lie just beyond the
     theory's capabilities

Without the word "natural," parts b to d become trivial; and we have no
formal definition of what it means to be natural. In fact, we don't even
have a formal definition of what it means for a theory to be
"constructive." Terms like these bring to mind the Supreme Court justice's
characterization of hard-core pornography: it is hard to define, but we
know it when we see it.

Consider the case of first-order (Peano) arithmetic. It's a nice theory.
We know that in PA you can carry out a lot of combinatorics and number
theory by coding finite objects as numbers. There is a second-order
version, ACA_0, in which one can formalize a surprising amount of
mathematics. An easy model-theoretic or proof-theoretic argument shows
that PA and ACA_0 prove the same first-order statements; but in some
cases, there is necessarily a superexponential increase in length when you
translate proofs from ACA_0 to PA. 

Peano arithmetic proves the same Pi^0_2 statements as its
intuitionistically justified analog, Heyting Arithmetic. We can also
formulate theories of equivalent strength in the language of set theory,
Martin-Loef's constructive type theory, or Feferman's language of
operations and classes. 

PA has a nice ordinal, epsilon_0. We can characterize the theory's
provable functions as those that are <epsilon_0 recursive, or,
alternatively, using a schema of primitive recursion in the higher finite
types. We have interesting combinatorial statements that are equivalent to
the 1-consistency (Pi^0_2 soundeness) of arithmetic, in the form of both
Ramsey-type theorems and WQO theorems.

Now, PA formalizes a certain kind of reasoning; let me call it
"arithmetic" reasoning. Given the results I have just described, we can
safely say that we understand this kind of reasoning; we know how it works
and what you can do with it. A general proof theoretic goal is to study
other theories that represent interesting parts of mathematical reasoning,
and to understand them as well as we understand arithmetic.

Ordinal analysis has proved to be a very useful tool in this pursuit: it
gives us a way of determining what a given theory can do, and how it can
do it; what it can't do, and why it can't. It also gives us a nice picture
of how abstract assumption about the infinite can have a bearing on the
realm of the finite. I've already discussed arithmetic, with its ordinal
epsilon_0. A fragment of arithmetic reasoning has been identified as
"finitary" (and arguably captures Hilbert's informal use of the term);
this will take you up to the ordinal omega^omega. In the other direction,
proof theorists have classified a broader class of mathematical reasoning
as "predicative". Roughly speaking, if you are a predicativist, you take
the natural numbers as a given totality, but not its power set. In filling
out the mathematical universe, we start with certain sets of natural
numbers, and use them to define more, repeating this ad infinitum; so the
universe of sets grows upwards, in a neverending process. Once again, we
have a characteristic ordinal, Gamma_0, which is obtained by iterating the
Veblen fixed-point operation from below. 

In contrast, an impredicative belief in the totality of sets of natural
numbers is tantamount to the acceptance of an uncountable cardinal, which
has simple reflecting properties. Once again, we have proof theoretic
ordinals that characterize the simplest forms of impredicativity, with
"collapsing" properties that serve as paradigms of these reflection
principles. Stronger axioms allow for snazzier kinds of transfinite
iteration and reflection; thanks to recent work by Rathjen and Arai, we
have ordinals that help clarify these processes as well.

Of course, ordinal analysis is well supplemented by other methods; the
more ways we have of understanding a theory, the better. I find Harvey's
recent work extremely interesting; using finitary combinatorial principles
to construct models of large cardinals helps us understand these
cardinals, as well as their bearing on the finite. Will these results, as
Harvey suggests, revolutionize mathematics, and change the way we think
about the infinite? For the moment I'd prefer to withhold judgement; but
even if they don't, there are still lots of interesting ideas in the work.

Incidentally, it is also worthwhile to go the other direction and study
very weak theories, which, in Razborov's words, embody "feasible reasoning
about feasible objects." There is still much to do in the field of bounded
arithmetic.

So far, I have tried to respond to Steve's question by justifying proof
theory relative to foundational goals. Of course, this begs another
question: why study foundations?

Mathematicians tend to justify pure research on two counts:

1) It is interesting: the questions are natural, the theories have an
internal coherence and a satisfying elegance.

2) It is useful: though often not directly applicable, pure mathematics
develops concepts, methods, and modes of thought that provide a powerful
and general framework for more applied pursuits.

Why is foundational research interesting? Of course, "interesting" is in
the eye of the beholder. But many of us are simply fascinated by
mathematics, a profound and mysterious endeavor. If you are held in thrall
by clever mathematical arguments and talk of the infinite, it is only
natural to try to understand how the arguments work, and what assumptions
we make about the infinite.

How might it be useful? One can look for "applications" outright;
applications to mathematics; or applications to philosophy. For
concreteness, I will focus on proof theory as an example; but one can make
similar cases for other kinds of foundational research.

Proof theory is predicated on the assumption that one can model aspects of
human reasoning in a formal, syntactic way. As a result, it isn't
surprising that proof-theoretic ideas have come up in artificial
intelligence, automated reasoning, logic programming, expert systems,
databases, and computer-aided verification; type theory and the
constructive propositions-as-types interpretation form a basis for
functional programming. I am not claiming that these pursuits are part of
proof theory, or even spinoffs thereof; only that the pure research,
without concern for applications, has facilitated more applied
developments. As such, it seems to me that proof theory has as much claim
to indirect "usefulness" as any branch of pure mathematics.

One can look for applications to mathematics in a number of different
forms. At the most basic level, foundational stances affect the way we
think about mathematics, the way we present it in our writings, and the
way we teach it to students. It also influences the issues we deem
important and choose to pursue. Hilbert's axiomatic method was as much a
way of doing mathematics as it was a research program, and particular
axiomatic foundations have influenced mathematical style and terminology. 

Foundational research can also raise (and answer) interesting mathematical
questions. For example, in proof theory, one can point to combinatorial
independences like the Paris-Harrington theorem and Friedman's
finitizations of Kruskal's theorem, which can be considered interesting
combinatorial theorems in their own right. Of course, one might take proof
theory to be good mathematics in and of itself; to many of us, notation
systems, infinitary trees, higher-type functionals, and so on are
interesting mathematical objects.

Such research can sometimes provide tools to answer mathematical questions
in other fields. In the case of proof theory, I wouldn't push this too
hard: e.g. Feferman has given Kreisel's "unwinding" program a mixed
evaluation. But Kohlenbach has been using proof-theoretic methods to
extract explicit bounds from proofs in numerical analysis. Insofar as the
results are useful to analysts, this strikes me as an interesting and
useful application.

Finally, as far as philosophical applications, it is worthwhile to note
that Hilbert and Bernays expressly felt that the primary merit of the
proof-theoretic approach lay in its ability to replace vague
epistemological questions with precise mathematical ones. Even in
situations where some kind of philosophical interpretation is unaviodable,
the mathematical analysis can provide a measure of precision and clarity.
For example, thanks to proof theory, we have a precise working definition
of what it means for an argument to be predicative;, and telling
formalizations of constructive reasoning. The kinds of results I described
above provide solid information that can help us evaluate various
philosophical stances in mathematics, like logicism, predicativism,
constructivism, or structuralism.

Having been long-winded in extolling the merits of my field, let me temper
the praise with a discussion of the inherent limitations. 

I have stated that the first part of the proof-theoretic approach involves
using formal systems to characterize various aspects of mathematical
activity. Set theorists may feel that proof theory is too conservative in
this regard, since the emphasis is on finding *minimal* proof systems,
rather more broad and powerful theories. This kind of parsimony is
remeniscent of the drunkard looking for his keys under the streetlamp: we
study the weaker systems because these are the ones we can get a handle on
constructively. If this is not your primary goal, it can be much more
interesting to consider strong principles that are mathematically
compelling.

The point is valid: proof theory and set theory address similar issues
with different attitudes and concerns, and each of these approaches yields
valuable insights. Furthermore, the ground between the two fields is
beginning to diminish, as proof theorists use ideas from the study of
large cardinals to analyze subsystems of second-order arithmetic, and
Friedman pushes his combinatorial independences up the large cardinal
hierarchy.

Many category theorists, on the other hand, may feel that proof theorists
are missing the point entirely. Since the Cantor-Dedekind revolution,
mathematics has had a structural character that is not well modeled by
tradional axiomatic frameworks. From the set-theoretic point of view,
first we define the natural numbers, and then we show that they have some
basic properties; finally, we show that these properties characterize the
structure uniquely, up to isomorphism. To the category theorist, this
stands the true order of things on its head: what is most important about
the natural numbers are their structural properties, and not their
(somewhat arbitrary) identification with certain sets. In other words,
set-theoretic foundations are too obsessed with ontology; rather than
explaining what mathematical objects *are*, it is much more telling to
give an informative account of the structural properties that
mathematicians actually use.

This criticism is also valid. Of course, a complete picture of
mathematical practice must recognize that it has *both* structural and
ontological components. Historically, we had particular examples of groups
and fields before we had the abstract characterizations; but the abstract
characterizations were telling, and led us to look for more examples. In
general, abstract structural characterizations are always accompanied by
concrete examples; and "constructing" further examples often leads to new
abstractions. Taken alone, neither the ontological nor the structural
account tells the whole story; but taken together, they complement each
other nicely. 

Finally, traditional forms of foundationalism have come under attack by a
number of philosophers and mathematicians. People like Lakatos, Kitcher,
Putnam, Tymoczko, Barwise, Putnam, Hersch, Manders, and many others have
suggested that the axiomatic approach is a misguided search for absolutes
that neglects some of the most interesting aspects of mathematical
activity. Mathematics is a distinctly human creative activity, and so it
is impossible to understand mathematics without appreciating the social,
historical, and cognitive elements behind it. In other words, we have to
move beyond the over-idealized model that the axiomatic approach has to
offer, and pay attention to what *really* goes on when we do mathematics.

At times, this debate becomes bitter. While the new guard proclaims that
the old foundationalism is dead, the old guard banishes the new research
programs to the realm of psychology, anthropology, theology, or just
outright flakiness. This friction is both unfortunate and unnecessary; one
can, at the same time, recognize the great strides made in mathematical
logic over the last century, while still maintaining that there are
additional aspects of mathematics that are worthy of sustained inquiry. I,
for one, would welcome an account of mathematical proof that explains why
some expositions are more explanatory than others; an account of meaning
that shows how mathematical concepts and notation can evolve, and yet
still denote the same structures; and account of rationality that explains
how we have come to accept the axioms and forms of argument that we do; an
account of what makes a certain classical theory "different" from a
constructive one, even though in principle we can interpret one in the
other; an account of what it means for a number-theoretic proof to "use"
analytic methods, even though we know that ultimately the whole thing can
be couched in the language of pure set theory; a deeper analysis of the
way the structural and ontological components of a mathematical theory
interact; an account of mathematical reasoning that includes heuristic
aspects. All of these things would supplement the traditional picture of
mathematics, without necessarily replacing it.

I have depicted the foundational enterprise as trying to give an
informative and coherent account of mathematical activity. It is unlikely
that any one approach will hold all the answers; we should welcome any
approach that can shed light on the subject. 

An analogy might help me get the point across. If you ever take a trip to
India, you will find it well worth your while to visit the Taj Mahal.
Guidebooks will tell you to spend an entire day in Agra, so that you can
admire the structure from many different angles and at different times of
day; they will even encourage you to go back and view it in different
seasons if possible. After all, the Taj Mahal is a complex and beautiful
structure, with different faces and moods that come out under different
kinds of light.

Mathematics is like that, a many-splendored thing that never ceases to 
captivate us with its power and elegance. We need to see it under many
different lights, and learn to appreciate its various personalities.
Anyone who tells you that they hold the one "true" picture of mathematics
simply fails to appreciate the depth and richness of the subject.


Jeremy Avigad
Assistant Professor of Philosophy
Carnegie Mellon University
e-mail: avigad+ at cmu.edu
http://macduff.andrew.cmu.edu