Monday , September 28 2020

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



Gentzen’s rules for natural deduction

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.

Source: Gerhard Gentzen, “ Untersuchungen über das logische Schließen I ”, pp. – Mathematische Zeitschrift . Springer, . The display above appears on page 210

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

[Other articles in category /math/logic] permanent link


Read More

About admin

Check Also

The Universe of Discourse: Another use for strace (isatty), Hacker News

The Universe of Discourse: Another use for strace (isatty), Hacker News

Another use for strace (isatty) (This is a followup to an earlier article describing an interesting use of strace.) A while back I was writing a talk about Unix internals and I wanted to discuss how the ls command does a different display when talking to a terminal than otherwise: ls to a terminal ls…

Leave a Reply

Your email address will not be published. Required fields are marked *