| |
VOLUME 5, ISSUE 1, PAPER 6
|
Cut-Simulation and Impredicativity
|
©Christoph E. Benzmueller, The University of Cambridge
©Chad E. Brown, Saarland University
©Michael Kohlhase, International University Bremen
|
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.
|
Publication date: March 3, 2009
Full Text: PDF | PostScript
DOI: 10.2168/LMCS-5(1:6)2009
Hit Counts: 1985 |
 Creative Commons | |
