Optimal Proof Systems for Propositional Logic and Complete Sets

摘要

A polymomial time computable function h: sigma sup * yieds sigma sup * whose range is the set of tautologies in Propositional Logic (TAUT), is called a proof system. Cook and Reckhow defined this concept in[5] and in order to ocmpare the relative strength of different proof systems, they considered the notion of p-simulation. Intutively a proof system h p-simulates a second one h' if there is a polynmial time computable function gamma translating proofs in h' into proofs in h. A proof system is called optimal if it p-simulates every other proof system. The question of whether p-optimal proof systems exist is an important one in the field. Krajicek and Pudlak[13,12] proved a sufficient condition for the existence of such optimal systems, showing that ifthe deterministic and nondeterministic exponential time classes coincide, then p-optimal proof systems exist. They also gave a condition implying the existence of optimal proof systems. In this paper we improve this result obtaining a weaker sufficient condition for this fact. We show that if a particular class of set with low information content in nondeterministic double exponential time is included in the corresponidng deterministic class, then p-optimal proof systems exist. Wealso show some complexity theoretical ocnsequences that follow from the assumption of the existence of p-optimal systems. We prove that if p-optimal systems exist then the class UP(and some other related complexity classes) have many-one complete languages, and that many-one complete sets for NP SPARSE follow from the existence of optimal proof systems.