On the expressive power of implication in classical propositional logic

In this paper we illustrate the expressive power of implication in classical propositional logic (CPC) by reworking the NP-hardness proof of the SAT problem from the point of view of implication as the primary connective. As a result two natural normal forms of implicational formulas emerge: conjunctions of implications CINF and INF where only implication and negation is used. Also, we provide a new, entirely proof-theoretic, demonstration of the result of Stålmarck that the classical validity problem for purely implicational formulas is co-NP-complete. Our approach uses a new focused proof system for the implicational fragment of CPC and illustrates both the proof-theoretic and automata-theoretic aspects of classical implication.