Natural Deduction
摘要
Gentzen’s natural deduction calculi are presented as a realization of an ideal first articulated by David Hilbert, according to which the meaning of a logical particle can be specified in terms of the characteristic inference patterns it governs. Gentzen’s distinctive approach to this program is analyzed with the algebraic notion of a universal property. On the “relational definition” scheme that results, each logical operator is characterized by a pair of rules that together specify a universal property. Gentzen’s remarks about essentially classical inferences like the double negation rule can be interpreted as the observation that classical reasoning resists relational characterization. Dually, Gödel’s observations about intuitionistic logic can be interpreted as the failure to account for constructive reasoning on the alternative scheme of “essential definition.” The special status of ex falso quodlibet, disjunctive syllogism, and the identity predicate are analyzed on the relational scheme.