技术摘要：定向一阶逻辑的教义语义

1. 问题陈述

本文解决了在逻辑框架内形式化定向等式的挑战。虽然 Lawvere 的范畴论视角成功地将经典等式刻画为收缩运算（contraction）的左伴随，但该方法依赖于对称性。在定向类型论中，类型被解释为范畴（或预序集）而非群胚（或集合），等式变为一种非对称关系（例如重写 $a \to b$ 或序关系 $a \le b$）。

核心难点在于处理方差（极性）。在定向设定下，变量可能出现在“负”位置（反变，例如态射的源）或“正”位置（协变，例如态射的目标）。标准的等式逻辑规则（自反性和 J-规则/消除规则）在此背景下失效，因为它们隐含地假设了对称性，或者允许变量同时以两种极性出现，从而推导出对称性（$a \le b \vdash b \le a$），这在定向逻辑中是无效的。以往对定向类型论的尝试往往难以处理这些极性约束，特别是在证明无关逻辑（其中等式是一个命题，而非拥有多个居民的类型）的背景下。

2. 方法论

作者通过推广 Lawvere 的超教义（hyperdoctrines）框架，开发了定向一阶逻辑（dFOL）及其教义语义。

语法：极性上下文

语法引入了极性上下文 $[\Theta \mid \Delta \mid \Gamma]$，根据方差将变量划分为三个集合：

• $\Theta$（负）： 仅出现在反变位置的变量。
• $\Gamma$（正）： 仅出现在协变位置的变量。
• $\Delta$（内自然）： 同时出现在两个位置（或被允许如此处理）的变量。

关键语法特征包括：

• 定向等式（$\le_A$）： 一个原始关系 $s \le_A t$，其中 $s$ 在负上下文中具有类型，而 $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）： 一个条件，确保谓词中的内自然变量仅源于正变量和负变量的坍缩，防止出现“第三种”方差类型。
  • 相对伴随： 定向等式不被刻画为标准左伴随，而是被刻画为左相对伴随，作用于一个类似收缩的运算，该运算将两个具有相反极性的变量坍缩为单个内自然变量。这捕捉了防止推导对称性的语法限制。
  • 极性蕴含： 被刻画为相对余伴随。

3. 主要贡献

1. dFOL 的语法： 一个精确的带定向等式的一阶逻辑自然演绎系统， featuring 一个受内自然性启发的严格极性系统。该系统明确禁止推导定向等式的对称性，同时保持标准逻辑连接词。
2. 定向等式的刻画： 本文将 Lawvere 的“等式即左伴随”推广为定向等式即左相对伴随。这为定向等式提供了精确的范畴普遍性质，解释了该关系的非对称性。
3. 定向教义： 引入定向教义作为语义框架。作者证明了 dFOL 的语法相对于该语义是可靠且完备的。
4. 预序完备性： 针对 dFOL 的经典片段，证明了相对于预序集（$\mathbf{Preord}$）标准模型的完备性结果。这确立了在任何预序模型中有效的任何蕴含都在语法中可推导。
5. 极性的处理： 本文展示了如何在证明无关的设定中管理方差，通过使用偏序纤维化（posetal fibrations）和偏序值纤维，将其与证明相关的定向类型论（如 $\mathbf{Cat}$ 中的那些）区分开来。

4. 结果

• 可靠性与完备性： 作者在理论范畴（$\mathbf{Theory}$）和定向教义 2-范畴（$\mathbf{DDoctrine}$）之间建立了一个双伴随（bi-adjunction）。这意味着 dFOL 是定向教义的内部语言。
• 预序的完备性： 利用适应极性上下文的 Henkin 风格构造，本文证明了 dFOL 的经典片段相对于预序模型是完备的。该构造将模型的定义域定义为闭项集，并按定向等式（$\le_A$）的可推导性进行排序。
• 导出规则： 该系统支持定向等式的传递性、自反性和同余的导出规则，以及极性量词与蕴含之间的交互规则。
• 反例： 本文说明了对称性（$a \le b \vdash b \le a$）是不可推导的，且预序模型作为此类推导的反模型。

5. 意义与主张

本文声称推进了 Lawvere 关于方差和 Hom-函子在逻辑中作用的工作。具体而言：

• 它在证明无关的设定中提供了定向等式的精确语法和语义刻画，填补了经典逻辑与定向类型论之间的空白。
• 它通过相对伴随将等式作为伴随的概念推广到定向情况，为理解定向结构提供了新的范畴工具。
• 它表明，通过极性上下文仔细管理极性，定向逻辑可以用标准逻辑技术（如 Henkin 完备性）来处理，而无需复杂的几何或高阶范畴机制。
• 该工作被定位为在逻辑框架内推理重写系统和定向现象（过程、转换）的基础步骤，区别于同伦类型论的证明相关方法。

作者明确指出，他们的重点是证明无关的情况，这由重写逻辑的性质（重写要么发生，要么不发生）以及范畴逻辑中偏序纤维化的使用所证明。他们并未声称解决依赖定向类型论的全部复杂性，而是为基于预序的一阶情况提供了坚实的基础。