跳转到内容

亚结构逻辑

维基百科,自由的百科全书

这是亚结构逻辑当前版本,由InternetArchiveBot留言 | 贡献编辑于2020年12月15日 (二) 22:37 (补救1个来源,并将0个来源标记为失效。) #IABot (v2.0.7)。这个网址是本页该版本的固定链接。

(差异) ←上一修订 | 最后版本 (差异) | 下一修订→ (差异)

数理逻辑中,特别是联合上证明论的时候,一些亚结构逻辑已经作为比常规系统弱的命题演算系统被介入了。同常规系统的不同之处在于它们有更少的结构规则可用:结构规则的概念是基于相继式(sequent)表达,而不是自然演绎的公式化表达。两个重要的亚结构逻辑是相干逻辑线性逻辑

相继式演算中,你可以把证明的每一行写为

这里的结构规则是重写相继式左手端的Γ的规则,Γ是最初被构想为命题的字符串。这个字符串的标准解释是合取式:我们希望把相继式符号

读做

(A B)蕴涵C

这里我们把右手端的Σ采纳为一个单一的命题C(这是直觉主义风格的相继式);但是所有的东西都同样的适用于一般情况,因为所有的操作都发生在十字转门(turnstile)符号的左边。

因为合取是交换性结合性的操作,相继式理论的形式架设通常包括相应的结构规则来重写相继式的Γ - 例如

演绎自

还有对应于合取特性的幂等性单调性的进一步的结构规则:从

我们可以演绎出

还有从

我们可以演绎出,对于任何B

线性逻辑中有重复的假设(hypothese)'被认为'不同于单一的出现,它排除了这两个规则。而相干逻辑只排除后者的规则,因为B明显的与结论无关。

这些是结构规则的基本例子。在应用到常规命题演算的时候,这些规则是没有任何争议的。它们自然的出现于证明理论中,并在那里被首次注意到(在获得一个名字之前)。

外部链接[编辑]