Survey of disjoint NP-pairs and relations to propositional proof systems <s> Verifiability: <s> Publisher Summary This chapter focuses on the length of proofs of finitistic consistency statements in first order theories. By the second incompleteness theorem of Godel, a sufficiently rich theory cannot prove its own consistency. The most interesting application of the lower bound is a more than elementary speed-up for the length of proofs in the Godel-Bernays (GB) relative to Zermelo–Fraenkel (ZF). The chapter discusses the length of formulas into the complexity. It is assumed that the proofs are coded by strings in a finite alphabet and the length of a proof is the length of the corresponding string. This is the most realistic measure. The weakest fragment of arithmetic that is used is Robinson's arithmetic. The chapter proves the lower bound on the length of proofs of finitistic consistency statements. <s> BIB001 </s> Survey of disjoint NP-pairs and relations to propositional proof systems <s> Verifiability: <s> For a finitely, axiomatized theory S one considers the statement that there is no proof of contradiction in S whose length is ≤n. The problem of the length of proofs of such statements is studied, in relation with problems of propositional proof systems <s> BIB002 </s> Survey of disjoint NP-pairs and relations to propositional proof systems <s> Verifiability: <s> In this paper we study the pairs (U,V) of disjoint NP-sets representable in a theory T of Bounded Arithmetic in the sense that T proves U intersection V = \emptyset. For a large variety of theories T we exhibit a natural disjoint NP-pair which is complete for the class of disjoint NP-pairs representable in T. This allows us to clarify the approach to showing independence of central open questions in Boolean complexity from theories of Bounded Arithmetic initiated in [1]. Namely, in order to prove the independence result from a theory T, it is sufficient to separate the corresponding complete NP-pair by a (quasi)poly-time computable set. We remark that such a separation is obvious for the theory S(S_2) + S Sigma^b_2 - PIND considered in [1], and this gives an alternative proof of the main result from that paper. [1] A. Razborov. Unprovability of lower bounds on circuit size in certain fragments of Bounded Arithmetic. To appear in Izvestiya of the RAN , 1994. <s> BIB003 </s> Survey of disjoint NP-pairs and relations to propositional proof systems <s> Verifiability: <s> A polynomial time computable function h : Σ* → Σ* whose range is a set L is called a proof system for L. In this setting, an h-proof for x ∈ L is just a string w with h(w) = x. Cook and Reckhow defined this concept in [13], and in order to compare the relative strength of different proof systems for the set TAUT of tautologies in propositional logic, they considered the notion of p-simulation. Intuitively, a proof system h' p-simulates h if any h-proof w can be translated in polynomial time into an h'-proof w' for h(w). We also consider the related notion of simulation between proof systems where it is only required that for any h-proof w there exists an h'-proof w' whose size is polynomially bounded in the size of w. A proof system is called (p-)optimal for a set L if it (p-)simulates every other proof system for L. The question whether p-optimal or optimal proof systems for TAUT exist is an important one in the field. In this paper we show a close connection between the existence of (p-)optimal proof systems and the existence of complete problems for certain promise complexity classes like UP, NP ∩ Sparse, RP or BPP. For this we introduce the notion of a test set for a promise class C and prove that C has a many-one complete set if and only if C has a test set T with a p-optimal proof system. If in addition the machines defining a promise class have a certain ability to guess proofs, then the existence of a p-optimal proof system for T can be replaced by the presumably weaker assumption that T has an optimal proof system. Strengthening a result from Krajicek and Pudlak [20], we also give sufficient conditions for the existence of optimal and p-optimal proof systems. <s> BIB004 </s> Survey of disjoint NP-pairs and relations to propositional proof systems <s> Verifiability: <s> We exhibit a relativized world where NP ∩ SPARSE has no complete sets. This gives the first relativized world where no optimal proof systems exist. ::: ::: We also examine under what reductions NP ∩ SPARSE can have complete sets. We show a close connection between these issues and reductions from sparse to tally sets. We also consider the question as to whether the NP ∩ SPARSE languages have a computable enumeration. <s> BIB005
The validity of a proof can be easily verified. Cook and Reckhow  formalized the intuitive notion of a proof system as follows: A propositional proof system (proof system for short) is a total function f : Σ * → TAUT such that f is onto and polynomial-time-computable. (TAUT denotes the set of tautologies.) For any tautology φ, if f (w) = φ, then w is a proof in the system f (f -proof) showing that φ is a tautology. That the validity of proofs is easy to verify is formalized by the requirement that f is polynomialtime-computable. Furthermore, the definition requires that only tautologies have proofs (correctness) and that every tautology has a proof (completeness). The following function shows that the resolution calculus can be interpreted as a propositional proof system in the formal sense. and u is a resolution refutation of ¬φ φ : if w = (φ, u) and |u| ≥ 2 |φ| and φ is a tautology true : otherwise Note that in this definition, both lines, the first and the second one, are necessary. The first line makes sure that tautologies in disjunctive normal form have f -proofs not much longer than the corresponding resolution proofs. The second line takes care of all the tautologies that are not in disjunctive normal form. Note that in this line, the test for tautology can be done by exhaustive search in polynomial time, since 2 |φ| ≤ |w|. A propositional proof system f is not necessarily honest; it is possible that a formula φ ∈ TAUT has only exponentially long proofs w, i.e., f (w) = φ and |w| = 2 Ω(|φ|) . A proof system f is polynomially bounded if the function f is honest. Cook and Reckhow demonstrated that NP = coNP if and only if there exists a polynomially-bounded proof system, and they proposed attacking the question of whether NP equals coNP by studying propositional proof systems. Let f and f be two proof systems. We say that f simulates f if there is a polynomial p and a function h : Σ * → Σ * such that for every w ∈ Σ * , f (h(w)) = f (w) and |h(w)| ≤ p(|w|). So for every f -proof w, h(w) is an f -proof of the same tautology. If f simulates f , then f -proofs are not much longer than f -proofs. If additionally h ∈ PF, then we say that f p-simulates f . A proof system is optimal (resp., p-optimal) if it simulates (resp., p-simulates) every other proof system. The notion of simulation between proof systems is analogous to the notion of reducibility between problems. Using that analogy, optimal proof systems correspond to complete problems. It is not known whether there exist optimal propositional proof systems, but the question is interesting, because if there is an optimal proof system f , then there is a polynomially-bounded proof system if and only if f is polynomially-bounded. The question of whether optimal propositional proof systems exist has been studied in detail. Krajíček and Pudlák BIB001 BIB002 showed that NE = coNE implies the existence of optimal proof systems. BIB004 proved that existence of optimal proof systems results in the existence of ≤ p m -complete sets for the promise class NP ∩ SPARSE. In the same paper, they showed that there exist p-optimal proof systems only if the complexity class UP has a many-one complete set. These results hold relative to all oracles. Therefore, optimal proof systems exist relative to any oracle in which NE = coNE holds. Krajíček and Pudlák BIB002 , Ben-David and Gringauze  , and Buhrman et al. BIB005 constructed oracles relative to which optimal proof systems do not exist. In addition, NP∩SPARSE does not have complete sets relative to the latter oracle. Razborov BIB003 related the study of propositional proof systems to disjoint NP-pairs. For every propositional proof system f , he associated a canonical disjoint NP-pair. Furthermore, he showed that if f is an optimal proof system, then the canonical pair for f is a complete disjoint NP-pair. We will explain these results in Section 5, but first, in order to define the notion of completeness for disjoint NP-pairs, it is necessary to describe reducibilities between disjoint NP-pairs.