Hard tautologies and optimal proof systems
Jan Krajı́ček · Cambridge University Press eBooks · 1995
We shall study in this chapter the topic of hard tautologies: tautologies that are candidates for not having short proofs in a particular proof system. The closely related question is whether there is an optimal propositional proof system, that is, a proof system P such that no other system has more than a polynomial speed-up over P . We shall obtain a statement analogous to the NP-completeness results characterizing any propositional proof system as an extension of EF by a set of axioms of particular form. Recall the notions of a proof system and p -simulation from Section 4.1, the definitions of translations of arithmetic formulas into propositional ones in Section 9.2, and the relation between reflection principles (consistency statements) and p -simulations established in Section 9.3. We shall also use the notation previously used in Chapter 9. Finitistic consistency statements and optimal proof systems We shall denote by Taut ( x ) the formula Taut 0 ( x ) from Section 9.3 defining the set of the (quantifierfree) tautologies, denoted TAUT itself. Recall from Section 9.2 the definition of the translation producing from a formula a sequence of propositional formulas (Definition 9.2.1, Lemma 9.2.2).