Positive Instantial Neighbourhood logic

本論文は、独立したボックスおよびダイアモンド様相を持つ否定を含まない様相体系である正の即時的近傍論理（Positive Instantial Neighbourhood Logic: PINL）を導入し、永続的近傍意味論、2-DLIosを用いた代数的意味論、および標準的なビットポロジカル表現を通じてその完全性を確立する。

要約

あなたは、**World（世界）と呼ばれる謎めいた都市を解明しようとしている探偵であると想像してください。この都市では、すべての人間（あるいは「世界」）には、個人的なNeighborhood（近隣領域）**が存在します。

伝統的な論理学では、探偵は次のように問いかけます。「この近隣領域にいる全員がルールに従っているか？」あるいは「ここにルールを破った人が少なくとも一人存在するか？」

この論文は、これらの近隣領域を調査するための、より詳細で新しい方法を紹介しています。それは**Positive Instantial Neighbourhood Logic（PINL：正の即時的近隣領域論理）**と呼ばれます。その仕組みを、シンプルな概念に分解して説明します。

1. 「否定禁止」のルール（ポジティブなひねり）

通常、探偵は事件を解決するために「いいえ」や「〜ではない」という言葉を使います。例えば、「全員が潔白であるわけではない」といった具合です。
しかし、この論文では「いいえ」という言葉の使用を禁止することに決めました。探偵は、何が「ない」かではなく、何が「ある」かという事実のみを語ることができます。

• 比喩： 果物籠を説明している場面を想像してください。「リンゴがある」「バナナがある」と言うことはできます。しかし、「オレンジはない」と言うことはできません。実際に存在するものだけを記述できるのです。
• 結果： 「いいえ」を使えないため、探偵の二大ツールであるBox（ボックス／□）（グループ内の全員が何かを行うかどうかをチェックする）と、Diamond（ダイヤモンド／♢）（グループ内に誰かが何かを行うかどうかをチェックする）は、完全に独立したツールとなります。これらはもう、互いを定義するために使われることはありません。

2. 二つの特別なツール：Box と Diamond

この新しい論理において、探偵は二つの特別なレンズを使って近隣領域を観察します。

• Boxレンズ (□): このレンズは、「特定のグループにおいて、全員が主要なルールに従っており、かつ特定の個人も存在することを証明するために存在しているか？」と問いかけます。
  • 例： 「全員が帽子を被っており（主要なルール）、かつ、そのグループの中に具体的に『背の高い人』と『背の低い人』が存在するようなグループはあるか？」
• Diamondレンズ (♢): このレンズは、「私たちが選びうるあらゆるグループについて、そのグループが『特定のルールを破る人々』だけで構成されているか、あるいは、そのグループの中に『主要なルールに従う人』が少なくとも一人含まれているか？」と問いかけます。
  • 例： 「どのグループを選んだとしても、そのグループは全員が嘘つきであるか、あるいは、少なくとも一人は真実を語っている。」

3. 「標準的な」地図の問題点

著者たちは、これらのルールを用いてこの都市の完璧な地図（標準モデル／カノニカル・モデル）を構築しようと試みました。しかし、そこで障害に突き当たりました。

• グリッチ（不具合）： 標準的な地図では、近隣領域は単なる「ラベルのない人々のリスト」として扱われます。もしあるリストが「Box」ツールの記述に適合する場合、地図はその同じリストを、たとえ本来はそうあるべきでない場合でも、「Diamond」ツールを満たすために誤って使用してしまう可能性があります。これは、例えば「背の高い人」の写真を使って、同じ写真の中に写っているからといって「背の低い人」の存在を証明してしまうようなものです。
• 修正策： これを解決するために、著者たちはTyped Map（型付けされた地図）を作成しました。単なる人々のリストではなく、地図上のすべての近隣領域にはラベルが付与されます。
  • 比喩： 都市のあらゆるグループには、名前タグが付いていると考えてください。あるグループは「Boxツールのためのグループ」とラベル付けされ、別のグループは「Diamondツールのためのグループ」とラベル付けされます。これにより、探偵が混乱して、間違ったグループを間違った仕事に使ってしまうことを防ぎます。

4. 代数的な「レシピ本」

この論文は、これらの論理的ルールを2-DLIOと呼ばれる数学的な「レシピ本」へと翻訳します。

• これは、論理的な命題を材料とする料理本のようなものです。
• この本には二種類の指示（レシピ）があります。一つは「Box」の材料のためのレシピ、もう一つは「Diamond」の材料のためのレシピです。
• 著者たちは、もし彼らの論理（PINL）に従うならば、それは本質的にこの特定のレシピ本に従っていることになるのだと証明しました。彼らは、「Lindenbaum代数」（これは「あらゆる可能な論理的レシピの集合」を指す格好の良い言い方です）が、このレシピ本に完璧に適合することを証明しました。

5. 最終的な地図：Bitopological City（双位相空間の都市）

最後に、著者たちは**Bitopological Space（双位相空間）**と呼ばれる、より壮大な最終版の都市地図を構築しました。

• この地図には、二層の地理構造があります：
  1. ポジティブ・レイヤー（正の層）： 物事が「どこにあるか」を示す層。
  2. ネガティブ・レイヤー（負の層）： 物事が「どこにないか」を示す層。ただし、これは「いいえ」という言葉を使わずに、失敗した事象のリスト、すなわち「カウンター理論」として記述されます。
• 大きな成果： 著者たちは、「レシピ本（代数）」とこの「二層の都市地図（位相空間）」が、実際には異なる角度から見た同じものであることを証明しました。レシピを知っていれば都市を構築でき、都市を見ればレシピを読み取ることができるのです。

まとめ

この論文は、近隣領域のための新しい「否定なし」バージョンの論理システムを作り上げました。著者たちは、BoxとDiamondという二つの主要なツールが混同されないよう、ラベル付けされた「型付き」の地図を構築することで、トリッキーな問題を解決しました。そして、この論理システムが、特定の種類の代数的なレシピ本および二層の都市地図と完璧に一致することを示すことで、数学的に健全であることを証明しました。

この論文が「行わない」こと：

• 実世界のコンピュータシステム、医学的診断、または法的ケースへの適用は行いません。
• 「双対性（duality）」の問題を完全に解決したとは主張していません（これを将来の理論への「第一歩」と呼んでいます）。
• BoxとDiamondのツールを一つのツールに統合することはありません。現時点では、それらを別々のものとして維持しています。

技術概要

技術要約：正のインスタンス的近傍論理 (Positive Instantial Neighbourhood Logic: PINL)

問題提起
インスタンス的近傍論理 (Instantial Neighbourhood Logic: INL) は、近傍フレームのための様相言語であり、普遍的なスコープ条件だけでなく、近傍内に出現する特定の「世界の様態（インスタンス）」に関する存在論的な情報をも表現することを可能にする。古典的な INL およびその余代数的双対性（ブール代数にインスタンス演算子を備えたもの、すなわち BAIOs を含む）は十分に発展しているが、体系的な「正の（否定を含まない）」バージョンの INL に関しては、文献における空白が存在する。

古典的な否定の欠如により、正の論理では $\Box$（ボックス）演算子と $\Diamond$（ダイアモンド）演算子の相互定義が妨げられる。したがって、正のバージョンの INL は、単なる古典的 INL の断片として扱うことはできず、独自の証明系、適切な正の近傍意味論、分配束に基づく代数的意味論、および標準的な表現（canonical representation）を必要とする。本論文は、これら基礎的な構成要素の欠如に対処するものである。

手法
著者らは、証明論、モデル論、代数学、および位相幾何学を組み合わせた多角的なアプローチを通じて、PINL と呼ばれる論理を開発する。

1. 構文と証明系: PINL の言語は、古典的な命題論理ではなく、有界分配束（$\top, \bot, \land, \lor$ を用いる）の命題基盤の上に構築される。これは、2 つの独立的で原始的なインスタンス的様相、すなわちボックス型の $\Box(\phi_1, \dots, \phi_n; \psi)$ とダイアモンド型の $\Diamond(\phi_1, \dots, \phi_n; \psi)$ を導入する。シーケントに基づく証明系は、有界分配束の公理と、それらの独立性を反映した $\Box$ および $\Diamond$ に関する特定の様相公理を用いて定式化される。
2. 意味論（持続的二側モデル）: この論理は、持続的二側近傍モデル (persistent two-sided neighbourhood models) 上で解釈される。これらの構造は、半順序集合 $(W, \leq)$ と、世界からアップセット（上方閉集合）への 2 つの近傍関数 $N_\Box$ および $N_\Diamond$ で構成される。決定的なのは、$N_\Box$ は単調増加（順序を保存）であり、$N_\Diamond$ は単調減少であることである。真理性は、$\Box$ のための「証拠 (witness)」条件（スコープおよびインスタンスの公式を満たす近傍の存在）と、$\Diamond$ のための「反証 (co-witness)」条件（条件の選言の普遍的充足）を通じて定義される。
3. 標準的構成と型付き意味論: 標準的な持続的意味論に対する直接的な標準的完全性の証明は、近傍の性質が外延的であること（ラベルのないアップセットが偶然にも複数の公式を証拠としてしまう可能性があること）によって阻害される。これを克服するため、著者らは補助的な 型付き持続的近傍意味論 (typed persistent neighbourhood semantics) を導入する。この設定では、近傍は、それが証拠となる、あるいは反証しようとしている特定の様相公式によってラベル付けされる。標準的モデルは、素理論ペア (prime theory pairs) $(a_1, a_2)$ から構築される。ここで $a_1$ は理論であり、$a_2$ は反理論である。タイプ・レマ（真理補題）がこの型付きモデルに対して確立され、意味論的な真理が素ペアの正の成分に属することと一致することが証明される。
4. 代数的意味論 (2-DLIOs): 本論文は、2-DLIOs（2 つのインスタンス的演算子の族 $(f_n)$（$\Box$ 用）と $(g_n)$（$\Diamond$ 用）を備えた有界分配束）を代数的対応物として導入する。PINL のリンデンバウム代数は 2-DLIO であることが示される。
5. 双位相的表現: 著者らは、素理論ペアから導出される 標準的双位相的 PINL 空間 (canonical bitopological PINL-space) を構築する。この空間は、2 つの位相（正のメンバーシップ集合 $U_\phi$ によって生成される $\tau_+$ と、負のメンバーシップ集合 $V_\phi$ によって生成される $\tau_-$）を備えている。この空間における許容可能な正の開集合の代数は、リンデンバウム 2-DLIO と同型であることが示される。

主要な貢献と結果

• 形式体系: $\Box$ と $\Diamond$ を、明確に異なる公理図式を持つ独立した原始的な演算子として扱う、PINL の言語と完全な証明系の定義。
• 完全性: 持続的二側近傍モデルに対する PINL の健全性と完全性の証明。これは、補助的な型付き意味論を用いることで達成され、これにより標準的構成における技術的な困難が解決される。
• 代数的特徴付け: 2-DLIOs を PINL の代数的意味論として導入。本論文は代数的健全性と完全性を証明し、PINL のリンデンバウム代数が 2-DLIO であることを示す。
• 標準的表現: 標準的双位相的 PINL 空間の構築。本論文は、この空間の許容可能な正の開集合の代数が、リンデンバウム 2-DLIO と同型であることを証明する。これにより、この論理の標準的な許容開表現が提供される。
• 関心の分離: 本研究は、古典的なブール枠組みや、相互作用公理が存在し得る完全な DLIO 枠組みから、正の独立演算子断片を明示的に分離している。

意義と範囲
本論文は、インスタンス的近傍論理の最初の体系的な、否定を含まない正のバージョンの開発を提供すると主張している。これは、証明系、意味論、および代数的基礎を確立することにより、文献における特定の空白を埋めるものである。

著者らは、本研究の範囲が 標準的表現定理 に限定されており、完全な圏論的双対理論ではないことを明示している。本研究は将来の双対理論（具体的には 2-DLIOs に対するプリースト型の、あるいは双位相的な双対性）のための基礎を築くものであるが、現在の論文では、必要な記述的 PINL 空間、射、または関手的扱いを定義していない。同様に、文献によって示唆されている「幾何学的」な INL（スコット連続性を伴うもの）についても、今後の課題として残されている。

その意義は、正の様相論理、近傍意味論、および分配束理論を橋渡しし、古典的な否定なしにインスタンス的性質を推論するための厳密な枠組みを提供し、将来の双対性研究に必要な代数的および位相幾何学的な道具を提供することにある。