コラム　排中律と背理法

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

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

もう１つは否定除去則（negation elimination）または\( \neg \)除去則（\( \neg \)-elimination）と呼ばれるもので、論理式\( \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で証明できない以上、新たにそういう演繹規則を導入してみよう、と考えることは自然だと思います。

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

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

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

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

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

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

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

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

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

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

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

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

• 述語論理へ戻る。