Benzmueller, Christoph and Brown, Chad E. and Kohlhase, Michael - Cut-Simulation and Impredicativity

lmcs:1144 - Logical Methods in Computer Science, March 3, 2009, Volume 5, Issue 1
Cut-Simulation and Impredicativity

Authors: Benzmueller, Christoph and Brown, Chad E. and Kohlhase, Michael

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.


Source : oai:arXiv.org:0902.0043
DOI : 10.2168/LMCS-5(1:6)2009
Volume: Volume 5, Issue 1
Published on: March 3, 2009
Submitted on: January 10, 2007
Keywords: Computer Science - Logic in Computer Science,Computer Science - Artificial Intelligence,F.4.1,I.2.3


Share

Consultation statistics

This page has been seen 52 times.
This article's PDF has been downloaded 9 times.