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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Natural Deduction

  • Curtis Franks

摘要

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.