A Measure of Inference in Classical and Intuitionistic Logics
By
Mamoru Kaneko and Nobu-Yuki Suzuki
要 約
本論文において推論・証明の複雑性を議論する。計算の複雑性は、問題の可算集合に適用するアルゴリズムがその実行にようする時間の大き さとして定義される。しかし、これは、特定のひとつの問題(シークエント)に必要な推論・証明の大きさを論じることを目的としていない。 特定のひとつの問題(シークエント)に必要な推論・証明の大きさを評価する試みは、論理学だけでなく、ゲーム理論・経済学(特に限定合理 性の問題)などからも重要である。本論文では、古典論論理と直観主義論理のシークエント計算の体系で、与えられたひとつのシークエントが 必要とする最小の証明の大きさ(証明の幅の意味で)を定義する。そして、具体的にその値を求める方法を与え、様々なシークエントに適用 し、最小の証明についての考察を行う。また、ゲーム理論的問題への応用、矛盾命題への応用を議論する。