Sorry for the radio silence; I’ve been under the weather lately.
Is there any major theorem in mathematics drier than Gentzen’s cut elimination theorem. I feel guilty for picking on proof theory, since it is an undeservedly unfashionable area of mathematics (it’s probably better known by computer scientists than mathematicians at this point). I feel guilty for picking on the cut elimination theorem in particular, since it’s an important ingredient in the proof that Goodstein’s theorem is independent of Peano arithmetic, which is one of my favorite theorems. But, I had to read the statement of the theorem forty-nine times before I got what it was trying to say. I have yet to make it all the way through the proof before blacking out.
I was trying to think of a theorem in a more-fashionable area of mathematics that is particularly dry. The best I could come up with the Riemann-Roch theorem (for curves). I know what it says. I know what it’s good for. I just can’t bring myself to like it.
“I feel guilty for picking on Goodstein’s theorem is independent of Peano arithmetic”
I think you must have mistyped this, because it doesn’t mean anything in English. Since your blog is usually a model of good communication, I’ve been trying to identify the missing words, but without success. Help!
The proof may be dry, but its consequences are far-reaching!
For a less dry take on it, check out Girard’s Proofs and Types, and also his original paper on Linear Logic (Theoretical Computer Science, 1987). Perhaps it’s the “syntactic bureaucracy” (to imitate Girard’s idiom) of the proof that is offensive to many.
Joseph, I’m pretty sure there’s a malformed link in there somewhere, since if you click on that one you get a bunch of garbage following the regular URL.
I followed the first part of the first wikipedia link, and then an internal link to find:
http://en.wikipedia.org/wiki/Self-verifying_theories
whose non-web citations include the cut-free stuff as:
Willard, D., 2002. “How to Extend the Semantic Tableaux and Cut-Free Versions of the Second Incompleteness Theorem to Robinson’s Arithmetic Q” . Journal of Symbolic Logic 67:465—496.
Joseph, the missing phrase (the culprit is a missing quote character… I happen to do this a lot of times, the trouble of digiting by hand) is
I feel guilty for picking on proof theory, since it is an undeservedly unfashionable area of mathematics (it’s probably better known by computer scientists than mathematicians at this point). I feel guilty for picking on the cut elimination theorem in particular, since it’s an important ingredient in the proof that Goodstein’s theorem is independent of Peano arithmetic, which is one of my favorite theorems. But, I had to read the statement of the theorem forty-nine times before I got what it was trying to say. I have yet to make it all the way through the proof before blacking out.
I’m confused. Cut elimination has a very simple statement that’s short, simple and to the point. The proof might be on the dry side. I’ve not bothered looking at it as I can imagine it’s essentially the same as ‘inlining’ functions in a compiler and that’s a boringly mechanical process. But the statement seems pretty snappy to me.
Sorry about that, Joseph. Sigfpe was right: one of my URLs was malformed, which messed everything else up.
In the wikipedia entry for Cut-elimination-theorem we read that the cut rule is:
“(1) (A, B, . . .) |- C
and
(2) C |- (D, E, . . .)
allows one to infer
(3) (A, B, . . .) |- (D, E, . . .) ”
In fact, the cut rule is more general than this, since the unstated premisses in (1) (denoted by “. . .”) do not need to be identical to the unstated consequences in (2) (denoted also by “. . .”).
I find descriptions of the sequent calculus also dry. Once you have that, the statement of cut elimination is short. I don’t find it to the point because the reason someone would care is not really evident. Pretty much I rely entirely on the analogy with inlining functions to see what it means.
How about the Caratheodory extension theorem (in beginners’ measure thory)?
Admittedly I haven’t tried to look at it for over five years now, it might have developed more flavour since… It always seemed to me one of those results you were glad was true, but hoped no one would ask you to prove (or enthuse about).
Maybe I’m just sick, but I was really excited by the sequent calculus when I first learned it. The idea that you could nail down a proof system for logic in such a small number of (once you get the notation) simple rules was a revelation.
The (meta)proofs do tend to get long and tedious sometimes, since they tend to proceed by cases, and you usually get the idea on the first case, but someone had to show that it works for the other cases too. If I’m confident I’ve been convinced, I usually skip over some detail, except for the odd edge case or tricky bit.
If you didn’t enjoy Gentzen, I’d recommend you don’t read Prawitz.
Yes, I too found Gentzen sequent calculus and cut elimination a revelation. My own involvement in this area was through its applications to categorical coherence problems, where sequent deductions can be used to present the morphisms in freely generated categories-with-structure (e.g., free cartesian closed categories or free typed lambda calculi, free symmetric monoidal closed categories, free *-autonomous categories [cf. linear logic]). The basic insight, due to Lambek, is that cut elimination is the sine qua non for developing algorithms that decide equality in such free structures (”word problems” for categorical structures, aka categorical coherence problems).
In fact, this was precisely the subject of my PhD dissertation!
[Note: this comment was submitted a couple of days ago awaiting moderation, because evidently reCaptcha caught me making a mistake in those two words I'm supposed to type below. I took the liberty of making a few edits.]
walt,
Did you read my rant about cut elimination? http://sigfpe.blogspot.com/2006/02/cut-rule-and-reading-seminars.html
I found the responses I got very helpful.
I have never used any of the techniques listed but they all sound like good ideas that I will use in my geometry class. They sound so complex but I will get around to it.
[...] Mathematica Eliminate Cut Elimination Theorems “Is there any major theorem in mathematics drier than Gentzen’s cut elimination [...]