Had a good time today puzzling over Gerhard Gentzen's 1934 paper, "Untersuchungen Ã¼ber das logische SchlieÃŸen. I." ("Investigations into logical reasoning"). I wanted to determine that this was really what I thought it was: the paper where he introduced cut-elimination and the subformula property, which I'm examining now in my research.
I was looking at the German version and I don't know anything about German. But Google Translate and the BeoLingus online DE-EN dictionary came to the rescue. (Phil tells me he has a translation, but where's the fun in that?)
The result was satisfying:
Eine nÃ¤here Untersuchung der besonderen Eigenschaften des natÃ¼rlich KalkÃ¼ls fÃ¼rte mich schlieÃŸlich zu einem sehr allgemeinen Satz, den ich im folgenden "Hauptsatz" nennen will. Der Hauptsatz besagt, dass sich jeder rein logische Beweis auf eine bestimmte, Ã¼brigens keineswegs eindeutige, Normalform bringen lÃ¤sst.
which I render,
A closer examination of the special properties of the natural calculus led me to a general theorem that I have called the `fundamental theorem'. The fundamental theorem says that any purely logical proof can be brought to a certain (incidentally, non-obvious) normal form.
And much later, after introducing the natural deduction calculi for classical (NK) and intuitionistic logic (NJ), as well as the respective sequent calculi (LJ and LK), we get to this understated result:
Hauptsatz: Jede LJ- bzw. LK-Herleitung lÃ¤ÃŸt sich in eine LJ- bzw. LK-Herleitung mit der gleichen Endsequenz umwandeln, in welcher die als
Schnitt bezeichnete SchluÃŸfigur nicht vorkommt.
Every LJ- (resp. LK-)derivation can convert to a LJ- (resp., LK-)derivation with the same end sequent, in which the rule called ``snip'' does not appear.
Instead of the usual name "cut," I've merrily translated the German "Schnitt" as "snip," because it pleases me--I like direct, etymological, native translations of this kind. (OED traces the English "snip" to Low German "schnipp," not terribly far off; "cut" has, of course, OE origin.)
(Sadly, I can't remember where I got the PDF of this original. The browsable online version linked above is from Gentzen's own alma mater, GÃ¶ttingen University.)
(Miscellanea: Fans of typographic history will appreciate the printer's use of letter spacing for emphasis, a practice unknown in English but apparently traditional in German, according to Wikipedia. It could be used roughly wherever we use italics in English.)