Cut-Simulation and Impredicativity

TL;DR

This paper explores how adding certain axioms to impredicative higher-order logics mimics the effect of cut rules, highlighting the need for calculi that incorporate these principles inherently.

Contribution

It demonstrates that common axioms in impredicative logics effectively function as cut rules, suggesting the development of calculi with built-in principles.

Findings

Adding axioms like Leibniz equations acts as cut in impredicative logics

Common axioms such as extensionality and induction mimic cut-elimination effects

Calls for calculi with built-in axioms rather than axiomatic addition

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.