Natural Deduction と Sequent Calculus の先駆者としての Peirce


  • Geraldine Brady  From Peirce to Skolem: A Neglected Chapter in the History of Logic, Amsterdam, North-Holland/Elsevier, Studies in the History and Philosophy of Mathematics, vol. 4, 2000


A third theory first introduced by Peirce[, which is one of his contributions to logic,] is his system of impricative propositional logic. This theory is developed in the first two chapters of Peirce's 1880 paper, “On the algebra of logic”, in which he determines the relationship between implication and deduction, deriving implications from deductions and conversely. This is a very close informal predecessor to “natural deduction systems” introduced by Dag Prawitz (1965). Yves Girard has interpreted the Gentzen sequent systems as simply a set of rules for manipulating natural deductions, and in this sense Peirce's system is a predecessor of the sequent calculus*1.

この引用文には註がついていて、そこにはF.William LawvereがPeirceのideaはclosed and enriched categoriesの先駆であるとの話も注意されている。Peirceがどのような理論・アイデアの先駆者となっているかをすべて逐一数え出したら切りがなさそうな勢いである。ものすごいお人ですね。あらためて思います。実にversatileだ。呆れてしまう…、と言ったら失礼かな?

*1:Brady, p.10.