First-Order Modal Logic in HOL: Deep and Shallow Embeddings with Automated Faithfulness (Extended Preprint)

あなたは、ある場所では真であり、別の場所では偽であるものについて考え、さらにそれらの場所における「すべての人」や「誰か」について語ることができる世界を、超知能ロボット（名前は「イザベル」としましょう）に教えようとしているところだと想像してください。これは、一階述語様相論理 (First-Order Modal Logic: FML) の世界です。それは、「もし〜だったら？」というゲームと、あらゆる可能な人物の出席確認を組み合わせたようなものです。

問題は、イザベルが非常に精密で高レベルな言語である 高階論理 (Higher-Order Logic: HOL) を話すことです。イザベルにこの「もし〜だったら？」ゲームを理解させるために、著者たちは、私たちの論理をイザベルの言語へと翻訳するための3つの異なる架け橋（埋め込み）を構築する必要がありました。

3つの架け橋

1. 深い架け橋（設計図 / The Deep Bridge）: これは、論理をレゴブロックを使って文字通り物理的なモデルとして構築するようなものです。あらゆるルール、あらゆる「かつ（and）」、あらゆる「否定（not）」、そしてあらゆる「全ての（for all）」が、巨大な構造物の中の個別のブロックとなります。これは重厚で詳細であり、論理の形状そのものを研究するには最適ですが、ロボットがその上で高速に動作させるには困難です。
2. 重量級の浅い架け橋（フルサービス・ホテル / The Heavyweight Shallow Bridge）: この架け橋は、豪華なホテルのようなものです。そこでは、すべてのゲスト（すべての論理式）に専用の部屋が用意され、その部屋には世界の地図、全人類のリスト、そして特定のガイドが付いています。すべてを明示的に運びます。非常に明快ですが、持ち運ぶには少々嵩張ります。
3. 軽量な浅い架け橋（ミニマリストのテント / The Lightweight Shallow Bridge）: これこそが、この論文の主役です。これは、小さくて持ち運び可能なテントです。このテントは、完全な地図や全員のリストを持ち歩く代わりに、「世界」と「ガイド」だけを持ちます。他の家具はすでにそこにあるものと仮定しています。これがあまりに軽量であるため、ロボットは「Sledgehammer」や「Nitpick」といった自動推論ツール上で、驚異的な速さで動作することができます。

大きな障害：全射性の問題 (The Surjectivity Problem)

ここで物語は複雑になります。著者たちは、軽量なテントと深い設計図が、実は全く同じことを言っているのだと証明したいと考えました。設計図において真であることは、テントにおいても真である、そしてその逆もまた然りであることを示したかったのです。

しかし、問題が発生しました。軽量なテントが使用するガイド（変数割り当て）は、可算な数の人々（自然数 1, 2, 3... のようなもの）しか指し示すことができません。しかし、深い設計図は、非可算な数の人々（実数直線上のすべての数のようなもの）が存在する宇宙を許容します。

もし宇宙が巨大で非可算である場合、可算なリストしか持たないガイドは、決して全員に到達することはできません。それは、1,000人の名前しか入らないリストを使って、スタジアムにいる10億人の観客の出席を取ろうとするようなものです。もし、非可算な宇宙において全員に到達させようとすれば、証明が崩れてしまうことに著者たちは気づきました。

魔法の解決策：下向きレーヴェンハイム–スコーレムの定理 (The Downward Löwenheim–Skolem Theorem)

これを解決するために、著者たちはガイドを非可算な群衆に到達させようとするのではなく、（可算）下向きレーヴェンハイム–スコーレムの定理という数学的な魔法のトリックを使用しました。

次のように考えてみてください。著者たちは、どんな巨大で非可算な宇宙に対しても、私たちが関心を持っている論理に関して全く同じように振る舞う、より小さく可算な「影の」宇宙が存在することを証明しました。それは、巨大な都市の完璧なミニチュアモデルを見つけるようなものです。そのモデルは、現実の街と同じようにすべての街角や建物が機能しながらも、机の上に載るほど小さいのです。

彼らは、たとえ現実の世界が非可算に巨大であっても、常にこの可算な影へと縮小できることを示しました。私たちの軽量なテントのガイドはこの可算な影の中の全員に到達できるため、テントと設計図の間の架け橋は再び強固なものとなりました。著者たちはこれが機能することを単に推測したりシミュレーションしたりしたのではなく、イザベルの中で厳密な数学的議論を構築し、これを証明したのです。

やらなかったこと（「ノー」のリスト）

この論文が、誤解を招かないように、何を行っていないのかを知っておくことは重要です：

• ドメインの変動なし (No Varying Domains): 彼らは、次元の間で人々のリストが変わる（例：別次元の間で人が生まれたり死んだりするSFのような設定）という問題には対処していません。彼らは、すべての可能世界において同じ集合の人が存在する定常ドメイン (constant domain) に固執しました。
• 等号なし (No Equality): 彼らは、自分たちの論理の中に特別な「等しい（$=$）」という記号を含めませんでした。彼らは、二つのものが同一であるかどうかではなく、物事の間の関係性に焦点を当てました。
• 無限の世界（未解決） (No Infinite Worlds (Yet)): 彼らの可算な影を成立させるために、彼らは「世界」の数もまた可算であると仮定しなければなりませんでした。彼らは、非可算な数の世界を扱うことは将来の課題であると認めています。

結果：検証されたつながり

著者たちは、これが機能すると示唆しただけではありません。彼らは、このプロセスをイザベルの中で**機械化（メカナイズ）**しました。彼らは置換メカニズム（変数を壊さずに交換するためのツール）を構築し、以下のことを証明しました：

1. 深い設計図と軽量なテントは、互いに忠実であること。
2. 軽量なテントで高速に証明を行うことができ、それらの証明は、詳細な設計図においても真であることが保証されること。
3. 彼らは、有名な論理規則（K公理やバルカン公式など）をチェックすることで、これらが成立することを確認し、テストを行いました。

要するに、著者たちは、コンピュータが量化子を伴う複雑な「もし〜だったら？」というシナリオについて推論するための、極めて効率的で軽量な方法を構築しました。そして、そのショートカットが、たとえ可能性の宇宙が無限に大きい場合でも、重要な詳細を飛ばしていないことを数学的に証明したのです。彼らは、潜在的な行き止まり（非可算ドメインの問題）を、巧みな数学的な縮小トリックを用いて、解決済みのパズルへと変えたのです。