コラム 排中律と背理法

Last-modified: Wed, 15 Mar 2017 23:25:50 JST (1724d)
Top > コラム 排中律と背理法
述語論理へ戻る。

ここでは排中律と背理法の関係について説明します。まず、背理法には2種類あることに注意しましょう。1つは演繹規則の例(7)で言及した否定導入則または\( \neg \)導入則と呼ばれるもので、論理式\( \Phi \)について

\( \Phi \)を仮定すれば\( \perp \)を帰結できる」ということを仮定すれば\( \neg(\Phi) \)を帰結できる。

という演繹規則です。こちらは弱い背理法と呼ばれることもあります。

もう1つは否定除去則(negation elimination)または\( \neg \)除去則(\( \neg \)-elimination)と呼ばれるもので、論理式\( \Phi \)について

\( \neg(\Phi) \)を仮定すれば\( \perp \)を帰結できる」ということを仮定すれば\( \Phi \)を帰結できる。

という演繹規則です。こちらは強い背理法と呼ばれることもあります*1

弱い背理法と強い背理法の違いは、「仮定した論理式に\( \neg \)が加わるのか減るのかの違い」です。通常の演繹規則のうち強い背理法以外のみを使って命題の証明を記述する体系を直観主義論理またはNJと呼び、強い背理法も使って命題の証明を記述する体系とは明確に区別されます。ここでは後者をNJneと呼ぶことにしましょう。

またNJに公理として排中律を加えた体系を古典論理またはNKと呼びます。NJで証明が書ける命題は当然NJneやNKでも証明が書けますが、NJneやNKで証明が書けるからと言ってNJでも証明が書けるとは限らないことが知られています。つまり、強い背理法を許容するか否かで、または排中律を公理に課すか否かで、証明できる命題の範囲が変わってしまいます。

直感的には、NJでは一度付いてしまった\( \neg \)記号を直接減らす演繹規則が存在しません*2。このことに目を向けると、\( \neg \)を減らすような帰結を与える強い背理法を許容するNJneがNJより広い範囲の命題を証明できることは、極めて自然であると思います。

実際、弱い背理法を使って強い背理法と同じことができないか、試行錯誤してみましょう。「\( \neg(\Phi) \)を仮定して\( \perp \)が帰結できる」ということを仮定します。\( \neg(\Phi) \)に対して弱い背理法を使うことで、\( \neg(\neg(\Phi) ) \)が帰結されました。\( \neg(\neg(\Phi) ) \)は直感的には\( \Phi \)と同じもののようですが、証明を記号化した形式体系においては明確に異なる論理式です。\( \neg(\neg(\Phi) ) \)から\( \Phi \)を証明できないか、ということで更に\( \neg(\neg(\neg(\Phi) ) ) \)を仮定して矛盾を導いてみましょう。\( \neg(\neg(\neg(\Phi) ) ) \)を仮定すると\( \neg(\neg(\Phi) ) \)かつ\( \neg(\neg(\neg(\Phi) ) ) \)が帰結されてしまうので、矛盾記号\( \perp \)が帰結されます。つまり「\( \neg(\neg(\neg(\Phi) ) ) \)を仮定すると\( \perp \)が帰結される」ことが分かったので、弱い背理法から\( \neg(\neg(\neg(\neg(\Phi) ) ) ) \)が帰結されます。困ったことに、\( \Phi \)からどんどん離れていってしまいました。このように、弱い背理法をいかに繰り返しても、\( \neg \)の個数が増えるばかりで一向に\( \neg \)を外すことが出来ないのです。

しかしながら、\( \neg(\neg(\Phi) ) \)から\( \Phi \)が帰結できないのは不便であることも多いです。NJで証明できない以上、新たにそういう演繹規則を導入してみよう、と考えることは自然だと思います。

\( \neg(\neg(\Phi) ) \)を仮定すると\( \Phi \)が帰結できる。

NJでは許容されないこの演繹規則を、二重否定除去則(double negation elimination)または\( \neg \neg \)除去則(\( \neg \neg \)-elimination)と呼びます。NJに二重否定除去則を演繹規則として加えた体系を、ここではNJdneと呼ぶことにしましょう。

以上で、NJに新たな公理または演繹規則を加えた体系を3つ用意できました。

(1) NJに強い背理法を加えた体系NJne
(2) NJに排中律を加えた体系NK
(3) NJに二重否定除去則を加えた体系NJdne

それでは、これら3つの体系の関係を調べましょう。

定理1(強い背理法と排中律と二重否定除去則の等価性)
\( \Phi \)を論理式とする。この時、以下が成り立つ。
(1) NJneにおいて、\( (\Phi) \vee (\neg(\Phi) ) \)が帰結できる。
(2) NKにおいて、\( \neg(\neg(\Phi) ) \)を仮定すると\( \Phi \)が帰結できる。
(3) NJdneにおいて、「\( \neg(\Phi) \)を仮定すると\( \perp \)が帰結できる」ということを仮定すると\( \Phi \)が帰結できる。

証明

(1)を示す。強い背理法により\( (\Phi) \vee (\neg(\Phi) ) \)を帰結させる。\( \neg( (\Phi) \vee (\neg(\Phi) )) \)を仮定する。\( \Phi \)を仮定すると、\( \Phi \)演繹規則の例(3)を適用することにより\( (\Phi) \vee (\neg(\Phi) ) \)が帰結され、従って演繹規則の例(1)により\( (\Phi) \vee (\neg(\Phi) ) \)かつ\( \neg( (\Phi) \vee (\neg(\Phi) )) \)が帰結されるので、演繹規則の例(5)により矛盾記号\( \perp \)が帰結される。以上より「\( \Phi \)を仮定すると\( \perp \)が帰結される」ということが(\( \neg( (\Phi) \vee (\neg(\Phi) )) \)の仮定下で)示されたので、演繹規則の例(7)により\( \neg(\Phi) \)が(\( \neg( (\Phi) \vee (\neg(\Phi) )) \)の仮定下で)帰結される。\( \neg(\Phi) \)演繹規則の例(3)を適用することにより\( (\Phi) \vee (\neg(\Phi) ) \)が帰結され、従って演繹規則の例(1)により\( (\Phi) \vee (\neg(\Phi) ) \)かつ\( \neg( (\Phi) \vee (\neg(\Phi) )) \)が帰結されるので、演繹規則の例(5)により矛盾記号\( \perp \)が帰結される。以上より「\( \neg( (\Phi) \vee (\neg(\Phi) )) \)を仮定すると\( \perp \)が帰結される」ということが(何の仮定もなく)示されたので、強い背理法により\( (\Phi) \vee (\neg(\Phi) ) \)が帰結される。

(2)を示す。\( \neg(\neg(\Phi) ) \)を仮定する。排中律により\( (\Phi) \vee (\neg(\Phi) ) \)が帰結される。\( \Phi \)を仮定すると自明に\( \Phi \)が帰結される。\( \neg(\Phi) \)を仮定すると、演繹規則の例(1)により\( \neg(\Phi) \wedge \neg(\neg(\Phi) ) \)が帰結され、演繹規則の例(5)により矛盾記号\( \perp \)が帰結され、演繹規則の例(6)により\( \Phi \)が帰結される。以上より、「\( \Phi \)を仮定すると\( \Phi \)が帰結される」ということと「\( \neg(\Phi) \)を仮定すると\( \Phi \)が帰結される」ということの両方が示されたので、演繹規則の例(4)により\( \Phi \)が帰結される。

(3)を示す。「\( \neg(\Phi) \)を仮定すると\( \perp \)が帰結される」と仮定する。演繹規則の例(7)により\( \neg(\neg(\Phi) ) \)が帰結される。従って、二重否定除去則により\( \Phi \)が帰結される。

以上でNJneとNKとNJdneの3つの体系においてはどのような命題が証明できるかが同じであるということが分かりました。ただし証明できる論理式が同じであったとしても、論理式の「証明の構造」は変わってしまいますし、またNKにのみ公理という特別な扱いの論理式が規定されている点も重要です。雑な言い方では「排中律と強い背理法と二重否定除去則が同値である」と述べることもありますが、排中律は公理(仮定なく帰結できる命題)であることに対し、強い背理法と二重否定除去則は演繹規則(どの命題を仮定するとどの命題が帰結できるかの規定)ですので、排中律を加えるということは証明手段は増やさない代わりに証明せずに使って良い命題を増やすということになり、対して強い背理法や二重否定除去則を加えるということは証明せずに使って良い命題は増やさない代わりに証明手段を増やすということになります。すなわち証明できる命題を増やすためのアプローチが明確に異なっています。

Encyclopedia of \( P \)-adic Numbersでは排中律を公理に加えているため、NKで考えていることになります。強い背理法と排中律と二重否定除去則の等価性によって、命題がNKで証明できることとNJneやNJdneで証明できることは等価であるので、強い背理法も二重否定除去則も演繹規則に加えて使うことにします。

さて、強い背理法やある意味でそれに等価なものを用いなければ証明できない命題(つまりNJでは証明できない命題)がたくさん存在します。強い背理法に限らず、弱い背理法もまた多くの命題の証明に不可欠なものです。NJから弱い背理法を除いてしまった体系では、多くの否定命題、すなわち「~でない」という形の多くの命題は証明できなくなってしまいます。何故ならば、直感的にはNJにおいて弱い背理法以外の演繹規則では\( \neg \)を増やすことが出来ない*3からです。

また、否定命題は見た目が否定の形をしていないことがあるので注意が必要です。それは、否定を含む述語を定義に持つ用語が存在するからです。

例2(否定を含む述語を定義に持つ用語の例)
(1) ~は無理数*4である。
(2) ~と~は異なる*5

こういった否定命題を証明する上では、必ず議論のどこかで\( \neg \)記号を増やす必要があり、そのためには弱い背理法が必要になることがほとんどです*6


余談ですが、数学者やそれに準じる者の中にも、背理法を用いた証明を好まない人もいます*7。その程度は様々ですが、基本的には「背理法を用いずにも証明でき、かつ背理法を用いることによって簡便になるわけでもない命題を、背理法によって証明することはあまり良くない」という主張が多いように思います。「簡便になるか否か」や「良いか良くないか」は数学的な意味を持つ文ではなく主観的な裁量によるものですが、「背理法を用いずに証明できるか否か」は数学的な意味を持ちます。

さて、ここまでも何度か現れたように「この命題は背理法を用いずに証明できる」という言説や「この命題の証明には背理法が本質的に必要である」という言説を目にすることが多々あります。その際に気を付けることの1つは、話者の使う「背理法」という言葉がどのような意味で発せられているかです。強い背理法のみを背理法と呼ぶ人もいれば、弱い背理法と強い背理法の両方を(意図的にまたは無意識に)背理法と呼ぶ人もいますし、強い背理法とある意味で等価である排中律や二重否定除去則のような公理や演繹規則のことも含めて背理法と呼ぶ人もいます。

例えば強い背理法のみを背理法と呼ぶ人が「背理法を使わずに証明した」と述べている場合は弱い背理法や排中律や二重否定除去則を使っている可能性がありますし、弱い背理法も含めて背理法と呼ぶ人が「この命題を証明するためには背理法を避けることができない」と述べている場合は弱い背理法を使わないことも考慮している可能性があります。

しかしながら、しばしば「背理法」という言葉の多義性に注意することなく相異なる流儀間で意見の食い違いが生じることもあり、その不毛性は火を見るより明らかなものです。そういう状況に出くわしたら、なるべく早い段階で「今話題にしている背理法という言葉の意味は何か」を確認しておくことが望ましいでしょう*8




*1 強い背理法のみを指して背理法と呼ぶ流儀もあります。
*2 正確には、[[演繹規則の例(2)>述語論理#true]]で&mathjax{(\neg(\Phi) ) \wedge (\Psi)};から&mathjax{\Psi};を帰結させるように見掛け上の&mathjax{\neg};の数を減らすことが出来ますので、そういう「情報を落とす」ような&mathjax{\neg};の減らし方しかない、と述べた方が無難なところです。しかしながら情報とは何か、という話になりますので、あくまで直感的な話です。
*3 正確には、[[演繹規則の例(3)>述語論理#true]]で&mathjax{\Phi};から&mathjax{(\Phi) \vee (\neg(\Psi) )};を帰結させるように見掛け上の&mathjax{\neg};の数を増やすことが出来ますので、そういう「情報を増やさない」ような&mathjax{\neg};の増やし方しかない、と述べた方が無難なところです。しかしながら情報とは何か、という話になりますので、あくまで直感的な話です。
*4 「無理数である」の定義は「有理数でない」です。
*5 「異なる」の定義は「等しくない」です。
*6 ただし、形式体系での証明と違って口頭での証明はしばしば必要な議論をうっかり省略してしまうことがあり、弱い背理法を使っている部分を無意識に省略してしまってたために弱い背理法を使わずに済んだと錯覚してしまう場合があります。それは「弱い背理法を使わずに証明できた」のではなく、「弱い背理法を使って証明したものを省略した」もしくは「証明できなかった」ということです。
*7 cf. [[グレ妹/群城すず>参考文献#groebner]]
*8 話者がそもそも弱い背理法と強い背理法の2種類の区別を知らない場合や、それらと同値なものを把握していない場合もあります。こういったことは一度でも耳にしているのでなければ自分で思い付くことが困難な話題ですので、それは仕方のないことです。たまたま当事者に知識がなかったからといって、それを責めることもまた多くの場合は不毛なことです。