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

を初めの方を拾い読みしていると、興味深い記述が見られる。PeirceがPeanoよりかなり前に自然数論の公理を提出していたという話は、随分前に読んだことがあるが、次のようなことも事実だという。

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.