Cut-Simulation in Impredicative Logics

Abstract. 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.

• Type: Conference
• Year: 2006
• Where: CADE
• Authors: Christoph Benzmüller, Chad E. Brown, Michael Kohlhase
• Keywords: Automated Reasoning, CADE 2006, Prominent Axioms, Sequent Calculus, Simple Axioms