TETRA'S MATH

数学と数学教育
<< 直観主義論理が認めないもの | main | 直観主義論理では成り立たない定理 >>

直観主義論理の公理系

 というわけで、野矢茂樹『論理学』から、直観主義の公理系をみてみたいと思います。命題論理の完全な公理系の「二重否定」が「否定除去」に変わります。

直観主義命題論理の公理系LIP----------------------

規則1[演繹規則DR]
 Aを仮定してBが導出されるとき,Aという仮定なしにA⊃Bを導出してよい

規則2[前件肯定式MP]
 A,A⊃BからBを導出してよい

規則3[背理法]
 A⊃(D∧¬D)から¬Aを導出してよい

規則4[否定除去]
 D∧¬Dからは任意のAを導出してよい

規則5[結合]
 A,BからA∧Bを導出してよい

規則6[分離]
 (1)A∧BからAを導出してよい
 (2)A∧BからBを導出してよい

規則7[∨入れ]
 (1)AからA∨Bを導出してよい
 (2)BからA∨Bを導出してよい

規則8[∨取り]
 A∨B、A⊃B、B⊃CからCを導出してよい

--------------------------------------------------

 「二重否定」というのは「¬¬AからAを導出してよい」というものであり、「¬¬Aが証明されたとすると、¬Aは証明されえないので、Aとしてよい」という考え方ですが、直観主義では後半の「¬Aは証明されえないので、Aとしてよい」の部分を認めません。¬AとAのどちらかであるとは考えないので。

 そして、否定除去型の背理法の場合、「¬Aと仮定したら矛盾が出たから¬(¬A)、だからA」という流れになり、最後で二重否定の考え方を使っているので、直観主義では認められないのだと思います。たぶん。

 なお、二重否定除去「¬¬A⊃A」は認められませんが、二重否定導入「A⊃¬¬A」の定理は成り立つそうです。

 また、直観主義論理の「否定除去」は「矛盾からは何を導出してもよい」といっているような規則で、ここで矛盾を拒否しているわけですが、従来の命題論理においては定理になっています。(でも古典論理の定理の証明で二重否定が使われているんですよぉ。なんか不思議。ひょっとすると二重否定なしの証明も可能なのかな? あるいは公理にしちゃったもんがち?)

 というわけで、公理としては「二重否定」よりも弱い「否定除去則」を取り入れているので、直観主義論理は古典論理の部分系ということになるようです。その結果、排中律を含むいくつかの定理が定理ではなくなります。

 そんなこんなで、排中律を認めないという立場から公理系の規則4が変わったのか、公理系の規則4を変えた結果、排中律が証明できなくなったのか、そこんところがいまひとつのみこめないのでした。

 でも、排中律を認めない態度も、二重否定を認めない態度も、否定除去型背理法を認めない態度も、根は同じであり、それが直観主義ということなのかもしれません。そういう態度のうちいちばんわかりやすく明確な争点となったのが「排中律」ということなのかもしれません。

(つづく)

論理学 | permalink
  

サイト内検索