We study the extension (introduced as BT in [5]) of the theory S1 2 by instances of the dual (onto) weak pigeonhole principle for p-time functions, dWPHP(PV )x x2 . 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 S1 2 +dWPHP(PV ). We construct a propositional proof system WF (based on a reformulation of Extended Frege in terms of Boolean circuits), which captures the b 1-consequences of S1 2 +dWPHP(PV ). We also show that WF p-simulates the Unstructured Extended Nullstellensatz proof system of [2]. We prove that dWPHP(PV ) is (over S1 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 (derandomization of probabilistic p-time algorithms) in a conservative extension of S1 2 + dWPHP(PV ). Preliminaries We assume the reade...