論理学FAQのブログ

授業でもらったコメントに対して書いたリプライを、ブログ形式に編集しました。

「コンピュータの理解を越える論理式」？

2019年5月13日のコメントペーパーより。レジュメは古典命題論理。

コメント：コメントペーパーの回答で、論理式は計算できるということに驚きました。じっさいにソフトのようなもので論理式を計算する人はいるのでしょうか？また、いるならばコンピュータの理解を越える論理式がこれから出る可能性はあるのでしょうか？ 

回答：ひとつめの問いについてはイエスで、ウェブ上にたくさんプログラムがあります。たとえば(ちょっとぐぐっただけですが) The Propositional Logic Calculator とか
Tree Proof Generator とか出てきますね。ふつうの論理学の授業では、前回の授業でお話した「タブロー (真理の木) 」の方法がよく使われるからか、それを自動生成するものが多い印象です。

ちなみに、以前放送大学のお仕事を手伝ったときに、みんなで

対話的タブローチェッカー「タブ朗」

というのを作りました。「タブ朗」は私の名前から取られています。これはコンピュータが自動で計算してくれるというよりも、コンピュータに間違いをチェックしてもらいながらタブローを自分で作るためのプログラムです。

さて、2つめの質問はきわめて重要で、授業でも話したいんですが、おそらく時間はないので書いてしまいましょう。

まず、「コンピュータの理解を越える」というのはなかなか難しい表現ですが、ここで問題になるのは計算可能性の概念だと思います。「計算する」とは、人間の勘や経験則に頼るのではなく、予め明確に決められた規則に従って、機械的な操作を繰り返し、有限ステップのうちに答えを出すことです。そして、ある問題に対してこのような仕方で答えをだすことのできるアルゴリズムが存在するとき、その問題は計算可能 (computable) であると言います *1。

さらに、与えられた入力に対して、とくに「イエス」か「ノー」のどちらかを答えとして返す問題を決定問題 (decision problem) と呼びます。推論の妥当性の判定は、妥当であるか妥当でないかを判定するわけですから、まさに決定問題ですね。そして、ある決定問題が計算可能であるとき、すなわち、与えられたどんな入力に対しても、(正しく)イエスあるいはノーを答えとして返すことのできる、そのようなアルゴリズムが存在するとき、その問題は決定可能 (decidable)であると言います。

さて、というわけで、「コンピュータの理解を越える」論理式なり推論があるかどうかという問題は、推論の妥当性は決定可能かどうか、という問題と理解することができると思います。任意の推論、つまり前提と結論の組み合わせが与えられたときに、それが妥当であるかどうかを判定するアルゴリズムは存在するかどうか、です。

もう少し正確さを期すことにしますが、この講義の最初から言っているように、論理と言ってもたくさんあります。ある推論が妥当であるかどうかは、それをどの論理の妥当性で考えるかに依存します。また、論理の違いはしばしば推論を表現する言語のちがいでもありますから、そのことにも注意して、次のように定義しましょう。

定義：ある論理 L (の妥当性決定問題) が決定可能であるとは、 L の論理式によって構成された任意の推論について、それが論理 L において妥当であるかどうかを判定することのできる、ひとつのアルゴリズムが存在することである。 

この定義のもとでは、まず、古典命題論理は決定可能です。たとえばタブローによる妥当性判定方法がアルゴリズムを与えてくれます。上で紹介したように、そのアルゴリズムは現実のコンピュータに実装することもできます。

次に、これから見る様相論理は基本的に決定可能です。「基本的に」というのは、いくつもある様相論理のうち代表的な体系は決定可能だということです。シンプルなタブローの方法だと、計算が終わらなくなることもあるので、別の方法が必要ですが、ともあれ決定可能です。

そして、前期の後半で見る古典述語論理は決定不可能です。述語論理は、命題論理の \neg, \wedge,\vee, \supset に加えて「すべての」と「存在する」を表す記号を扱う論理です。決定不可能ということは、タブローの方法であろうが何であろうが、どのようなアルゴリズムを考えても、どれだけ高性能なコンピュータを使っても、ちゃんとした答えを与えることのできない推論が出てきてしまうということです。典型的には、計算プロセスが循環 (ループ) してしまったり、無限に展開したりしてしまいます。

決定不可能性の内実をより詳しく言うと、述語論理は半決定可能 (semi-decidable) ではあります。すなわち、入力された推論が妥当な推論のときには必ず「イエス」という答えを出すアルゴリズムは作ることができます (たとえばタブローがそうです)。ただし、妥当でない推論に対しては、そうはいきません。どのようなアルゴリズムも「ノー」と答えが出せない推論を抱えてしまいます。

すでに述べましたが、この決定不可能性は、どのようなアルゴリズムを考えても、どれだけ高性能なコンピュータを使っても、原理的に不可能という意味です。ここで考えている計算可能性というのは、1930年代にチューリングやチャーチらによって確立された概念で、現代のわたしたちが使っているコンピュータの理論的な基盤となっています。ということで、述語論理は以上に述べたような意味で「コンピュータの理解を越える」と言ってよいのではないでしょうか。

*1:ここでは「機械的な操作」とか「アルゴリズム」とかいう言葉を使ってざっくり説明していますが、数学における計算可能性理論では、これらの概念が厳密に定義されます。また、計算可能性概念がかかわる「問題」としては自然数上の関数だけを考えます。つまり、自然数が入力されたときに何らかの自然数を答えとして出力するという問題です。推論の妥当性判定などの操作は、以前に少し触れたように、まずはそれらを自然数上の関数として表現して、それから計算可能性を判断するという手順になります。