Logic seminar

Proof complexity of intuitionistic implicational formulas

We study implicational formulas in the context of proof complexity of intuitionistic 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 Hrubes [1], generalized to exponential separation between EF and SF systems in superintuitionistic logics of unbounded branching by Jerabek [2], can be realized by implicational tautologies. [1] P. Hrubes, A lower bound for intuitionistic logic, Annals of Pure and Applied Logic 146 (2007), 72--90. [2] E. Jerabek, Substitution Frege and extended Frege proof systems in non-classical logics, Annals of Pure and Applied Logic 159 (2009), 1--48.