Proof complexity of intuitionistic implicational formulas

TL;DR

This paper explores the proof complexity of implicational formulas in intuitionistic logic, showing efficient transformations and polynomial simulations between proof systems, with implications for lower bounds and separations.

Contribution

It introduces an efficient transformation of tautologies to implicational tautologies and demonstrates polynomial simulation of full intuitionistic logic by implicational fragments.

Findings

Polynomial simulation of full IPC by implicational fragments in EF proofs

Efficient transformation of tautologies preserving proof lengths

Application of lower bounds and separations to implicational tautologies

Abstract

We study implicational formulas in the context of proof complexity of intuitionistic propositional logic (IPC). On the one hand, we give an efficient transformation of tautologies to implicational tautologies that preserves the lengths of intuitionistic extended Frege (EF) or substitution Frege (SF) proofs up to a polynomial. On the other hand, EF proofs in the implicational fragment of IPC polynomially simulate full intuitionistic logic for implicational tautologies. The results also apply to other fragments of other superintuitionistic logics under certain conditions. In particular, the exponential lower bounds on the length of intuitionistic EF proofs by Hrube\v{s} \cite{hru:lbint}, generalized to exponential separation between EF and SF systems in superintuitionistic logics of unbounded branching by Je\v{r}\'abek \cite{ej:sfef}, can be realized by implicational tautologies.