Every super-polynomial proof in purely implicational minimal logic has a polynomially sized proof in classical implicational propositional logic

Edward Hermann Haeusler

In this article we show how any formula A with a proof in minimal implicational logic that is super-polynomially sized has a polynomially-sized proof in classical implicational pro…