Definability of Functional Properties in the Basic Modal-Temporal Language over Ordered Frames

技術的要約：順序フレームにおける基本様相・時間論理における関数的性質の定義可能性

問題提起
本論文は、基本様相言語に$\Box$（すべての関数像において）に加え、プライヤーの時間演算子である$G$（将来において常に）および$H$（過去において常に）を付加して形成される基本様相・時間言語$LT \times W$の表現力を調査するものである。本研究では、5つの異なる順序型（前順序（PRE）、厳密前順序（sPRE）、半順序（PO）、線形順序（LO）、および厳密線形順序（sLO））における、全射性、非全射性、単射性、全射性、単調増加性、厳密単調増加性、単調減少性、厳密単調減少性、および定数性の9つの特定の関数的性質の定義可能性に焦点を当てる。

中心となる課題は、複数のアクセシビリティ関数が共存し、様相演算子がそれらの結合された像に対して無差別に量化を行う「マルチフロー（multiflow）」の設定である。先行研究（例：[1, 3]）では、厳密線形順序および一様ドメイン（U-Dom）特性のようなグローバルな制約に限定して分析を行ってきた。本論文は、これらの性質が単独で定義可能であるかどうか、また、その定義可能性が2つの異なる意味論的解釈（現在の瞬間を含む標準的な解釈と、現在の瞬間を除外する厳密な解釈）によってどのように変化するかを、より広範な順序構造のスペクトルにわたって検証することで、定義可能性を明らかにすることを目的としている。

手法
著者らは、$LT \times W$の表現境界をマッピングするために、2段階の分析的アプローチを採用している。

1. 任意の順序マルチフロー設定： フレームが任意の関数の族で構成される一般的な設定において、定義可能性の限界をまず確立する。ここでは、様相演算子はすべての関数の像の和集合に対する二階の量化子として機能する。著者らは、性質を満たすフレームを、その性質を満たさないフレームへと写すp-モルフィズム（これは関数的双模倣を誘導する）を用いて、非定義性を証明する。もしp-モルフィズムが、ある性質を満たすフレームを、その性質を満たさないフレームへと写す場合、その性質は定義不可能である。
2. 構造的精緻化（最小フレーム）： 表現力の限界の源泉を特定するために、著者らは「最小関数フレーム」（$O_2$族）を導入し、フレームを最大2つのフローと単一のアクセシビリティ関数に制限する。この簡約化により、マルチフロー設定の二階の複雑さが、一次の相対的読みへと崩壊する。
3. 比較分析： 最小フレームの結果を、以下の他の2つの枠組みと比較する。
   • インデックス付き言語： 演算子が特定の関数を区別するために明示的にラベル付けされているもの。
   • 一様ドメイン（U-Dom）フレーム： フレーム内のすべての関数が共通のドメインを共有するもの。
4. 意味論的変異： 標準的解釈（$G, H$）と厳密な解釈（$G^*, H^*$）の両方の条件下で分析を行い、現在の瞬間を除外することが定義可能性の景観を変化させるかどうかを判断する。

主な貢献と結果

• マルチフロー設定における表現限界：
  一般的なマルチフロー設定において、この言語は著しく弱い。本研究では、全射性と全射性のみが定義可能であり、かつそれは線形順序（LOおよびsLO）においてのみであることを証明している。その他の性質（単射性、単調性、定数性など）は、線形順序を含むあらゆる順序型において定義不可能である。これは、複数の関数の個別の振る舞いを不明瞭にする「無差別な量化」に起因する。

• 最小フレームの影響：
  意味論を最小フレーム（単一関数）に制限することで、定義可能性の景観は劇的に拡大する：

  • 単調増加性と単調減少性： これらはすべての順序型（PRE, sPRE, PO, LO, sLO）において定義可能となる。
  • 単射性： 標準的な解釈の下で、厳密線形順序（sLO）において定義可能となる。
  • 厳密単調増加性／厳密単調減少性： 厳密前順序および厳密線形順序において定義可能となる。
  • 定数性： 最小フレームにおいても非線形順序（PRE, sPRE, PO）では定義不可能なままであり、独自の意味論的等価性の議論を必要とする。

• 厳密な解釈の役割：
  一般的なマルチフロー設定では、標準的解釈と厳密な解釈の選択は同一の結果をもたらす。しかし、最小フレームにおいては、厳密な解釈（$G^*, H^*$）が重要な利点をもたらす：

  • 標準的な解釈では定義不可能な線形順序（LO）において、単射性の定義を可能にする。
  • すべての順序型において、それらを厳密な対応物として扱うことで、厳密単調増加性と厳密単調減少性の定義を可能にする。

• 枠組みの等価性：
  本論文は、最小フレームで得られた定義可能性のパターンが、インデックス付き言語（関数が構文的に区別されているもの）およびU-Domフレームと同一であることを示している。これは、元の枠組みの表現力の限界が、演算子自体の弱さからではなく、ドメインが異なる関数の制御不能な多重性に由来することを示している。関数の多重性が（構造的簡略化、ドメインの一様性、または構文的インデックス化を通じて）制御されると、基本演算子は本来の能力を取り戻す。

• 根本的な障害：
  関数の多重性を制御した後でも、「核」となる性質――全射性、非全射性、単射性、全射性、および定数性――は、すべての非線形順序（PRE, sPRE, PO）において定義不可能なままである。著者らは、連結性の欠如（点の比較不能性）が、解釈や構造的精緻化に関わらず、時間的様相が克服できない根本的な障害であると結論付けている。

意義
本論文は、順序フレーム上の基本様相・時間言語の表現限界を体系的に分類している。その主要な意義は、元のマルチフロー設定における基本的な関数的性質の定義不可能性が、時間的演算子の固有の欠陥ではなく、制御不能な関数的多重性の構造的な副産物であることを特定した点にある。

最小フレーム、インデックス付き言語、およびU-Domフレームが同一の定義可能性パターンを示すことを示すことで、本研究は、どのような条件下で関数的性質が定義可能になるのかという精密な条件を明らかにしている。構造的簡略化によって単調性と単調減少性をすべての順序型にわたって定義可能にできる一方で、全射性や単射性のようなグローバルなドメイン比較を必要とする性質にとって、線形的な連結性の欠如が永続的な障壁であり続けることを確立している。また、p-モルフィズムによる標準的な非定義性の証明を回避し、独自の意味論的等価性の議論を必要とする定数性の特殊な地位についても強調している。