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

    2 Documents citing this article

    Share

    Consultation statistics

    This page has been seen 357 times.
    This article's PDF has been downloaded 167 times.