Dual weak pigeonhole principle, Boolean complexity, and derandomization

We study the extension (introduced as BT by Krajı́ček in Fund. Math. 170 (2001) 123) of the theory S21 by instances of the dual (onto) weak pigeonhole principle for p-time functions, dWPHP(PV)x2x. 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 S21+dWPHP(PV). We construct a propositional proof system WF (based on a reformulation of Extended Frege in terms of Boolean circuits), which captures the ∀Π1b-consequences of S21+dWPHP(PV). We also show that WF p-simulates the Unstructured Extended Nullstellensatz proof system of Buss et al. (Comput. Complexity 6 (1996/1997) 256). ve that dWPHP(PV) is (over S21) 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 S21+dWPHP(PV).