×

Dual weak pigeonhole principle, Boolean complexity, and derandomization. (English) Zbl 1057.03047

Summary: We study the extension [introduced as BT by J. Krajiček in Fundam. Math. 170, 123–140 (2001; Zbl 0987.03051)] 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+\text{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^b_1\)-consequences of \(S^1_2+\text{dPHP(PV)}\). We also show that WF p-simulates the Unstructured Extended Nullstellensatz proof system of S. Buss, R. Impagliazzo, J. Krajíček, P. Pudlák, A. A. Razborov and J. Sgall [Comput. Complexity 6, 256–298 (1997; Zbl 0890.03030)].
We prove 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 (derandomization of probabilistic p-time algorithms) in a conservative extension of \(S^1_2+\text{dWPHP(PV)}\).

MSC:

03F20 Complexity of proofs
03F30 First-order arithmetic and fragments
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Buss, S., Bounded Arithmetic (1986), Bibliopolis: Bibliopolis Naples · Zbl 0649.03042
[2] Buss, S.; Impagliazzo, R.; Krajı́ček, J.; Pudlák, P.; Razborov, A.; Sgall, J., Proof complexity in algebraic systems and bounded depth Frege systems with modular counting, Comput. Complexity, 6, 256-298 (1996/1997) · Zbl 0890.03030
[3] S. Cook, Feasibly constructive proofs and the propositional calculus, in: Proceedings Third Annual ACM Symposium on Theory of Computing, ACM Press, New York, 1975, pp. 83-97.; S. Cook, Feasibly constructive proofs and the propositional calculus, in: Proceedings Third Annual ACM Symposium on Theory of Computing, ACM Press, New York, 1975, pp. 83-97. · Zbl 0357.68061
[4] Krajı́ček, J., Bounded Arithmetic, Propositional Logic, and Complexity Theory (1995), Cambridge University Press: Cambridge University Press Cambridge · Zbl 0835.03025
[5] Krajı́ček, J., On the weak pigeonhole principle, Fund. Math., 170, 123-140 (2001) · Zbl 0987.03051
[6] Krajı́ček, J.; Pudlák, P., Quantified propositional calculi and fragments of bounded arithmetic, Z. Math. Logik Grundlag. Math., 36, 29-46 (1990) · Zbl 0696.03031
[7] Krajı́ček, J.; Pudlák, P., Some consequences of cryptographical conjectures for \(S_2^1\) and EF, Inform. and Comput., 140, 82-94 (1998) · Zbl 0892.68029
[8] Maciel, A.; Pitassi, T.; Woods, A., A new proof of the weak pigeonhole principle, J. Comput. System Sci., 64, 843-872 (2002) · Zbl 1051.03049
[9] Nisan, N.; Wigderson, A., Hardness vs. Randomness, J. Comput. System Sci., 49, 149-167 (1994) · Zbl 0821.68057
[10] Parikh, R., Existence and feasibility in arithmetic, J. Symbolic Logic, 36, 494-508 (1971) · Zbl 0243.02037
[11] Paris, J.; Wilkie, A.; Woods, A., Provability of the pigeonhole principle and the existence of infinitely many primes, J. Symbolic Logic, 53, 1235-1244 (1988) · Zbl 0688.03042
[12] J.-P. Ressayre, A conservation result for system of bounded arithmetic, unpublished manuscript, 1986.; J.-P. Ressayre, A conservation result for system of bounded arithmetic, unpublished manuscript, 1986.
[13] N. Thapen, The weak pigeonhole principle in models of bounded arithmetic, Ph.D. Thesis, Oxford University, 2002.; N. Thapen, The weak pigeonhole principle in models of bounded arithmetic, Ph.D. Thesis, Oxford University, 2002. · Zbl 1008.03024
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.