On an optimal propositional proof system and the structure of easy subsets of TAUT

AbstractIn this paper we develop a connection between optimal propositional proof systems and structural complexity theory—specifically, there exists an optimal propositional proof system if and only if there is a suitable recursive presentation of the class of all easy (polynomial time recognizable) subsets of TAUT. As a corollary we obtain the result that if there does not exist an optimal propositional proof system, then for every theory T there exists an easy subset of TAUT which is not T-provably easy