{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T07:58:42Z","timestamp":1781078322773,"version":"3.54.1"},"reference-count":29,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":3663,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[2004,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This article is a continuation of our search for tautologies that are hard even for strong propositional proof systems like <jats:italic>EF.<\/jats:italic> cf. [14, 15]. The particular tautologies we study, the <jats:italic>\u03c4<\/jats:italic>-formulas. are obtained from any <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S0022481200008161_inline1\"\/>\/poly map <jats:italic>g<\/jats:italic>; they express that a string is outside of the range of <jats:italic>g<\/jats:italic>, Maps <jats:italic>g<\/jats:italic> considered here are particular pseudorandom generators. The ultimate goal is to deduce the hardness of the <jats:italic>\u03c4<\/jats:italic>-formulas for at least <jats:italic>EF<\/jats:italic> from some general, plausible computational hardness hypothesis.<\/jats:p><jats:p>In this paper we introduce the notions of pseudo-surjective and iterable functions (related to free functions of [15]). These two properties imply the hardness of the <jats:italic>\u03c4<\/jats:italic>-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 <jats:italic>g<\/jats:italic> yielding hard <jats:italic>\u03c4<\/jats:italic>-formulas in terms of a hitting set type property (all relative to a propositional proof system). We show that a proof system containing <jats:italic>EF<\/jats:italic> admits a pseudo-surjective function unless it simulates a proof system <jats:italic>WF<\/jats:italic> introduced by Je\u0159\u00e1bek [11]. an extension of <jats:italic>EF<\/jats:italic>.<\/jats:p><jats:p>We propose a concrete map <jats:italic>g<\/jats:italic> 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 <jats:italic>n<\/jats:italic><jats:sup>3 \u2212<jats:italic>\u03b5<\/jats:italic><\/jats:sup> (that improves upon a direct construction of Alekhnovich et al. [2]).<\/jats:p>","DOI":"10.2178\/jsl\/1080938841","type":"journal-article","created":{"date-parts":[[2005,3,2]],"date-time":"2005-03-02T21:30:47Z","timestamp":1109799047000},"page":"265-286","source":"Crossref","is-referenced-by-count":31,"title":["Dual weak pigeonhole principle, pseudo-surjective functions, and provability of circuit lower bounds"],"prefix":"10.1017","volume":"69","author":[{"given":"Jan","family":"Kraj\u00ed\u010dek","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200008161_ref021","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(05)80043-1"},{"key":"S0022481200008161_ref008","article-title":"Candidate one-way functions based on expander graphs","volume":"90","author":"Goldreich","year":"2000","journal-title":"Electronic Colloquium on Computational Complexity"},{"key":"S0022481200008161_ref019","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1997.2674"},{"key":"S0022481200008161_ref014","doi-asserted-by":"publisher","DOI":"10.4064\/fm170-1-8"},{"key":"S0022481200008161_ref020","first-page":"48","volume-title":"Mathematical Foundations of Computer Science (B. Bystrica, August '90)","volume":"452","author":"Kraj\u00ed\u010dek","year":"1990"},{"key":"S0022481200008161_ref018","first-page":"193","volume-title":"Computer Science Logic (Kaiserlautern, October '89)","volume":"440","author":"Kraj\u00ed\u010dek","year":"1990"},{"key":"S0022481200008161_ref025","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(98)80023-2"},{"key":"S0022481200008161_ref022","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0075316"},{"key":"S0022481200008161_ref016","unstructured":"Kraj\u00ed\u010dek J. , Hardness assumptions in the foundations of theoretical computer science, preprint in ITI series: http:\/\/iti.mff.cuni.cz\/series\/index.html, 01 2003."},{"key":"S0022481200008161_ref017","first-page":"1063","volume":"54","author":"Kraj\u00ed\u010dek","year":"1989","journal-title":"Propositional proof systems, the consistency of first order theories and the complexity of computations"},{"key":"S0022481200008161_ref028","first-page":"29","volume-title":"Proceedings of the 17th IEEE Conference on Computational Complexity","author":"Razborov","year":"2002"},{"key":"S0022481200008161_ref015","doi-asserted-by":"publisher","DOI":"10.2307\/2687774"},{"key":"S0022481200008161_ref012","first-page":"287","volume-title":"Logic from Computer Science, Proceedings of a Workshop held November 13\u201317, 1989, in Berkeley","volume":"21","author":"Kraj\u00ed\u010dek","year":"1992"},{"key":"S0022481200008161_ref010","first-page":"220","volume-title":"Proceedings of the 29th Annual ACM Symposium on Theory of Computing","author":"Impagliazzo","year":"1997"},{"key":"S0022481200008161_ref007","first-page":"36","volume":"44","author":"Cook","year":"1979","journal-title":"The relative efficiency of propositional proof systems"},{"key":"S0022481200008161_ref006","first-page":"83","volume-title":"Proceedings of the 7th Annual ACM Symposium on Theory of Computing","author":"Cook","year":"1975"},{"key":"S0022481200008161_ref002","first-page":"43","article-title":"Pseudorandom generators in propositional proof complexity","volume":"23","author":"Alekhnovich","year":"2000","journal-title":"Electronic Colloquium on Computational Complexity"},{"key":"S0022481200008161_ref005","doi-asserted-by":"publisher","DOI":"10.1007\/BF01294258"},{"key":"S0022481200008161_ref003","first-page":"569","volume-title":"11th Annual Conference of the European Association for Computer Science Logic (CSL)","volume":"2471","author":"Atserias","year":"2002"},{"key":"S0022481200008161_ref001","first-page":"346","volume-title":"Proceedings of the IEEE 29th Annual Symposium on Foundation of Computer Science","author":"Ajtai","year":"1988"},{"key":"S0022481200008161_ref027","first-page":"201","article-title":"Unprovability of lower bounds on the circuit size in certain fragments of bounded arithmetic","volume":"59","author":"Razborov","year":"1995","journal-title":"Rossi\u012dskaya Akademiya Nauk, Seriya Matematicheskaya"},{"key":"S0022481200008161_ref026","unstructured":"Razborov A. A. , Pseudorandom generators hard for k-DNF resolution and polynomial calculus resolution, preprint, 05 2003."},{"key":"S0022481200008161_ref024","first-page":"499","volume-title":"Logic from Computer Science, Proceedings of a Workshop held November 13\u201317, 1989, in Berkeley","volume":"21","author":"Pudl\u00e1k","year":"1992"},{"key":"S0022481200008161_ref013","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511529948"},{"key":"S0022481200008161_ref029","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63248-4_8"},{"key":"S0022481200008161_ref009","doi-asserted-by":"publisher","DOI":"10.1145\/6490.6503"},{"key":"S0022481200008161_ref023","first-page":"1235","volume":"53","author":"Paris","year":"1988","journal-title":"Provability of the pigeonhole principle and the existence of infinitely many primes"},{"key":"S0022481200008161_ref004","first-page":"517","volume-title":"Proceedings of the 31st ACM Symposium on Theory of Computation","author":"Ben-Sasson","year":"1999"},{"key":"S0022481200008161_ref011","volume-title":"Annals of Pure and Applied Logic","author":"Je\u0159\u00e1bek"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200008161","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,6]],"date-time":"2019-05-06T21:28:50Z","timestamp":1557178130000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200008161\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,3]]},"references-count":29,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2004,3]]}},"alternative-id":["S0022481200008161"],"URL":"https:\/\/doi.org\/10.2178\/jsl\/1080938841","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,3]]}}}