"What's wrong with Tonk(?)" (Roy T. Cook)

JPL (2005)34:217-226, こちらから入手可能。
本日話題になった論文。有名なBelnapの "Tonk" は、以下のようなものです。二座の論理結合子 Tonk  \otimes は、

  • 導入:任意の B について、Aから  A\otimes B が導入可能
  • 除去: A\otimes Bから B が導出可能

Tonkは、ダメットの論理結合子の導入ルールの要請を満たしながら、一方で(古典論理上で)体系を自明化する(矛盾を招く)ことが知られています・・・そりゃ、Tonk 導入→除去を行えば、任意の論理式が証明できるのだから、当たり前と言えば当たり前。
しかし、これは実は当たり前ではなかった!Cookが示したことは、 relevant logic のある体系では、Tonkは非自明なモデルを持つ(つまり関係論理の意味で矛盾を導かない)ということで、すなわち、Tonkを論理結合子として持つ有意味な論理体系が存在すると言うことです。この体系は、4値論理の真理関数をrelationにすることで得られ、意味論から論理が定義されています。
本日話題になったのは、このCookの体系は本当に「論理」なのか、ということです。論理学の研究対象になっていると言う意味で、もちろんこの体系は論理と言えます(そして、この種の体系を論理の仲間から除外することは、関係論理と矛盾許容論理の大きな部分を論理学から追放することになるでしょう)。しかし、通常の「論理」に関する哲学者の要求は、Tonkを許すことに抵抗を感じます。その意味で、論理学者と哲学者の間で食い違いがあるとすれば、何が食い違っているのかが明確化されなければならないのでしょう。