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

Abstract

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 propositional logic . This fact provides an argument in favor that any classical propositional tautology has short proofs, i.e., NP=CoNP.

This paper has been withdrawn by the author due to a fatal error in the general form of the deduction used for proved the main proposition

References in corpus (1)

• Propositional Logics Complexity and the Sub-Formula Property

Cited by in corpus (2)

• Going from the huge to the small: Efficient succinct representation of proofs in Minimal implicational logic
• Yet another argument in favour of NP=CoNP