割切消除定理

割切消除定理，也称为“Hauptsatz”（根岑 1969），指出每个后承演算推导都可以转换为另一个具有相同终结式（底部后承式）且其中不出现割切规则的推导。

所有没有割切的推导都具有子公式属性，即推导中出现的所有公式都是来自终结式的公式的子公式。

该定理的强化形式适用于后承演算的经典变体。这种形式指出，任何推导都可以转换为另一个具有相同终结式并具有以下属性的推导。

1. 它没有割切。

2. 它包含一个所谓的中间后承式，其推导不包含和，并且在中间后承式下方推导中出现的唯一推理规则是和规则和结构规则。