The Universe of Discourse: Gentzen's rules for natural deduction, Hacker News

is Gerhard Gentzen’s original statement. of the rules of Natural Deduction (“ein Kalkül für‘ natürliche ’, intuitionistische Herleitungen”):

Natural deduction looks pretty much exactly the same as it does today, although the symbols are a little different. But only a little! Gentzen has not yet invented !! land !! for logical and, and is still using !! & !!. But he has invented !! forall !!. The style of the !! lnot !! symbol is a little different from what we use now, and he has that tent thingy !! ⋏ !! where we would now use !! bot !!. I suppose !! ⋏ !! Did not catch on because it looks too much like !! land !!. (He similarly used !! ⋎ !! to mean !! top !!, but as usual, that doesn’t appear in the deduction rules.)

We still use Gentzen’s system for naming the rules. The notations “UE” and “OB” for example, stand for “und-Einführung” and “oder-Beseitigung”, which mean “and-introduction” and “or-elimination”.

Gentzen says (footnote 4, page 186) that he got the !! lor, supset, exists !! signs from Russell, but he did not want to use Russell’s signs !! cdot, equiv, sim, () !! because they already had other meanings in mathematics. He took the !! & !! from Hilbert, but Gentzen disliked his other symbols. Gentzen objected especially to the “Uncomfortable” overbar that Hilbert used to indicate negation (“[Es] stellt eine Abweichung von der linearen Anordnung der Zeichen dar ”). He attributes his symbols for logical equivalence (!! supset subset !!) and negation to Heyting, and explains that his new !! forall !! symbol is analogous to !! exists !!. I find it remarkable how quickly this caught on. Gentzen also later replaced !! & !! with !! land !!. Of the rest, the only one that did stick was !! supset subset !! in place of !! equiv !!. But !! equiv !! is much less important than the others, being merely an abbreviation.

Gentzen died at age 90, a casualty of the World War.

[ Addendum 20200214: Thanks to Andreas Fuchs for correcting my German grammar. ]

What do you think?

GIPHY App Key not set. Please check settings