亚结构逻辑

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

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

${\displaystyle \Gamma \vdash \Sigma }$。

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

${\displaystyle {\mathcal {A}},{\mathcal {B}}\vdash {\mathcal {C}}}$

读做

(A 与B)蕴涵C。

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

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

${\displaystyle {\mathcal {B}},{\mathcal {A}}\vdash {\mathcal {C}}}$

演绎自

${\displaystyle {\mathcal {A}},{\mathcal {B}}\vdash {\mathcal {C}}}$。

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

${\displaystyle \Gamma ,{\mathcal {A}},{\mathcal {A}},\Delta \vdash {\mathcal {C}}}$

我们可以演绎出

${\displaystyle \Gamma ,{\mathcal {A}},\Delta \vdash {\mathcal {C}}}$。

还有从

${\displaystyle \Gamma ,{\mathcal {A}},\Delta \vdash {\mathcal {C}}}$

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

${\displaystyle \Gamma ,{\mathcal {A}},{\mathcal {B}},\Delta \vdash {\mathcal {C}}}$。

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

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

外部链接

• Article on Substructural logics（页面存档备份，存于互联网档案馆） at the Stanford Encyclopedia of Philosophy