Weak Pigeonhole Principle, and Randomized Computation
Emil Jeřábek · 2005
We study the extension 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). Then we show 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 (conditional derandomization of probabilistic p-time algorithms) in a conservative extension of S1 2 + dWPHP(PV). We also develop in S1 2 the algebraic machinery needed for implicit list-decoding of Reed-Muller error-correcting codes (including some results on a modification of Soltys ’ theory ∀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