Publication details

Saarland University Computer Science

Cut-Simulation and Impredicativity

Christoph Benzmueller, Chad E. Brown, Michael Kohlhase

Logical Methods in Computer Science 5(1:6):1-21, March 2009

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.

Available at LMCS

Show BibTeX               

Login to edit

Legal notice, Privacy policy