在逻辑学中, 顺序逻辑是亚结构逻辑的一种, 不假设任何结构性规则.
因此, 在线性逻辑的基础上, 顺序逻辑将线性的蕴涵关系 A⊸B 分裂为两种: 左蕴涵 A↣B 和右蕴涵 B↠A. 在 Ω⊢B 且 A∈Ω 的情况下, A 左蕴涵还是右蕴涵 B 取决于 A 在 Ω 的最左边还是最右边.
注 0.1. 在 [Lambek 1958] 原文中, 左右蕴涵的符号如下: AA↣B↠B对应 A对应 B\B/A
本文使用的是 Frank Pfenning 版本的符号, 该版本没有改变左右操作符的顺序, 且更加接近某种 “箭头”, 和 ⊸ 类似.
目录1逻辑连接词2规则3应用文法解析4参考文献1逻辑连接词
参见: 逻辑连接词
顺序逻辑中的命题使用形式文法定义如下:
A,B::=∣∣A•B∣A↣B∣A↠BA⊕B∣A&B1∣⊤∣0
除此之外还有类比左右蕴涵的一种反过来的 A•B, 记作 A∘B (读作 “反接”), 它完全等价于 B•A, 因此基本上可以说是冗余的, 不再赘述.
2规则 对于相继式 Ω⊢A, 若某规则对 Ω 中的连接词进行消除, 那么称之为左规则, 反之则称之为右规则.
顺序逻辑中使用相继式演算风格的规则定义如下, 用 Ω 代表语境. 若有多个语境, 则使用下标区分. 若要使用自然演绎, 请参见相继式演算–自然演绎类比.
•
与对应的连接词 A•B (读作 “A 接 B”):
Ω1,Ω2⊢A•BΩ1⊢AΩ2⊢BΩ1,A•B,Ω2⊢CΩ1,A,B,Ω2⊢C
•
左蕴涵:
Ω⊢A↣BA,Ω⊢BΩL,ΩA,A↣B,ΩR⊢CΩA⊢AΩL,B,ΩR⊢C
•
右蕴涵:
Ω⊢A↠BΩ,A⊢BΩL,A↠B,ΩA,ΩR⊢CΩA⊢AΩL,B,ΩR⊢C
后续的规则类似线性逻辑, 只是额外有顺序限制而已, 一并列出.
Ω⊢A&BΩ⊢AΩ⊢BΩL,A&B,ΩR⊢CΩL,A,ΩR⊢CΩL,A&B,ΩR⊢CΩL,B,ΩR⊢C
Ω⊢A⊕BΩ⊢AΩ⊢A⊕BΩ⊢BΩL,A⊕B,ΩR⊢CΩL,A,ΩR⊢CΩL,B,ΩR⊢C
⊢1ΩL,1,ΩR⊢CΩL,ΩR⊢C
Ω⊢⊤ΩL,0,ΩR⊢C
另见: 切规则
3应用
文法解析 顺序逻辑可以用于语境无关文法的解析, 它天生就对前后顺序敏感, 因此语境无关文法可以轻易地翻译成某种顺序逻辑.
例 3.1. 如下文法描述了 “成对匹配的括号” 构成的语言: S::={S}∣{}∣SS例如字符串 {{}}{} 可以如此匹配: S→SS→{S}{}→{{}}{}该文法可以用如下规则描述: S{}S{S}SSS其中, 两种括号、S 都看作逻辑命题, 字符串可以看作一组公式或者说逻辑意义上的语境, 若某字符串能推出单个的 S, 则可以说它属于该语言.
4参考文献 •
Joachim Lambek (1958). “The mathematics of sentence structure”.
逻辑学基本概念命题 • 真值 • 相继式、判断、推导规则 • 逻辑连接词 • 逻辑和谐命题逻辑真、假 • 或、与、非、蕴涵 • 排中律 • Heyting 代数、Boole 代数谓词逻辑一阶逻辑 • 一阶语言 • 一阶理论 • 二阶逻辑 • 高阶逻辑 • 谓词 • 全称量词、存在量词模型论模型 • Gödel 完备性定理 • 紧性定理 • 量词消去亚结构逻辑线性逻辑 • 相关逻辑 • 仿射逻辑 • 顺序逻辑 • 伴随逻辑[查看模板]
术语翻译
顺序逻辑 • 英文 order logic • 日文 非可換論理
A 左蕴涵 B (Lambek 原版记号) • 英文 A under B
A 右蕴涵 B (Lambek 原版记号) • 英文 B over A
A 接 B • 英文 A fuse B
A 反接 B • 英文 A twist B