A non-uniform view of Craig interpolation in modal logics with linear frames

本論文は、K4.3を拡張する通常の様相論理は一般にクレイグの補間特性を欠くものの、与えられた一対の論理式に対してクレイグの補間式が存在するか否かを判定する特定の問題は決定可能であり、かつcoNP完全であること、そしてこの結果が標準的な線形時間フロー上のプリオア的時相論理にも拡張されることを示している。

要約

あなたは、式Aと式Bという2人の容疑者を追う探偵だと想像してください。あなたは、Aが真であれば、Bも必ず真になる（AはBを包含する）という事実を確信しています。

論理学の世界には、クレイグの補間特性（Craig Interpolation Property）と呼ばれる特別なルールがあります。それは、AがBを包含する場合、必ず「仲介者」となる文が存在するというものです。この仲介者をIと呼びましょう。この仲介者Iには、非常に具体的な役割があります。

1. Iは、AとBの両方に登場する言葉（変数）のみを使用しなければならない。
2. 「AならばI」、かつ「IならばB」が成り立つ。

これは、Iが「翻訳者」であることを意味します。もしAが「英語」を話し、Bが「フランス語」を話しているとしたら、補間文Iは、両方の言語に共通する言葉のみを用いて、Aの意味が論理的にBへと流れていることを証明する文章なのです。

問題：失われた架け橋

多くの論理体系（標準的な数学や基本的なコンピュータ論理など）では、この架け橋Iは常に存在します。しかし、この論文の著者たちが注目しているのは、K4.3とその周辺の、非常にトリッキーな論理体系です。これらの論理は「線形」の世界、つまり、過去から未来へと一方向に進む時間や、行列に並ぶ人々のように、一本の直線的な世界を描写しています。

この「線形」の世界では、「架け橋のルール（クレイグの補間特性）」が崩壊します。つまり、AがBを包含しているにもかかわらず、ルールに適合する仲介文Iが見つからない場合があるのです。これは、論理的には成立しているのに、共通の語彙だけを使ってその繋がりを要約できる文章が一つも見つからない、というような状況です。

通常、論理がこのルールを破る場合、研究者たちは「架け橋が見つからない以上、この繋がりを研究することはできない」と言って諦めてしまいます。

新しいアプローチ：「架け橋は存在するか？」ゲーム

著者たちは、より「非一様（non-uniform）」なアプローチを取りました。彼らは、「すべての文のペアに対して、架け橋は常に存在するか？」（答えはノーです）と問うのではなく、より実践的な問いを投げかけました。

「これら特定の2つの文、AとBに対して、架け橋は存在するのか？」

これは、メカニックに対して「すべての車にエンジンがあるか？」と聞くのではなく、「この特定の車にエンジンは積まれているか？」と聞くようなものです。彼らはこれを**補間存在問題（Interpolant Existence Problem: IEP）**と呼んでいます。

大発見：妥当性チェックと同じ難易度である

著者たちは驚くべきことを証明しました。これらの論理において「架け橋のルール」は崩壊していますが、特定の2つの文に対して架け橋が存在するかどうかを判断することは、決して超高度で不可能なタスクではないということです。

コンピュータサイエンスの用語で言えば、架け橋が存在するかどうかを判定する難易度は、元の命題（AならばB）が真であるかどうかをチェックする難易度と全く同じです。彼らはこの複雑さを**coNP完全（coNP-complete）**と呼びます。

例え話：
川を渡ろうとしている場面を想像してください。

• 旧来の見方： 「橋が壊れているのだから、決して渡ることはできない。」
• 著者たちの見方： 「橋は壊れているが、あなたを渡らせるための特定の『ボート』が存在するかどうかは確認できる。そして、そのボートが存在するかを確認することは、そもそも川が存在するかを確認することと同じくらい簡単だ。」

彼らは、これらの線形論理において、架け橋を見つけるためにスーパーコンピュータは必要なく、標準的なコンピュータで効率的に解決できることを示しました。これは、他の類似した論理体系において、架け橋の存在を知ることが元の命題の真偽判定よりも遥かに難しい場合があるため、大きな発見なのです。

どうやって解決したのか：「記述的フレーム」の地図

これを解決するために、著者たちは**記述的フレーム（descriptive frames）**というツールを用いました。これは、論理的世界の詳細な高解像度地図のようなものです。

• あるときは、単純で有限な線のように見えます。
• またあるときは、無限に続くクラスター（点の集まり）の連鎖、例えば、頭部と無限に続く尾を持つ「タダポール（おたまじゃくし）」のような形をした、無限に広がる鎖のように見えます。

著者たちは、たとえこれらの地図が複雑になったとしても、「架け橋が存在しない」という悪いケースは常に非常に具体的で理解可能なパターンに従うことを発見しました。彼らは、これらの無限で複雑な地図を、真実を保持したまま、扱いやすい多項式サイズのバージョンへと常に縮小できることを証明しました。

彼らはこの手法を以下に適用しました：

1. 標準的な線形論理： 直線の論理（K4.3）。
2. 時間論理： 「未来」と「過去」の両方を扱う論理（時間の流れを扱うもの）。彼らは、整数（..., -2, -1, 0, 1, 2...）、有理数（分数）、実数（連続数）、および有限の時間といった、特定の時間の流れを調査しました。

これらすべてにおいて、架け橋の存在をチェックすることは計算量的に管理可能（coNP完全）であることを彼らは証明しました。

まとめ

この論文は、「これらの論理には補間特性がない」という「ネガティブな」事実を、「ポジティブな」研究課題へと転換させました。彼らは、完璧な架け橋が存在しない線形の世界であっても、特定の状況において架け橋が存在するかどうかを効率的に判断できることを示しました。

要約すると： これらの線形の世界において「完璧な架け橋のルール」が崩れていても、私たちは暗闇に取り残されるわけではありません。特定の文のペアに対して道が存在するかどうかを調べるための、信頼できる効率的な懐中電灯を、私たちは手にしているのです。

技術概要

技術的要約：線形フレームにおける様相論理の非一様的なクレイグ補間に関する考察

問題設定
クレイグ補間特性（CIP）は、任意の妥当な含意 $\phi \to \psi$ に対して、$\phi$ と $\psi$ の共有語彙のみを用いる補間式 $\iota$ が存在し、$\phi \to \iota$ および $\iota \to \psi$ もまた妥当であるという論理学における基本的な性質である。K4.3（線形推移的フレームの論理）を拡張する多くの正規様相論理において、CIPが欠如していることは、既知の「負の」事実である。特に、非有界な深さを持つフレームを持つ論理においては顕著である。伝統的に、CIPの欠如は、与えられた論理に対する補間式研究の終焉を意味してきた。

本論文は、CIPの欠如を、**補間式存在問題（IEP）**の調査を通じて研究課題へと再構成する。すなわち、論理 $L$ において $\phi \to \psi$ が妥当であるとき、$L$ におけるクレイグ補間式が存在するかどうかを問うものである。一様的なCIPとは異なり、IEPは単純な妥当性判定に還元できない。なぜなら、含意の妥当性は補間式の存在を保証しないからである。中心となる問いは、IEPがこれらの論理における妥当性問題（含意）よりも計算量的に困難であるかどうかである。他の論理（例：名辞を持つ様相論理や一階述語論理の断片）における先行研究では、IEPは大幅に困難（例：3ExpTime）になる可能性が示唆されている。本論文は、K4.3を含む命題様相論理において、この傾向が当てはまるかどうかを調査する。

手法
著者らは、**双模倣（bisimulation）と記述的フレーム（descriptive frames）**に基づく、非一様的なモデル論的手法を用いている。

1. 双模倣による特徴付け： 本論文は、$\phi \to \psi$ が $L$ において補間式を持たないための条件として、「$\phi$ を満たすモデル $M_1$ と $\neg\psi$ を満たすモデル $M_2$ が存在し、それらの根の点が $\sigma$-双模倣である（ここで $\sigma$ は共有されるシグネチャ）」という既知の基準（定理3.2）を利用している。
2. 記述的フレーム： 分析は、記述的フレーム（分化、緊密性、およびコンパクト性の条件を満たす特定の内部集合の代数を備えたフレーム）の構造に大きく依存している。これは、GL.3 や Log{(N, <)} のような論理において、CIPの反例が標準的なクリプキ・フレームでは表現できず、無限の記述的フレームを必要とするためである。
3. 構造的分解： 核となる技術的革新は、これら双模倣モデルの構造の分析にある。著者らは、モデルを $\sigma$-ブロック（特定の双模倣特性を持つ点の区間）に分割し、補間式の欠如を証拠立てるあらゆる双模倣モデルのペアが、「準有限」なモデルのペアへと変換可能であることを示す。これらのモデルは、特定の原子的フレーム（有限の鎖、有限のクラスター、または $C(\bigcirc_k, \bullet)$ のような「タドポール（tadpole/蝌蚪）」構造）に基づく単純モデルの順序和として構築される。
4. 準多項式サイズ特性： 有限公理化された論理に対して、著者らは、これらの証拠となるモデルが入力式のサイズおよび論理の公理のサイズに対して多項式によって抑えられることを証明した。これは準多項式サイズ双模倣モデル特性と呼ばれる。

主要な貢献と結果

• 決定可能性と計算量： 本論文は、K4.3を含むすべての有限公理化正規様相論理について、IEPが決定可能であり、coNP完全であることを証明している。

  • この結果は、IEPが妥当性問題（これらの方程式においてはcoNP）よりも困難ではないことを示しており、これは非常に重要である。これは、他の論理的枠組みにおける最近の非一様的な補間結果（IEPが厳密に困難であるケース）とは対照的である。
  • 証明には、双模倣基準を満たす多項式サイズのモデルを推測し、論理の公理を検証する非決定論的アルゴリズムが含まれる。

• 準多項式サイズ双模倣モデル特性： 著者らは、すべての有限公理化されたK4.3の拡張が「準多項式サイズ双模倣モデル特性」を持つことを確立した。これは、もし補間式が存在しないならば、モデルが多項式個の単純モデルに基づく原子的フレームの順序和であるような、双模像を証拠立てるモデルのペアが存在することを意味する。

  • d-持続的余極限部分フレーム論理（その一クラス）については、この特性はさらに強く、モデルが多項式サイズの標準的なクリプキ・フレームとなる多項式サイズ双模倣モデル特性を持つ。

• プリオア的（Priorean）時間論理への拡張： 手法は、標準的な時間の流れ（未来と過去の両方の様相を含む）におけるプリオア的時間論理へと拡張されている：

  • Lin（すべての線形フレーム）、LinQ（有理数）、および LinR（実数）：これらの論理は多項式サイズ双模倣モデル特性を持ち、そのIEPはcoNP完全であることが示されている。
  • Lin<ω（有限の厳密な線形順序）および LinZ（整数）：これらの論理は多項式サイズ特性は持たないが、準多項式サイズ双模倣モデル特性を持ち、そのIEPもcoNP完全であることが証明されている。
  • 時間論理の証明には、双方向の鎖と両方向の極限クラスターを扱う必要があり、新しいフレーム構築（例：対称的な「タドポール」フレーム $C(\bullet, \bigcirc_k, \bullet)$）が必要となる。

意義と主張
本論文は、CIPを欠く広範な様相論理のファミリー（K4.3の拡張）をカバーする、クレイグ補間存在に関する最初の一般的な結果を提供すると主張している。IEPがこれらの論理においてcoNP完全であることを示すことで、著者らは、CIPの欠如が必ずしも存在問題の計算量クラスを高くすることにはならないという直感に異を唱えている。

本研究は、IEPの複雑さはCIPの失敗に本質的に結びついているのではなく、むしろ失敗を証拠立てるために必要なモデルの構造的特性に依存していることを示唆している。著者らは、これを様相論理をIEPの複雑さに基づいて分類するためのステップとして位置づけている。

なお、本論文は、補間式の計算に関する非構成的な証明であることを明記している。すなわち、存在の決定手順は提供するが、補間式自体を計算する効率的なアルゴリズムや、そのサイズの大きさの上限を与えるものではない。また、著者らは、証明において記述的フレームが不可欠であることを強調しており、d-持続的ではないが強固なクリプキ完全性を持つ論理（LinRなど）において、KripkeフレームがIEPに十分であるかという未解決の問いを提起している。