結構規則

在證明論中，結構規則是不提及任何邏輯連結詞的推理規則，它直接操作於判斷或相繼式。結構規則通常模仿邏輯的元理論性質。拒絕一個或多個結構規則的邏輯被歸類為亞結構邏輯。

常見結構規則[編輯]

{\frac {\Gamma \vdash \Sigma }{\Gamma ,A\vdash \Sigma }}

在十字轉門的左側，和

{\frac {\Gamma \vdash \Sigma }{\Gamma \vdash A,\Sigma }}

在右側。

{\frac {\Gamma ,A,A\vdash \Sigma }{\Gamma ,A\vdash \Sigma }}

和

{\frac {\Gamma \vdash A,A,\Sigma }{\Gamma \vdash A,\Sigma }}

{\frac {\Gamma _{1},A,\Gamma _{2},B,\Gamma _{3}\vdash \Sigma }{\Gamma _{1},B,\Gamma _{2},A,\Gamma _{3}\vdash \Sigma }}

和

{\frac {\Gamma \vdash \Sigma _{1},A,\Sigma _{2},B,\Sigma _{3}}{\Gamma \vdash \Sigma _{1},B,\Sigma _{2},A,\Sigma _{3}}}

。(這也叫做排列規則)。

沒有任何上述結構規則的邏輯將把相繼式解釋為純粹的序列；帶有交換規則它們就是多重集；帶有緊縮和交換規則二者它們就是集合。

最著名的結構規則叫做切。證明論理論家花了相當的努力來證實切規則在各種邏輯中是多餘的。更嚴格的說，證實了切只是(某種意義上)簡化證明的工具，不能增加可以證明的定理。成功消除了切規則叫做切消定理，直接有關於規範化計算(參見lambda 演算)的哲學；它經常對給定邏輯的判定的複雜性給出好的指示。