On the Existence of Optimal Propositional Proof Systems and Oracle-relativized Propositional Logic
We investigate suucient conditions for the existence of optimal propositional proof systems. We concentrate on conditions of the form CoNF = NF. We introduce a purely combinatorial property of complexity classes-the notions of slim vs. fat classes. These notions partition the collection of all previously studied time-complexity classes into two complementary sets. We show that for every slim class an appropriate collapse entails the existence of an optimal propositional proof system. On the other hand, we introduce a notion of a propositional proof system relative to an oracle and show that for every fat class there exists an oracle relative to which such an entailment fails. As the classes P (polynomial functions), E (2 O(n) functions) and EE (2 O(2 n) functions) are slim, this result includes all the previously known suuciency conditions for the existence of optimal propositional proof systems. On the other hand, the classes N EX P, QP (the class of quasi-polynomial functions) and EEE (2 O(2 2 n) functions), as well as any other natural time-complexity class which is not covered by our suuciency result, are fat classes. As the proofs of all the known suuciency conditions for the existence of optimal propositional proof systems carry over to the corresponding oracle-relativized notions, our oracle result shows that no extension of our suuciency condition to non-slim classes can be obtained by the type of reasoning used so far in proofs on these issues.