伴随逻辑

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

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

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

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

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

1逻辑连接词

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

给定拟序集 , 伴随逻辑中的命题使用形式文法定义如下, 其中 , 且 :

其中:

代表某种模态, 例如 “满足某结构性规则”,

代表模态 下自带的命题.

定义函数 , 其中 是模态, 代表该模态对应的逻辑支持的结构性规则, 代表弱化规则 代表收缩规则.

2伴随相继式演算规则

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

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

结构性规则:

和谐规则:

伴随规则:

蕴涵:

, 极性为负:

, 极性为正:

:

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

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