**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