Der Hauptsatz
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
Schnittbezeichnete 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.)
Comments
I would say that the practice of letter spacing isn't completely unknown. You occasionally see it in titles of things. However, the way it's used tends to evoke a sort of feeling about the text and not simply emphasis as in the German usage.
Personally, I think letter spacing actually brings more emphasis to a word than italics. (I used to use it myself in some of my more esoteric days.) After all, white space is perhaps the most important aspect aspect of graphic design, typography, web design, etc.
Posted by: Sean | September 4, 2008 11:23 PM
I find letter-spacing, in text, pretty subtle: My eye doesn't really fix on it. Word-spacing changes anyway in full-justified text—and sometimes letter-spacing, too—so it doesn't "read," to me.
People use letter-spacing in English, in logos and the like, but isn't it more a matter of being stylish, rather than using it for emphasis? I don't think I've ever seen it in text, except perhaps in truly experimental places.
Posted by: Ezra | September 5, 2008 12:23 PM
Do you find this s u b t l e? If I space out words like e m p h a s i s, what's your impression?
As for full-justified text, it occasionally screws with my senses for exactly that reason. I've never really liked it.
Posted by: Sean | September 5, 2008 10:45 PM
It's not so subtle when you call attention to it as a technique!
Seriously, though, I love italics. The different letter shapes make them stick out pretty well.
Anyways, I dig that the Germans had another way of doing emphasis, just for the historical-variety angle.
Posted by: Ezra | September 10, 2008 1:08 PM