Higher-order Kripke models for intuitionistic and non-classical modal logics

ビクトル・バルソサ＝ナシメントによる論文「直観主義論理および非古典的様態論理のための高次クリプキモデル」の解説を、日常的な言葉と創造的なアナロジーを用いて翻訳したものです。

大きなアイデア：「モデルのモデル」を構築する

必然的（必ず起こる）ことと可能的（起こりうる）ことについて、人々がどのように判断するかを理解しようとしていると想像してください。

標準的な論理（古典数学で使われるもの）では、クリプキモデルという道具を使います。クリプキモデルを、異なる**「可能世界」の地図**だと考えてください。

• 世界：事実が真か偽かである具体的な状況（例：「雨が降っている」）。
• 地図：これらの世界をつなぐネットワーク。世界 A が世界 B とつながっている場合、B は A に対する「可能な代替案」であることを意味します。
• 規則：世界 A においてあることが「必然的」であるなら、それは A に接続されているすべての世界で真でなければなりません。

問題点：
この論文は、直観主義論理に焦点を当てています。これは、「証明がある場合でなければ、『真』か『偽』かとは言えない」と信じる人々が使う、異なる種類の数学です。この論理では、真理は時間とともに成長します（数学者が新しい定理を発見していくように）。

この「成長する真理」のシステム内で「可能性」を扱う従来の方法は厄介です。それは、2 つの異なる種類の関係（接続）が絡み合ったモデルを必要とします。まるで、街をナビゲートするために、道路用と地下鉄用の 2 つの地図を同時に使おうとしているようなものです。これらがどのように相互作用するかという規則は複雑で、視覚化するのが困難です。

解決策：「ネスト型」アプローチ

著者であるビクトル・バルソサ＝ナシメントは、視点の劇的な変化を提案します。2 つの地図を 1 つに押し込むのではなく、モデルのモデルを構築することを提案するのです。

アナロジー：タイムライン図書館
数学者の人生のタイムラインがすべて本になっている図書館を想像してください。

• 本の中（モデル）：章は時間の異なる瞬間（朝、午後、夜）を表しています。朝から夜へと進むにつれて、数学者はより多くの定理を証明します。これが標準的な「クリプキモデル」です。
• 図書館（新しいモデル）：さて、図書館自体を地図だと想像してください。この新しい地図における「世界」は、単なる時間の瞬間ではなく、**本全体（タイムライン）**です。

この新しいシステムでは：

1. 「世界」はタイムライン：「朝に雨が降っているか？」と問うのではなく、「タイムライン A の朝において真か？」と問います。
2. 接続：本同士に線を引きます。「タイムライン A」が「タイムライン B」とつながっている場合、それはタイムライン B がタイムライン A の有効な代替バージョンであることを意味します。
3. 魔法のトリック：タイムライン A の朝においてあることが「可能」かどうかを判断するには、タイムライン A の午後を見るのではなく、タイムライン B の朝を見ます。

なぜこれが優れているのか？
古い厄介なシステムでは、「可能性」の規則は、「成長する真理」の規則の中に収まるように慎重に設計する必要がありました。この新しい「ネスト型」システムでは、規則はシンプルで自然です。

• 必然性：「朝に定理 X を証明することが必然的か？」→「私のタイムラインに接続されているすべての代替タイムラインの朝において、定理 X が証明されているか？」
• 可能性：「朝に定理 X を証明することが可能か？」→「朝に定理 X を証明している代替タイムラインが少なくとも 1 つ存在するか？」

著者はこれを高次クリプキモデルと呼んでいます。ロシアのマトリョーシカのようなものです。

• レベル 0：単一の世界（真理の割り当て）。
• レベル 1：レベル 0 の世界からなるモデル（標準的なクリプキモデル）。
• レベル 2：レベル 1 のモデルからなるモデル（新しい「高次」モデル）。

2 つの主要なキャラクター：IK と MK

この論文は、この新しいシステムを、著者がIKとMKと呼ぶ 2 つの特定の論理システムでテストしています。

1. IK（慎重派）：この論理は少し慎重です。あることが必然的かどうかを確認するには、代替タイムラインそのものだけでなく、そのタイムライン内のすべての未来の瞬間も調べます。「もし代替日の朝に X を証明できないなら、それは必然的ではない」と言うようなものです。
2. MK（大胆派）：この論理はより強力です。代替タイムライン内の特定の瞬間のみを見ます。その代替の「将来の成長」は無視します。「その日の後に何が起ころうとも、代替日の朝に X を証明できるなら、それは可能である」と言うようなものです。

著者は、この新しい「タイムライン図書館」システムが、これら 2 つの論理の両方に対して完璧に機能することを証明しています。実際、この新しいシステムは非常にクリーンであるため、古いシステムの複雑な規則（「二重関係」規則）が、無理やり導入するのではなく、自然に現れるようになります。

「大いなる一般化」

この論文の最も興奮する部分は、最終節です。著者は、「モデルのモデル」というアイデアが直観主義論理のためだけではないと提案しています。

彼は予想（さらに証明を必要とする強い推測）を提示します。

• 古い問題：標準的なクリプキモデル（レベル 1）では完全に記述できない、奇妙で複雑な論理システムがいくつか存在します。それらは「不完全」です。
• 新しい希望：モデルをネストし続ける（レベル 2、レベル 3 など）ことで、存在するすべての論理システムを記述できるかもしれません。

ビデオゲームのグラフィックだと考えてください。

• 標準モデル（レベル 1）：8 ビットグラフィックのようなもの。単純なゲームでは機能しますが、複雑なシーンになるとぼやけてブロック状になります。
• 高次モデル（レベル 2、3...）：4K や 8K グラフィックのようなもの。より多くの詳細の層（モデルの中にモデル）を追加することで、論理がどれほど複雑になっても、あらゆるシーンを完璧にレンダリングできます。

まとめ

この論文は、私たちは論理モデルを間違った方法で見てきたと主張しています。2 つの異なる規則を 1 つの地図に無理やり詰め込もうとするのではなく、モデルが新しいモデルの構成要素となるような階層を構築すべきです。

• 古い方法：2 種類の道路が混在する厄介な地図。
• 新しい方法：何が可能かを理解するために地図間を移動する、地図の図書館。

このアプローチは数学的に優雅で、概念的にはサウル・クリプキの「可能世界」という元のアイデアに近く、数十年にわたり数学者を悩ませてきた論理の最も困難な問題を解決する可能性を秘めています。