Semantics for the minimal well-determined logic

「もし〜ならば」と「かつ」の論理：真実の国の探偵物語

あなたは、指紋やアリバイの代わりに「文章」を手がかりにする、ある謎解きに挑む探偵だと想像してください。論理学の世界には、「命題論理」と呼ばれる特別な分野があります。これは、単純な文をどのように結びつけて複雑な真実を構築するかを研究するものです。これは、推論の文法のようなものだと考えてください。この文法における最も有名な2つの道具は、「連言」（2つのものを結合する「かつ／and」という言葉）と、「含意」（条件を設定する「もし〜ならば／if... then」という言葉）です。

通常、私たちが推論を行うときには、「モドゥス・ポネンス（肯定式）」と呼ばれる黄金律があります。それは私たちの思考を動かすエンジンです。「もし雨が降っていれば、地面は濡れている。雨が降っている。したがって、地面は濡れている。」このルールは非常に自然に感じられるため、私たちはしばに当たり前のように受け入れています。しかし、もしこのルールが自動的に機能することを前提としない、論理システムを構築しようとしたらどうなるでしょうか？「かつ」と「もし〜ならば」がシステム全体を壊すことなく機能するために必要な、絶対的な最小限のルールを見つけたいとしたら？これが、イゴール・ゴルブノフとミハイル・リバコフが取り組んでいる問いです。彼らは、よくある論理の「最小限」のバージョン、つまり、意味を成すのに十分な強さでありながら、意図しないことを強制しないほど強くはないシステムを探しているのです。

論文の大きな発見：エンジンを持たない論理

この論文の中で、著者たちは「最小限の決定論的論理（minimal well-determined logic）」と呼ぶ、非常に特定の、削ぎ落とされたバージョンの論理について調査しています。彼らはまず、「『かつ』と『もし〜ならば』を機能させるために必要な最小のルールのセットは何だろうか？」という問いから始まります。

通常、論理学者は、公理（出発点の真実）と、一つの真実から別の真実へと移動する方法を教えるルール（モドゥス・ポネンスのようなもの）を列挙することでシステムを構築します。著者たちは、モドゥス・ポネンスを最初からのルールとして仮定することなく、この最小限の論理を定義する方法を見つけ出しました。システムを適切に設定すれば、「もしAならばBであり、かつAである、したがってBである」というルールは、他のルールから自然に「創発」されることが分かったのです。それは、毎回押して進ませるのではなく、鍵を回せばエンジンが自ら始動する車を組み立てるようなものです。

この論理が機能することを証明するために、著者たちはそれを可視化する新しい方法を編み出す必要がありました。彼らは、「最小元を持つ下半束（lower semilattice）」という数学的構造に基づいた「意味論（semantics）」（記号を解釈する方法）を作成しました。

これをイメージする方法は以下の通りです。ピラミッドで作られたブロックを想像してください。

• ブロックは、異なる文や概念を表します。
• ピラミッドの形状は、これらの概念がどのように関連しているかを表します。もし2つのブロックを組み合わせてより大きなブロックを作れるなら、それがあなたの「かつ（連言）」です。
• 最上部のブロックは「最大元」であり、究極の真実、あるいはすべてが満たされた状態を表します。

ほとんどの論理システムにおいて、「もし〜ならば（含意）」は2つのブロックを取り込み、新しいブロックを吐き出す機械のようなものです。しかし、この最小限の論理では、「もし〜ならば」は常に同じように新しいブロックを生み出すわけではないことに、著者たちは気づきました。時には条件が満たされず、機械はただ停止していることがあります。そのため、彼らは「もし〜ならば」を「部分関数（partial function）」として定義しました。それは、正しいコインを入れて初めて動作する自動販売機のようなものです。もし正しい組み合わせのブロック（最初のブロックがピラミッド内で2番目のブロックの中に「含まれている」場合）を投入すれば、機械は最上部のブロック（真）を返します。もし条件が満たされない場合、機械は結果を出しません。つまり、未定義となります。この「部分的」な性質こそが、モドゥス・ポネンスのルールを最初から存在させることなく、論理を機能させる鍵なのです。

驚きの展開：それは速い！

ここから物語は非常にエキサイティングになります。通常、論理をその骨組みまで削ぎ落とすと、数学がめちゃくちゃになったり、ルールをチェックするのが信じられないほど難しくなったりすることを予想するかもしれません。「標準的なルールを取り除いたら、ある文が真であるかどうかを判断するのに永遠に時間がかかるのではないか？」と思うかもしれません。

しかし、著者たちは驚くべき発見をしました。実は、非常に速いのです。

彼らは、与えられた文がこの最小限の論理において「トートロジー（常に真となる文）」であるかどうかをチェックするための、特定のアルゴリズム（コンピュータのためのステップ・バイ・ステップのレシピ）を設計しました。彼らは、このアルゴリズムが**多項式時間（polynomial time）**で動作することを証明しました。

これを日常的な言葉で言えば、こうなります。あなたがパズルを持っていると想像してください。もしそのパズルが「難しい」場合（多くの複雑な論理問題のように）、パズルを解くのにかかる時間は、パズルの大きさが大きくなるにつれて指数関数的に増大します。サイズが2倍になれば、解くのに100万倍長くかかるかもしれません。しかし、この最小限の論理の場合、パズルを解くのにかかる時間は、単純な曲線（例えば、サイズの2乗など）のようにしか増えません。文の長さが2倍になっても、コンピュータが必要とする作業量は、100万倍増えるのではなく、ほんの少し増えるだけなのです。

著者たちはこれに驚きました。彼らは、ほとんどの「自然な」論理（古典論理を含むもの）は、コンピュータで素早く解くのが非常に困難（coNP困難）であると指摘しています。しかし、この最小限に削ぎ落とされた論理は、その奇妙な「部分的」なルールにもかかわらず、コンピュータにとって実は扱いやすいものなのです。

これが意味すること

この論文は単に「ここに新しい論理があります」と言っているだけではありません。それは完全なツールキットを提供しています。

1. 新しい定義： 標準的な「もしAならばB」というルールを仮定せずに、この論理を構築する方法を示しました。
2. 新しい地図： この論理がどのように振る舞うかを説明するために、「ピラミッド（半束）」の意味論を構築しました。
3. 証明： 彼らの地図がルールと完全に一致していること（健全性と完全性）を証明しました。
4. スピードテスト： このシステムにおいてある文が真であるかどうかをチェックすることが、計算量的に容易であること（多項式時間）を証明しました。

著者たちはまた、この最小限の論理が基礎であることを指摘しています。後でより多くのルールを追加して、より強い論理を作ることはできますが、まずはこのクリーンで効率的なベースからスタートするのです。彼らは、この論理が古典論理とは根本的な部分で異なることも示しました。つまり、古典論理をコンピュータにとって難しくさせている「難しい問題」を、この論理は含んでいないのです。

要約すると、ゴルブノフとリバコフは、論理システムからその最も有名なエンジンを取り除き、それでも車が完璧に走行できることを見つけ出し、さらに、それは驚くほど速く走るスポーツカーであることも突き止めました。彼らは、「もし〜ならば」と「かつ」についての新しい考え方を提示しました。それは数学的に優雅であり、かつ計算量的に効率的なものです。