Cut-Simulation and Impredicativity

DOI10.2168/LMCS-5(1:6)2009MaRDI QIDQ3623018zbMATH OpenFDO

Authors Christoph Benzmüller, Michael Kohlhase, Chad E. Brown

Publication date 29 April 2009

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/0902.0043

zbMATH Keywords

cut eliminationcut simulation impredicative higher-order logichigher-order proof automationsequent calculustype theory

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05)

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.

Recommendations

• Cut-Simulation in Impredicative Logics
• Cut Elimination in the Presence of Axioms
• A Constructive Semantic Approach to Cut Elimination in Type Theories with Axioms
• Cut elimination in the intuitionistic theory of types with axioms and rewriting cuts, constructively
• Cut elimination for a logic with induction and co-induction

Cited in

(8)

• Automating free logic in HOL, with an experimental application in category theory
• Cut-elimination for quantified conditional logic
• Extensional higher-order paramodulation in Leo-III
• Effective normalization techniques for HOL
• The higher-order prover \textsc{Leo}-II
• Proofs and reconstructions
• Cut-Simulation in Impredicative Logics
• Analytic tableaux for higher-order logic with choice

This page was built for publication: Cut-Simulation and Impredicativity

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3623018)