查看“︁结构规则”︁的源代码

在[[证明论]]中，'''结构规则'''是不提及任何[[逻辑连结词]]的[[推理规则]]，它直接操作于判断或[[相继式]]。结构规则通常模仿逻辑的元理论性质。拒绝一个或多个结构规则的逻辑被归类为[[亚结构逻辑]]。

==常见结构规则==
* '''弱化'''，这里的[[相继式]]的假设或结论可以扩展到额外的数目。在符号形式中弱化规则可以写为
:<math>\frac{\Gamma \vdash \Sigma}{\Gamma, A \vdash \Sigma}</math> 在[[十字转门]]的左侧，和
:<math>\frac{\Gamma \vdash \Sigma}{\Gamma \vdash A, \Sigma}</math> 在右侧。
* '''紧缩'''，这里的在相继式同一侧两个相等的(或可合一的)成员可以替代为单一的一个成员(或公共实例)。符号化为:
:<math>\frac{\Gamma, A, A \vdash \Sigma}{\Gamma, A \vdash \Sigma}</math> 和
:<math>\frac{\Gamma \vdash A, A, \Sigma}{\Gamma \vdash A, \Sigma}</math>。在使用[[归结原理]]的[[自动定理证明]]中也叫做'''因子化'''。在[[经典逻辑]]中称为[[蕴含的幂等性]]。
* '''交换'''，这里的在相继式同一侧的两个成员可以对换。符号化为:
:<math>\frac{\Gamma_1, A, \Gamma_2, B, \Gamma_3 \vdash \Sigma}{\Gamma_1, B, \Gamma_2, A, \Gamma_3 \vdash \Sigma}</math> 和
:<math>\frac{\Gamma \vdash \Sigma_1, A, \Sigma_2, B, \Sigma_3}{\Gamma \vdash \Sigma_1, B, \Sigma_2, A, \Sigma_3}</math>。(这也叫做''排列规则'')。

没有任何上述结构规则的逻辑将把相继式解释为纯粹的[[序列]]；带有交换规则它们就是[[多重集]]；带有紧缩和交换规则二者它们就是[[集合 (数学)|集合]]。

最著名的结构规则叫做'''[[切消定理|切]]'''。证明论理论家花了相当的努力来证实切规则在各种逻辑中是多余的。更严格的说，证实了切只是(某种意义上)简化证明的工具，不能增加可以证明的定理。成功消除了切规则叫做'''[[切消定理]]'''，直接有关于规范化[[计算]](参见[[lambda 演算]])的哲学；它经常对给定逻辑的[[判定]]的[[复杂性]]给出好的指示。

==参见==
*[[相继式演算]]
*[[亚结构逻辑]]
*[[线性逻辑]]
*[[仿射逻辑]]
*[[严格逻辑]]
*[[有序逻辑]]

[[Category:证明论]]
[[Category:推理规则]]