FOM: proof theory and foundations

[Colin McLarty]

        Jeremy's well thought post on proof theory includes two remarks I
would differ on:


>    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
>    traditional axiomatic frameworks.


        I don't know anyone who thinks proof theory entirely misses the
point of foundations. Category theory uses proof theoretic considerations,
for weak fragments of first order logic (what we call "low in the
heirarchy") for various mathematical purposes. And a lot of us find it
interesting for foundations that so much of category theory lives that
low--it is not only possible but most natural to axiomatize categorical set
theory (among many other things) in a logic so weak that every sentence in
it is trivially true in a universe with just one object and one arrow, plus
one first order axiom saying there exists a set with at least two different
elements. 

        A lot of classical proof theory about the strength of various
theories is interesting to me. It is not a pressing foundational concern to
me since in my heart I'm sure ZF plus measurable cardinals and a whole lot
more is consistent. But it is interesting to know what implies what. 

> In other words [category theorists may feel that]
>    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.

        But here I object that ZF set theory does not tell us what numbers
*are*, only what they *could be*. It tells us they could be the finite von
Neumann ordinals. Or again they could be the finite Wiener ordinals. They
could be any of infinitely many things. This "could be" has real uses, but I
don't think it teaches us the ontology of math. It teaches us more
articulate ways we *could choose* to understand math, but I think that the
direction math has actually gone since Dedekind and Cantor (long before ZF
set theory) urges a more structuralist understanding.

Colin