Dual weak pigeonhole principle, Boolean complexity, and derandomization

@article{citeulike:131998, abstract = {We study the extension (introduced as BT by Krajicek 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 [forall][Pi]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).We prove 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).}, author = {Jerabek, Emil }, citeulike-article-id = {131998}, doi = {10.1016/j.apal.2003.12.003}, journal = {Annals of Pure and Applied Logic}, keywords = {bounded\_arithmetic}, month = {October}, number = {1-3}, pages = {1--37}, posted-at = {2005-03-18 11:18:35}, priority = {2}, title = {Dual weak pigeonhole principle, Boolean complexity, and derandomization}, url = {http://dx.doi.org/10.1016/j.apal.2003.12.003}, volume = {129}, year = {2004} }

TY - JOUR ID - citeulike:131998 L3 - citeulike-article-id:131998 TI - Dual weak pigeonhole principle, Boolean complexity, and derandomization JF - Annals of Pure and Applied Logic VL - 129 IS - 1-3 SP - 1 EP - 37 N2 - We study the extension (introduced as BT by Krajicek 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 [forall][Pi]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).We prove 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). KW - bounded_arithmetic AU - Jerabek, Emil PY - 2004/10// UR - http://dx.doi.org/10.1016/j.apal.2003.12.003 ER -