証明力が拡張された適切さの論理体系ER

概要

論文の詳細を見る
論理の主たる目的は, 人間の行なう演繹的な推論を形式化することである。しかし, 古典論理における含意「ならば」は, 日常利用する「ならば」とは, 違和を感じる箇所もある。例えば, 古典論理では, 「2+3=5」が真であることから, 「雪は白いならば, 2+3=5」が真となる。しかし, このような推論は, 奇異に感じられる。古典論理の含意が持つこのような違和感は次のように3つに分類される。1. 関連性の違和感 A→(B→A), 2. 恒真性の違和感 (A∧¬A)→B, A→(B∨¬B), 3. 偶然性の違和感 A→((A→B)→B)。適切さの論理は, これらの違和感を除去することを目的として研究されてきた。Lewisによる関連性の違和感が除去された厳密含意の提案に始まり, 多くの適切さの論理の体系が提案されている。代表的な体系としては, ChurchやMohによる, 関連性と恒真性の違和感が除去された論理体系Rや, Ackennannによる, すべての違和感が除去された論理体系Eなどがある。関連性・恒真性の違和感は強い違和感とみなされ, ほとんどの体系で, これらは除去されている。一方, 適切さの論理では, 体系が弱いという問題がある。例えば, 自然演繹における推論規則Disjunctive syllogism (DS)が許されない。[numerical formula]この推論規則が認められない理由は, 以下のように(A∨¬A)+Bが証明可能となるためである。[numerical formula][5]では, DSが問題のある規則と見なされ, 適切さの論理では, この推論規則は除去されている。また, 違和感を含んでいない以下の式が, 適切さの論理では定理ではない。1. A→(B→(A∧B)), 2. A→(A∧(B∨¬B))。適切さの論理では, 1.が定理である場合, A→(B→A)が定理となり, また, 2.が定理である場合, A→(B∨¬B)が定理となるため, これら2つの式は定理とはならない。このように, 適切さの論理では, 違和感を除去するために, 結果として, 定理となることが自然であると考えられる式が定理とはならず, また, 自然な推論規則が成り立たない。本稿では, 関連性・恒真性の違和感が除去されており, 体系Rよりも強い論理体系ERを提案する。ERは, [4]に示されているsequentによる自然演繹の体系として与えられ, 各推論規則では, 式の属性が利用される。この属性は, 証明を制御し, 違和感を含む式の推論を防ぐために利用される。また, 属性を利用する点からみると, ERは, Labelled deductive systemの一種であるといえる。
1997-09-24

証明力が拡張された適切さの論理体系ER

スポンサーリンク

概要

著者

関連論文

スポンサーリンク