直観主義や直観主義論理そのものには特に思い入れはない。ブラウワーの文章を読んだ覚えはないし、ダメットの文章もほとんど読んでいない。ポアンカレの文章も。でも、もう少し日の目を浴びても良いと思う(それとも知らないだけで、けっこう浴びているのだろうか)。
直観主義論理と自然演繹
自然演繹による証明では、何かある論理式を仮定するところから証明が始まる。仮定された論理式から別の論理式を導き、新しく導かれた論理式からまた別の論理式を導いていく。証明で立てられる仮定は一つとは限らない(複数の仮定を立てないといけない場合の方がたぶん多い)。また証明の途中で、立てていた仮定が取り除かれる場合もある(そのような証明規則が用意されている)。
直観主義論理に対する自然演繹では、論理積・論理和・含意・否定・矛盾の各論理記号について、導入則と除去則と呼ばれる演繹規則を持っている(否定と矛盾についてはちょっと特殊な面がある)。古典論理の場合は、これにさらに追加の演繹規則(または公理)がある。
直観主義論理では、この導入則・除去則の役割が古典論理の場合よりもきれいに説明することができるという特長がある。
導入則と除去則の説明
直観主義論理の自然演繹では、導入則がその記号の意味を説明していると見なすことができる。一方、除去則は導入則が説明する意味から導かれる。
論理積
論理積の導入則は、AとBからA∧Bを導出してよいというもの。証明図では次のようになる。
(∧の導入則)
そしてこの規則が「∧」という記号の意味を説明しているとみなせる。つまり
「A∧B」というのは、AとBの両方が証明できることをあらわしている。
とみなすことができる。
しかし導入則が論理積の意味を説明しているといっても、論理積について他の規則はいらないというわけではない。論理積の記号は導入則を使った場合にのみで登場するのではなく、論理積を含んだ式を仮定として置いた場合でも登場する。したがって、論理積が導入済みの式に対する規則がいる。
そこで、A∧BはAとBの両方が証明できることをあらわしているのだから、
(∧の除去則)
というふたつの規則があっても良いだろう。この規則はA∧Bの意味「AとBの両方が証明できる」によって正当化されている、と考えることもできる(A∧Bの代わりにAの証明とBの証明があるとみなせば、この規則が成り立つので)。
また、除去則によって論理積記号をいったん消したあと、再び元の式を復活させることができる。
二つある除去則のうちどちらか一方しか認められていなかったら、元の式を復活させることはできない。つまり、この除去則には
- 導入則によって正当化されている。
- いったん記号を除去しても、導入則を使って元の式を再現できるようになっている。
という性質がある。
含意
Aを仮定してBが導けたとき、つまり
となったとき、Aを仮定から除いた上でを導いてよい。これを証明図では
(→の導入則)
と書く。四角カッコで囲まれた論理式は仮定から除かれたことを表している。ここで添字の数字は、証明のどの部分でその仮定を除いたのかを示している。この証明図には明示されていないけど、A以外に他の仮定があってもかまわない(それらの仮定はそのまま残っている)。また同じ仮定は一度に消せる。例えば次のように。
仮定から除いたことを論理式の上に横線を引いて示す書き方をする場合もある。
論理積のときと同様、この導入則が→の意味を説明しているとみなせる。
「A→B」というのは、Aの証明があったときにBの証明ができることをあらわす。
A→Bの意味に「Aの証明があったときに」とあるので、Aの証明を持ってくると除去則ができる。
(→の除去則)
この規則も、導入則が与える意味によって正当化されているとみなすことができる(A→Bの代わりに、Aの仮定があってBで終わる証明があると考える)。
そして論理積の場合と同様に、含意記号をいったん消して再び復活させることができる。
論理和
論理和の導入則は次のもの。
(∨の導入則)
よって
「A∨B」というのは、AかBのどちらかは証明できるということをあらわしている。
と考えることができる。
∨の除去則は少し面倒。A∨Bから何かを導きたいのだけど、Aを導くわけにもBを導くわけにもいかない。でもAからもBからも共通の結論が出せるなら、それをA∨Bから導くことは正当化される。
(∨の除去則)
除去則でいったん記号を消して導入則で復活させるというのも、論理和の場合はわかりにくい。次のようになるのだけど、一度消しているように見えないかもしれない。
矛盾
普通、矛盾というのは否定によって説明される。たとえば「矛盾とは、何かとその否定が両方成り立つことだ」というように。でも自然演繹では、否定よりも矛盾が基本的な役割を果たす。これはいくらか不自然な感じもするけど、否定よりも矛盾のほうが証明との結びつきが強いからだと考えて納得しておく。
それで矛盾に対する推論規則だけど、矛盾の導入規則はない。積極的にない。したがって導入規則に基づいた矛盾の意味の説明はこうなる。
「
」というのは、決して証明されないことをあらわしている。
ただし、決して証明されないといっても、何かを仮定すればそれから証明されることは普通にある(例えばを仮定した場合、簡単に
は導かれる)。
次は、矛盾の除去則をどうするかが問題になる。矛盾についての導入則がないので、どんな強力な除去則を与えても矛盾記号をいったん消したらそれを復活させることはできない。
そこで考えられる限りでもっとも強力な規則を考える。つまり「矛盾からは何を導いても良い」。
(
規則)
この規則は一応記号を除去しているけれど、別の論理式を導入しているので除去則とは呼ばないことにする。
この規則を矛盾の意味から正当化するとこうなる。矛盾は、決して証明されないこと、もっとも証明されにくいことをあらわしている、それが証明されてしまうなら他の何が証明できても良い。他の除去則の正当化ほどうまくいっていない気もするけど、一応これで正当化できたことにする。
否定
矛盾の意味づけができたので、これに基づいて否定に対する意味づけと推論規則を与えることができる。Aの否定¬Aは
¬A≡A→
と定義することができる。あるいは次のような導入則・除去則を与えても良い。
(¬の導入則)
(¬の除去則)
述語論理の場合
面倒になったので述語論理の場合(∀と∃についての推論規則)は省略。
まとめ
以上で、直観主義論理についての規則は全て出た。
直観主義論理に対する自然演繹は、各論理記号について導入則と除去則があり、しかも導入則が記号の意味を説明し、それによって除去則が正当化されるという綺麗な関係が成り立っている。
古典論理の場合、この関係が崩れてしまう。古典論理の場合、以上の推論規則に加え、別の推論規則(あるいは公理)が加わる。付け加え方はいろいろ可能で、例えば二重否定除去則を付け加えてもいいし、パースの規則でもいい。
そのうちのひとつが排中律で、次の形の式を仮定無しで置けるという規則。
(排中律)
仮定ではないことがわかるように、ここでは式の上に横線を引いた。
(追記:公理や推論規則を追加する以外にも直観主義論理の「自然さ」(3)で与えたような、結論として複数の論理式を置いてよいことにするというやり方もある)
古典論理になると、直観主義論理で成り立っていた関係が成り立たなくなる。直観主義論理ではA∨BはAかBのどちらかは証明できるということをあらわしていた。でも古典論理ではAも¬Aも証明できない場合でもA∨¬Aは証明できることになり、導入則が記号の意味を説明するという関係が成り立たなくなってしまう。
古典論理を知っている立場から見れば、排中律その他を導入して古典論理の体系にする理由は充分にある。ド・モルガンの法則などを使った式変形がやりやすいし意味論がすごく簡単になる。でも自然演繹の体系だけを見ると、直観主義論理の部分で調和が取れているので、わざわざその調和を乱す規則や公理を追加する動機があまりないように見える。
直観主義論理の方が自然だと見ることだってできる。という強引な締め。
