Abstract

We study the extension of the theory S^1_2 by instances of the dual (onto) weak pigeonhole principle for p-time functions, dWPHP(PV)^x_{x^2}. We propose a natural framework for formalization of randomized algorithms in bounded arithmetic, and use it to provide a strengthening of Wilkie's witnessing theorem for S^1_2+dWPHP(PV). Then we show that dWPHP(PV) is (over S^1_2) equivalent to a statement asserting the existence of a family of Boolean functions with exponential circuit complexity. Building on this result, we formalize the Nisan-Wigderson construction (conditional derandomization of probabilistic p-time algorithms) in a conservative extension of S^1_2+dWPHP(PV). We also develop in S^1_2 the algebraic machinery needed for implicit list-decoding of Reed\hyph Muller error\hyph correcting codes (including some results on a modification of Soltys' theory \forall LAP), and use it to formalize the Impagliazzo-Wigderson strengthening of the Nisan-Wigderson theorem.

We construct a propositional proof system WF (based on a reformulation of Extended Frege in terms of Boolean circuits), which captures the \forall\Pi^b_1-consequences of S^1_2+dWPHP(PV). As an application, we show that WF and G_2 p-simulate the Unstructured Extended Nullstellensatz proof system.

We also consider two theories which have explicit counting facilities in their language. The first one is the Impagliazzo-Kapron logic; we propose a modification of the theory, and prove a generalization of the Impagliazzo-Kapron soundness theorem to \forall\exists-consequences of the theory. The second one is a feasible theory of approximate counting, formulated in a variant of Kleene's 3-valued logic. We introduce the theory, and prove a witnessing theorem for its existential consequences.

Table of Contents

1. Introduction

2. Preliminaries
   2.1 Computational complexity
   2.2 Bounded arithmetic
   2.3 Propositional proof complexity

3. Randomized computation in bounded arithmetic
   3.1 Definable probabilistic algorithms
   3.2 Properties of definable MFRP
   3.3 Witnessing dWPHP

4. Hard Boolean functions
   4.1 Hard functions and dWPHP(PV)
   4.2 The Nisan-Wigderson generator
   4.3 Finite fields in bounded arithmetic
      4.3.1 Basic properties of finite fields
      4.3.2 Some linear algebra
      4.3.3 List decoding of Reed-Solomon codes
      4.3.4 List decoding of Reed-Muller codes
      4.3.5 Hardness amplification

5. A propositional proof system associated with dWPHP(PV)
   5.1 Circuit Frege
   5.2 WPHP Frege

6. Theories with explicit counting
   6.1 Impagliazzo-Kapron logic
      6.1.1 Description of the theory
      6.1.2 The soundness theorem
   6.2 A theory of approximate counting
      6.2.1 Kleene's logic
      6.2.2 The theory C^1_2
      6.2.3 A witnessing theorem for C^1_2

Bibliography

A. Some bounds on binomial coefficients