Authors: Christoph Benzmueller ; Chad E. Brown ; Michael Kohlhase

We investigate cut-elimination and cut-simulation in impredicative (higher-order) logics. We illustrate that adding simple axioms such as Leibniz equations to a calculus for an impredicative logic -- in our case a sequent calculus for classical type theory -- is like adding cut. The phenomenon equally applies to prominent axioms like Boolean- and functional extensionality, induction, choice, and description. This calls for the development of calculi where these principles are built-in instead of being treated axiomatically.

Comment: 21 pages

• 03B35 - Mechanization of proofs and logical operations
• 03F05 - Cut-elimination and normal-form theorems