We give a simple and direct proof that super-consistency implies the cut elimination property in deduction modulo. This proof can be seen as a simplification of the proof that super-consistency implies proof normalization. It also takes ideas from the semantic proofs of cut elimination that proceed by proving the completeness of the cut-free calculus. As an application, we compare our work with the cut elimination theorems in higher-order logic that involve V-complexes.

翻译：我们给出一个简单且直接的证明，证明超一致性在模演绎中蕴含切消除性质。该证明可视为超一致性蕴含证明归一化定理的简化版本，同时借鉴了通过证明无切演算完全性来推导切消除的语义证明思想。作为应用，我们将此工作与涉及V-复合体的高阶逻辑切消除定理进行了比较。