查看“亚结构逻辑”的源代码

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

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

:<math>\Gamma\vdash\Sigma</math>。

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

:<math>\mathcal A,\mathcal B \vdash\mathcal C</math>

读做

:(''A'' '''与'''''B'')'''蕴涵'''''C''。

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

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

:<math>\mathcal B,\mathcal A\vdash\mathcal C</math>

演绎自

:<math>\mathcal A,\mathcal B\vdash\mathcal C</math>。

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

:<math> \Gamma,\mathcal A,\mathcal A,\Delta\vdash\mathcal C</math>

我们可以演绎出

:<math> \Gamma,\mathcal A,\Delta\vdash\mathcal C</math>。

还有从 

:<math> \Gamma,\mathcal A,\Delta\vdash\mathcal C</math>

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

:<math> \Gamma,\mathcal A,\mathcal B,\Delta\vdash\mathcal C</math>。

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

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

== 外部链接 ==

* [http://plato.stanford.edu/entries/logic-substructural/ Article on ''Substructural logics''] at the [[Stanford Encyclopedia of Philosophy]]

[[Category:亚结构逻辑|*]]
[[Category:形式逻辑系统]]