Cut-simulation and impredicativity

Abstract

We investigate cut-elimination and cut-simulation in impredicative (higherorder) 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.