伴随逻辑

在逻辑学中, 伴随逻辑是亚结构逻辑的一种, 不直接假设任何结构性规则, 而是对其进行控制.

考虑某种融合了线性逻辑和结构逻辑中的命题的新逻辑, 其中拥有将两种命题互相转化的能力. 对于线性命题 $A$, 令 $\uparrow A$ 为满足结构性规则版本的 $A$; 再引入反向的操作 $\downarrow A$, 就得到了简单的伴随逻辑. 由于 $\uparrow A$ 满足结构规则, 我们可以将其复制 (借助收缩规则) 多份再转回线性逻辑. 在这基础上, 可以引发一些思考:

•	站在 Curry–Howard 对应的视角看待逻辑的话, 线性逻辑可以看作是操作资源的程序, 而结构逻辑可以看作是某种元程序, $\uparrow$ 和 $\downarrow$ 就对应了某种程序的翻译过程.

•	线性逻辑中代表命题满足结构规则的$!$ 模态可以这样定义: $$!A::=\downarrow \uparrow A$$这可以解释 $!$ 的极性: 由于 $\uparrow$ 是负的、$\downarrow$ 是正的, 因此两者复合后既不是正的也不是负的.

伴随逻辑将这种情况推广到允许多种逻辑融合的情况, 而 $\uparrow ,\downarrow$ 两个运算符也要带上参数, 指定它从哪个逻辑发送到哪个逻辑.

1逻辑连接词

注 1.1. 本文不考虑顺序逻辑, 换言之, 在整个伴随逻辑的框架下, 我们都假设交换规则成立. 若要支持去掉该规则, 可能会引入过多的逻辑连接词, 不利于展示核心想法.

给定拟序集 $(V,\le )$, 伴随逻辑中的命题使用形式文法定义如下, 其中 $l,m,k\in V$, 且 $l\ge m\ge k$:

$$\begin{array}{rl}{A}_m,B_m::=& A_m\to B_m\mid A_m\ast B_m\\ \mid & A_m+B_m\mid A_m\&B_m\\ \mid & 1\mid \top \mid 0\mid p_m\\ \mid & {\uparrow }_k^m{A}_k\mid {\downarrow }_m^l{A}_l\end{array}$$

其中:

•	$m,k,l$ 代表某种模态, 例如 “满足某结构性规则”,
•	$p_m$ 代表模态 $m$ 下自带的命题.

定义函数 $\sigma (m)\subseteq \{W,C\}$, 其中 $m\in V$ 是模态, $\sigma (m)$ 代表该模态对应的逻辑支持的结构性规则, $W$ 代表弱化规则、$C$ 代表收缩规则.

2伴随相继式演算规则

对于相继式 $\Delta ⊢A$, 若某规则对 $\Delta$ 中的连接词进行消除, 那么称之为左规则, 反之则称之为右规则.

伴随逻辑中的规则使用相继式演算风格的规则定义如下, 用 $\Delta$ 代表语境.

•	结构性规则: $$\frac{W\in \sigma (m)\Delta ⊢C_r}{\Delta ,A_m⊢C_r}\frac{C\in \sigma (m)\Delta ,A_m,A_m⊢C_r}{\Delta ,A_m⊢C_r}$$

•	和谐规则: $$\frac{}{A_m⊢A_m}\frac{\Delta \ge m\ge r\Delta ⊢A_m{\Delta }^{\prime },A_m⊢C_r}{\Delta ,{\Delta }^{\prime }⊢C_r}$$

•	伴随规则: $$\frac{\Delta ⊢A_k}{\Delta ⊢{\uparrow }_k^m{A}_k}\frac{k\ge r\Delta ,A_k⊢C_r}{\Delta ,{\uparrow }_k^m{A}_k⊢C_r}\frac{\Delta \ge l\Delta ⊢A_l}{\Delta ⊢{\downarrow }_m^l{A}_l}\frac{\Delta ,A_l⊢C_r}{\Delta ,{\downarrow }_m^l{A}_l⊢C_r}$$

•	蕴涵: $$\frac{\Delta ,A_m⊢B_m}{\Delta ⊢A_m\to B_m}\frac{\Delta \ge m\Delta ⊢A_m{\Delta }^{\prime },B_m⊢C_r}{\Delta ,{\Delta }^{\prime },A_m\to B_m⊢C_r}$$

•	与, 极性为负: $$\frac{\Delta ⊢A_m{\Delta }^{\prime }⊢B_m}{\Delta ,{\Delta }^{\prime }⊢A_m\times B_m}\frac{\Delta ,A_m,B_m⊢C_r}{\Delta ,A_m\times B_m⊢C_r}$$

•	与, 极性为正: $$\frac{\Delta ⊢A_m\Delta ⊢B_m}{\Delta ⊢A_m\&B_m}\frac{\Delta ,A_m⊢C_r}{\Delta ,A_m\&B_m⊢C_r}\frac{\Delta ,B_m⊢C_r}{\Delta ,A_m\&B_m⊢C_r}$$

•	或: $$\frac{\Delta ⊢A_m}{\Delta ⊢A_m+B_m}\frac{\Delta ⊢B_m}{\Delta ⊢A_m+B_m}\frac{\Delta ,A_m⊢C_r\Delta ,B_m⊢C_r}{\Delta ,A_m+B_m⊢C_r}$$

其余规则较为简单, 一并列出:

$$\frac{}{⊢1}\frac{\Delta ⊢C_r}{\Delta ,1⊢C_r}\frac{}{\Delta ⊢\top }\frac{}{\Delta ,0⊢C_r}$$

3伴随自然演绎规则

参考 [Jang–Roshal–Pfenning–Pientka 2024].

另见相继式演算–自然演绎类比.

4参考文献

•	Klaas Pruiksma, William Chargin, Frank Pfenning, Jason Reed (2018). “Adjoint Logic”.
•	Junyoung Jang, Sophia Roshal, Frank Pfenning, Brigitte Pientka (2024). “Adjoint Natural Deduction (Extended Version)”. arXiv: 2402.01428.

术语翻译

伴随逻辑 • 英文 adjoint logic