In the comments to Programming Language and Logic Links, citylight asked for an example of what proof theory is good for. I wanted to sketch an example using Goodstein sequences.

Proving that Goodstein sequences always eventually go to zero requires transfinite induction up to the ordinal \epsilon_0. Gentzen proved, using transfinite induction up to \epsilon_0, that Peano arithmetic was consistent. By Godel’s second incompleteness theorem, not consistent system can prove its own consistency, so transfinite induction up to \epsilon_0 is not expressible in Peano arithmetic, and Goodstein’s theorem is independent of it.

More details can be found at Fast Growing Functions and Unprovable Theorems.

Ah thanks for that – yes I’ve seen that result elsewhere, very neat.

I was wondering more about mathematical uses for the kind proof theory that gets dirty with the syntax of proofs, normalisation results and so forth. It seems to me that most mathematical uses of logic don’t have much concern for the syntax of proofs. Once you have logical soundness and completeness, and you know the proof system is recursively enumerable, you cease to care about its syntax, or what its proofs look like. Infact, once you’ve proved Goedel’s results, it seems you may aswell forget about the proof theory altogether, and concern yourself only with the semantics of the language, as in model theory.

But, I wonder if there are any examples that would prove this suspicion wrong.

To continue the debate on that other post, things like this (the Goodstein result) demonstrate why mathematicians should care about foundations – if you’re struggling with a hard problem (P != NP for example) you’d rather like to know if it’s actually independent from the axioms you’re working with. It saves you wasting time trying to prove something from insufficient assumptions.

Gentzen’s proof uses proof normalization (cut elimination), so the Goodstein independence result is an example of getting dirty. It even gives you a model-theoretic result that is apparently not accessible to model theory itself: there must be a model of Peano arithmetic in which Goodstein’s theorem is false.

Oh right – interesting.

I’d obviously not looked at that in enough depth, I had presumed that Godel was the only proof theory it was using…