Abstract: Disjoint NP-pairs are an interesting complexity-theoretic concept with important applications in cryptography and propositional proof complexity. In this dissertation we explore the connection between disjoint NP-pairs and propositional proof complexity. This connection is fruitful for both fields. Various disjoint NP-pairs have been associated with propositional proof systems which characterize important properties of these systems, yielding applications to areas such as automated theorem proving. Further, conditional and unconditional lower bounds for the separation of disjoint NP-pairs can be translated to results on lower bounds to the length of propositional proofs. In this way disjoint NP-pairs have substantially contributed to the understanding of propositional proof systems.

Conversely, this dissertation aims to transfer proof-theoretic knowledge to the theory of NP-pairs to gain a more detailed understanding of the structure of the class of disjoint NP-pairs and in particular of the NP-pairs defined from propositional proof systems. For a proof system P we introduce the complexity class DNPP(P) of all disjoint NP-pairs for which the disjointness of the pair is efficiently provable in the proof system P. We exhibit structural properties of proof systems which make the previously defined canonical NP-pairs of these proof systems hard or complete for DNPP(P). Moreover, we demonstrate that non-equivalent proof systems can have equivalent canonical pairs and that depending on the properties of the proof systems different scenarios for DNPP(P) and the reductions between the canonical pairs exist. As an important tool for our investigation we use the connection of propositional proof systems and disjoint NP-pairs to theories of bounded arithmetic.

Table of Contents

1. Introduction

2. Propositional Proof Systems
    - Propositional Logic
    - Propositional Proof Complexity
    - Frege Systems and Their Extensions
    - Efficient Deduction
    - The Propositional Sequent Calculus
    - Natural Properties of Proof Systems

3. Arithmetic Theories and Proof Systems
    - Theories of Bounded Arithmetic
    - A Translation of Arithmetic Formulas into Propositional Formulas
    - Coding Propositional Proofs in Bounded Arithmetic
    - Consistency Statements
    - The Correspondence Between Arithmetic Theories and Propositional
      Proof Systems
    - The Correspondence Between S1_2 and EF
    - Regular Proof Systems
    - Comparing Properties of Proof Systems

4. Disjoint NP-Pairs
    - Reductions Between NP-Pairs
    - The Simulation Order of Disjoint NP-Pairs
    - Examples for Combinatorially Defined Pairs
    - NP-Pairs Characterize Properties of Proof Systems
    - Representations of NP-Pairs
    - The Complexity Class DNPP(P)
    - The Canonical Pair and the Reflection Principle
    - The Class DNPP(P) Under the Strong Strong Reduction
    - Canonical Candidates for Complete Pairs
    - Symmetry of Disjoint NP-Pairs
    - NP-Pairs and the Simulation Order of Proof Systems
    - A Weak Reduction Between Proof Systems
    - Proof Systems with Equivalent Canonical Pairs
    - Different Scenarios for DNPP(P)
    - On the Complexity of Ref(P)
    - Are Canonical Pairs Something Special?

5. Two Applications
    - Security of Public-Key Crypto Systems
    - Pseudorandom Generators in Proof Complexity

6. Disjoint Tuples of NP-Sets
    - Basic Definitions and Properties
    - Representable Disjoint Tuples of NP-Sets
    - Disjoint Tuples from Proof Systems
    - Arithmetic Representations
    - On Complete Disjoint Tuples of NP-Sets