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

常見結構規則

編輯
  • 弱化,這裡的相繼式的假設或結論可以擴展到額外的數目。在符號形式中弱化規則可以寫為
 十字轉門的左側,和
  在右側。
  • 緊縮,這裡的在相繼式同一側兩個相等的(或可合一的)成員可以替代為單一的一個成員(或公共實例)。符號化為:
 
 。在使用歸結原理自動定理證明中也叫做因子化。在經典邏輯中稱為蘊含的冪等性
  • 交換,這裡的在相繼式同一側的兩個成員可以對換。符號化為:
 
 。(這也叫做排列規則)。

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

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

參見

編輯