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

lmcs:1144 - Logical Methods in Computer Science, March 3, 2009, Volume 5, Issue 1 - https://doi.org/10.2168/LMCS-5(1:6)2009
Cut-Simulation and Impredicativity

Authors: Christoph Benzmueller ; Chad E. Brown ; Michael Kohlhase

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.


Volume: Volume 5, Issue 1
Published on: March 3, 2009
Accepted on: June 25, 2015
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 276 times.
This article's PDF has been downloaded 120 times.