割切消除定理

割切消除定理，也稱為“Hauptsatz”（根岑 1969），指出每個後承演算推導都可以轉換為另一個具有相同終結式（底部後承式）且其中不出現割切規則的推導。

所有沒有割切的推導都具有子公式屬性，即推導中出現的所有公式都是來自終結式的公式的子公式。

該定理的強化形式適用於後承演算的經典變體。這種形式指出，任何推導都可以轉換為另一個具有相同終結式並具有以下屬性的推導。

1. 它沒有割切。

2. 它包含一個所謂的中間後承式，其推導不包含和，並且在中間後承式下方推導中出現的唯一推理規則是和規則和結構規則。