##
**Dual weak pigeonhole principle, pseudo-surjective functions, and provability of circuit lower bounds.**
*(English)*
Zbl 1068.03048

Summary: This article is a continuation of our search for tautologies that are hard even for strong propositional proof systems like EF [cf. the author, Fundam. Math. 170, 123–140 (2001; Zbl 0987.03051) and Bull. Symb. Log. 7, 197–212 (2001; Zbl 0983.03046)]. The particular tautologies we study, the \(\tau\)-formulas, are obtained from any \(\mathcal P\)/poly map \(g\); they express that a string is outside of the range of \(g\). Maps \(g\) considered here are particular pseudorandom generators. The ultimate goal is to deduce the hardness of the \(\tau\)-formulas for at least EF from some general, plausible computational hardness hypothesis.

In this paper we introduce the notions of pseudo-surjective and iterable functions (related to free functions of the second paper cited above). These two properties imply the hardness of the \(\tau\)-formulas from the function but unlike the hardness they are preserved under composition and iteration. We link the existence of maps with these two properties to the provability of circuit lower bounds, and we characterize maps \(g\) yielding hard \(\tau\)-formulas in terms of a hitting set type property (all relative to a propositional proof system). We show that a proof system containing EF admits a pseudo-surjective function unless it simulates a proof system WF introduced by E. Jeřábek [Ann. Pure Appl. Logic 129, 1–37 (2004; Zbl 1057.03047)], an extension of EF.

We propose a concrete map \(g\) as a candidate function possibly pseudo-surjective or free for strong proof systems. The map is defined as a Nisan-Wigderson generator based on a random function and on a random sparse matrix. We prove that it is iterable in a particular way in resolution, yielding the output/input ratio \(n^{3-\varepsilon}\) (that improves upon a direct construction of M. Alekhnovich, E. Ben-Sasson, A. A. Razborov, and A. Wigderson [SIAM J. Comput. 34, 67–88 (2004; Zbl 1096.03070)]).

In this paper we introduce the notions of pseudo-surjective and iterable functions (related to free functions of the second paper cited above). These two properties imply the hardness of the \(\tau\)-formulas from the function but unlike the hardness they are preserved under composition and iteration. We link the existence of maps with these two properties to the provability of circuit lower bounds, and we characterize maps \(g\) yielding hard \(\tau\)-formulas in terms of a hitting set type property (all relative to a propositional proof system). We show that a proof system containing EF admits a pseudo-surjective function unless it simulates a proof system WF introduced by E. Jeřábek [Ann. Pure Appl. Logic 129, 1–37 (2004; Zbl 1057.03047)], an extension of EF.

We propose a concrete map \(g\) as a candidate function possibly pseudo-surjective or free for strong proof systems. The map is defined as a Nisan-Wigderson generator based on a random function and on a random sparse matrix. We prove that it is iterable in a particular way in resolution, yielding the output/input ratio \(n^{3-\varepsilon}\) (that improves upon a direct construction of M. Alekhnovich, E. Ben-Sasson, A. A. Razborov, and A. Wigderson [SIAM J. Comput. 34, 67–88 (2004; Zbl 1096.03070)]).

### MSC:

03F20 | Complexity of proofs |

68Q17 | Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) |

### Keywords:

hard tautologies; propositional proof systems; pseudorandom generators; computational hardness; provability; circuit lower bound; Nisan-Wigderson generator; input/output ratio
Full Text:
DOI

### References:

[1] | DOI: 10.1016/S0022-0000(05)80043-1 · Zbl 0821.68057 · doi:10.1016/S0022-0000(05)80043-1 |

[2] | Provability of the pigeonhole principle and the existence of infinitely many primes 53 pp 1235– (1988) · Zbl 0688.03042 |

[3] | DOI: 10.1145/6490.6503 · doi:10.1145/6490.6503 |

[4] | Electronic Colloquium on Computational Complexity 90 (2000) |

[5] | The relative efficiency of propositional proof systems 44 pp 36– (1979) · Zbl 0408.03044 |

[6] | Proceedings of the 7th Annual ACM Symposium on Theory of Computing pp 83– (1975) |

[7] | DOI: 10.1007/BF01294258 · Zbl 0890.03030 · doi:10.1007/BF01294258 |

[8] | Proceedings of the 31st ACM Symposium on Theory of Computation pp 517– (1999) |

[9] | 11th Annual Conference of the European Association for Computer Science Logic (CSL) 2471 pp 569– (2002) |

[10] | Electronic Colloquium on Computational Complexity 23 pp 43– (2000) |

[11] | Proceedings of the IEEE 29th Annual Symposium on Foundation of Computer Science pp 346– (1988) |

[12] | DOI: 10.1006/inco.1997.2674 · Zbl 0892.68029 · doi:10.1006/inco.1997.2674 |

[13] | Computer Science Logic (Kaiserlautern, October ’89) 440 pp 193– (1990) · Zbl 0716.68007 |

[14] | Propositional proof systems, the consistency of first order theories and the complexity of computations 54 pp 1063– (1989) · Zbl 0696.03029 |

[15] | DOI: 10.2307/2687774 · Zbl 0983.03046 · doi:10.2307/2687774 |

[16] | DOI: 10.4064/fm170-1-8 · Zbl 0987.03051 · doi:10.4064/fm170-1-8 |

[17] | Bounded arithmetic, propositional logic, and complexity theory 60 (1995) |

[18] | Logic from Computer Science, Proceedings of a Workshop held November 13–17, 1989, in Berkeley 21 pp 287– (1992) |

[19] | DOI: 10.1007/BFb0075316 · doi:10.1007/BFb0075316 |

[20] | Annals of Pure and Applied Logic |

[21] | Proceedings of the 29th Annual ACM Symposium on Theory of Computing pp 220– (1997) |

[22] | DOI: 10.1007/3-540-63248-4_8 · doi:10.1007/3-540-63248-4_8 |

[23] | Proceedings of the 17th IEEE Conference on Computational Complexity pp 29– (2002) |

[24] | Rossiĭskaya Akademiya Nauk, Seriya Matematicheskaya 59 pp 201– (1995) |

[25] | Handbook of proof theory pp 547– (1998) |

[26] | Logic from Computer Science, Proceedings of a Workshop held November 13–17, 1989, in Berkeley 21 pp 499– (1992) |

[27] | Mathematical Foundations of Computer Science (B. Bystrica, August ’90) 452 pp 48– (1990) |

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.