技術的概要：指向付き第一階論理の教義的意味論

1. 問題提起

本論文は、論理的枠組み内で指向付き等式を形式化する課題に取り組む。Lawvere の圏論的視点により、古典的等式は縮約に対する左随伴として成功裡に特徴づけられたが、このアプローチは対称性に依存している。指向付き型理論では、型が群圏（または集合）ではなく圏（または半順序集合）として解釈されるため、等式は非対称な関係（例えば、書き換え $a \to b$ または順序 $a \le b$）となる。

核心的な困難は変異性（極性）の処理にある。指向付き設定において、変数は「負」の位置（反変、例えば射の始点）または「正」の位置（共変、例えば射の終点）に現れる可能性がある。等式に関する標準的な論理規則（反射律と J 規則/消去則）は、この文脈では失敗する。なぜなら、それらは暗黙に対称性を仮定するか、あるいは変数が両方の極性に同時に現れることを許容して、対称性（$a \le b \vdash b \le a$）を導出してしまうからであり、これは指向付き論理では無効である。以前の指向付き型理論への試みは、特に証明無関係な論理（等式が型ではなく命題であり、複数の要素を持たない場合）の文脈において、これらの極性制約に直面して苦慮してきた。

2. 手法

著者らは、Lawvere の超教義（hyperdoctrines）の枠組みを一般化することにより、指向付き第一階論理（dFOL）とその教義的意味論を開発する。

構文：極性付き文脈

構文は、変数をその変異性に基づいて 3 つの集合に分割する極性付き文脈 $[\Theta \mid \Delta \mid \Gamma]$ を導入する。

• $\Theta$（負）: 反変位置にのみ現れる変数。
• $\Gamma$（正）: 共変位置にのみ現れる変数。
• $\Delta$（ダイ自然）: 両方の位置に現れる変数（またはそのように扱われることを許容される変数）。

主要な構文的特徴は以下の通りである。

• 指向付き等式（$\le_A$）: 負の文脈で型付けされた $s$ と正の文脈で型付けされた $t$ に対する原始関係 $s \le_A t$。
• 極性付き含意: 含意 $\psi \Rightarrow \phi$ は、$\psi$ の文脈の極性を反転させる（turnstile の左から右へ移動させる）。これは第一引数の反変性を反映する。
• 極性付き量化子: 量化子（$\forall^p, \exists^p$）は、束縛変数の変異性を追跡するために極性 $p \in \{-, \Delta, +\}$ でインデックス付けされる。
• 代入規則: 特殊な代入メカニズム（定義 2.7）が、極性付き文脈間での項の再インデックス付けを処理し、ダイ自然変数が一貫して代入されることを保証する。

意味論：指向付き教義

意味論は、Lawvere の教義を一般化した指向付き教義を通じて捉えられる。

• 基底圏: 標準的な型の圏の代わりに、基底は極性化圏 $ndp(\mathcal{C})$ であり、その対象は三つ組 $(\Theta, \Delta, \Gamma)$ であり、射は変異構造を尊重する。
• ファイバー構造: 関手 $P: ndp(\mathcal{C})^{op} \to \mathbf{Pos}$ が、極性付き文脈を命題の半順序集合に写像する。
• 主要な条件:
  • ダイ自然変異性の欠如（ndv）: 述語におけるダイ自然変数が、正と負の変数を縮約することからのみ生じることを保証する条件。これにより、「第三の」変異性のタイプが防止される。
  • 相対随伴: 指向付き等式は、標準的な左随伴ではなく、反対極性の 2 つの変数を単一のダイ自然変数に縮約する縮約のような操作に対する左相対随伴として特徴づけられる。これは対称性の導出を防止する構文的制限を捉える。
  • 極性付き含意: 相対右随伴として特徴づけられる。

3. 主要な貢献

1. dFOL の構文: ダイ自然性から着想を得た厳密な極性システムを備えた、指向付き等式を伴う第一階論理のための精密な自然演繹系。この系は、標準的な論理結合子を維持しつつ、指向付き等式に対する対称性の導出を明示的に禁止する。
2. 指向付き等式の特徴づけ: 本論文は、Lawvere の「等式は左随伴である」という概念を、指向付き等式は左相対随伴であるという形に一般化する。これは、関係の非対称性を考慮した、指向付き等式のための精密な圏論的普遍性質を提供する。
3. 指向付き教義: 意味論的枠組みとしての指向付き教義の導入。著者らは、dFOL の構文がこの意味論に対して健全かつ完全であることを証明する。
4. 半順序集合完全性: 半順序集合（$\mathbf{Preord}$）の標準モデルに対する、dFOL の古典的部分に関する特定の完全性結果が証明される。これにより、すべての半順序集合モデルで有効な帰結は、構文において導出可能であることが確立される。
5. 極性の処理: 本論文は、証明無関係な設定で変異性をどのように管理するかを示す。これは、$\mathbf{Cat}$ などの証明関連指向付き型理論とは区別され、半順序ファイバーと半順序値ファイバーを使用することによって達成される。

4. 結果

• 健全性と完全性: 著者らは、理論の圏（$\mathbf{Theory}$）と指向付き教義の 2-圏（$\mathbf{DDoctrine}$）の間の双随伴を確立する。これは、dFOL が指向付き教義の内部言語であることを意味する。
• 半順序集合に対する完全性: 極性付き文脈に適応された Henkin 様式の構成を用いて、dFOL の古典的部分が半順序集合モデルに対して完全であることが証明される。この構成は、モデルの定義域を、指向付き等式（$\le_A$）の導出可能性によって順序付けられた閉項の集合として定義する。
• 導出規則: この系は、指向付き等式の推移律、反射律、合同性に関する導出規則、および極性付き量化子と含意の間の相互作用規則をサポートする。
• 反例: 対称性（$a \le b \vdash b \le a$）が導出不可能であることを示すため、本論文は反例を提示する。半順序集合モデルは、そのような導出に対する反モデルとして機能する。

5. 意義と主張

本論文は、論理における変異性と Hom-関手の役割に関する Lawvere の業績を進展させると主張する。具体的には：

• 証明無関係な設定における指向付き等式に対する精密な構文的・意味論的特徴づけを提供し、古典論理と指向付き型理論の間のギャップを埋める。
• 相対随伴を通じて、等式を随伴とするという概念を指向付きケースに一般化し、指向付き構造を理解するための新たな圏論的ツールを提供する。
• 複雑な幾何学的または高次圏論的機械を必要とするのではなく、極性付き文脈を通じて極性を慎重に管理することにより、指向付き論理を（Henkin 完全性のような）標準的な論理技術で扱えることを示す。
• この作業は、ホモトピー型理論の証明関連アプローチとは区別される、論理的枠組み内での書き換えシステムおよび指向付き現象（プロセス、遷移）の推論のための基礎的ステップとして位置づけられる。

著者らは明示的に、焦点が証明無関係なケースにあると述べている。これは、書き換え論理の性質（書き換えが発生するか否かのいずれかである）および圏論的論理における半順序ファイバーの使用によって正当化される。彼らは、依存指向付き型理論の完全な複雑さを解決するとは主張せず、第一階・半順序集合ベースのケースに対する堅牢な基礎を提供するに留まる。