顺序逻辑

在逻辑学中, 顺序逻辑是亚结构逻辑的一种, 不假设任何结构性规则.

因此, 在线性逻辑的基础上, 顺序逻辑将线性的蕴涵关系 $A⊸B$ 分裂为两种: 左蕴涵 $A\rightarrowtail B$ 和右蕴涵 $B\twoheadrightarrow A$. 在 $\Omega ⊢B$ 且 $A\in \Omega$ 的情况下, $A$ 左蕴涵还是右蕴涵 $B$ 取决于 $A$ 在 $\Omega$ 的最左边还是最右边.

注 0.1. 在 [Lambek 1958] 原文中, 左右蕴涵的符号如下: $$\begin{array}{rlrl}A& \rightarrowtail B& 对应A& \backslash B\\ A& \twoheadrightarrow B& 对应B& /A\end{array}$$

本文使用的是 Frank Pfenning 版本的符号, 该版本没有改变左右操作符的顺序, 且更加接近某种 “箭头”, 和 $⊸$ 类似.

1逻辑连接词

参见: 逻辑连接词

顺序逻辑中的命题使用形式文法定义如下:

$$\begin{array}{rl}A,B::=& A•B\mid A\rightarrowtail B\mid A\twoheadrightarrow B\\ \mid & A\oplus B\mid A\&B\\ \mid & 1\mid \top \mid 0\end{array}$$

除此之外还有类比左右蕴涵的一种反过来的 $A•B$, 记作 $A\circ B$ (读作 “反接”), 它完全等价于 $B•A$, 因此基本上可以说是冗余的, 不再赘述.

2规则

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

顺序逻辑中使用相继式演算风格的规则定义如下, 用 $\Omega$ 代表语境. 若有多个语境, 则使用下标区分. 若要使用自然演绎, 请参见相继式演算–自然演绎类比.

•	与对应的连接词 $A•B$ (读作 “$A$ 接 $B$”): $$\frac{{\Omega }_1⊢A{\Omega }_2⊢B}{{\Omega }_1,{\Omega }_2⊢A•B}\frac{{\Omega }_1,A,B,{\Omega }_2⊢C}{{\Omega }_1,A•B,{\Omega }_2⊢C}$$

•	左蕴涵: $$\frac{A,\Omega ⊢B}{\Omega ⊢A\rightarrowtail B}\frac{{\Omega }_A⊢A{\Omega }_L,B,{\Omega }_R⊢C}{{\Omega }_L,{\Omega }_A,A\rightarrowtail B,{\Omega }_R⊢C}$$

•	右蕴涵: $$\frac{\Omega ,A⊢B}{\Omega ⊢A\twoheadrightarrow B}\frac{{\Omega }_A⊢A{\Omega }_L,B,{\Omega }_R⊢C}{{\Omega }_L,A\twoheadrightarrow B,{\Omega }_A,{\Omega }_R⊢C}$$

后续的规则类似线性逻辑, 只是额外有顺序限制而已, 一并列出.

$$\frac{\Omega ⊢A\Omega ⊢B}{\Omega ⊢A\&B}\frac{{\Omega }_L,A,{\Omega }_R⊢C}{{\Omega }_L,A\&B,{\Omega }_R⊢C}\frac{{\Omega }_L,B,{\Omega }_R⊢C}{{\Omega }_L,A\&B,{\Omega }_R⊢C}$$

$$\frac{\Omega ⊢A}{\Omega ⊢A\oplus B}\frac{\Omega ⊢B}{\Omega ⊢A\oplus B}\frac{{\Omega }_L,A,{\Omega }_R⊢C{\Omega }_L,B,{\Omega }_R⊢C}{{\Omega }_L,A\oplus B,{\Omega }_R⊢C}$$

$$\frac{}{⊢1}\frac{{\Omega }_L,{\Omega }_R⊢C}{{\Omega }_L,1,{\Omega }_R⊢C}$$

$$\frac{}{\Omega ⊢\top }\frac{}{{\Omega }_L,0,{\Omega }_R⊢C}$$

另见: 切规则

3应用

文法解析

顺序逻辑可以用于语境无关文法的解析, 它天生就对前后顺序敏感, 因此语境无关文法可以轻易地翻译成某种顺序逻辑.

例 3.1. 如下文法描述了 “成对匹配的括号” 构成的语言: $$\begin{array}{r}S::=\{S\}\mid \{\}\mid SS\end{array}$$例如字符串 $\{\{\}\}\{\}$ 可以如此匹配: $$S\to SS\to \{S\}\{\}\to \{\{\}\}\{\}$$该文法可以用如下规则描述: $$\frac{\{\}}{S}\frac{\{S\}}{S}\frac{SS}{S}$$其中, 两种括号、$S$ 都看作逻辑命题, 字符串可以看作一组公式或者说逻辑意义上的语境, 若某字符串能推出单个的 $S$, 则可以说它属于该语言.

4参考文献

•	Joachim Lambek (1958). “The mathematics of sentence structure”.

术语翻译

顺序逻辑 • 英文 order logic • 日文 非可換論理

$A$ 左蕴涵 $B$ (Lambek 原版记号) • 英文 $A$ under $B$

$A$ 右蕴涵 $B$ (Lambek 原版记号) • 英文 $B$ over $A$

$A$ 接 $B$ • 英文 $A$ fuse $B$

$A$ 反接 $B$ • 英文 $A$ twist $B$