An Exponential Lower Bound for Proofs in Focused Calculi

Abstract

In [7], Iemhoff introduced a special form of sequent-style rules and axioms, which she called focused, and studied the relationship between the focused proof systems, the systems only consisting of this kind of rules and axioms, and the uniform interpolation of the logic that the system captures. Subsequently, as a negative consequence of this relationship, she excludes almost all super-intuitionistic logics from having these focused proof systems. In this paper, we will provide a complexity theoretic analogue of her negative result to show that even in the cases that these systems exist, their proof-length would computationally explode. More precisely, we will first introduce two natural subclasses of focused rules, called $\mathrm {PPF}$ and $\mathrm {MPF}$ rules. Then, we will introduce some $\mathbf {CPC}$-valid ($\mathbf {IPC}$-valid) sequents with polynomially short tree-like proofs in the usual Hilbert-style proof system for classical logic, or equivalently $\mathbf {LK} + \mathbf {Cut}$, that have exponentially long proofs in the systems only consisting of $\mathrm {PPF}$ ($\mathrm {MPF}$) rules.

Supported by the ERC Advanced Grant 339691 (FEALORA) and by the grant 19-05497S of GA ČR.