{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T18:17:08Z","timestamp":1781893028670,"version":"3.54.5"},"reference-count":10,"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":1472,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[2010,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The undecidability of first-order logic implies that there is no computable bound on the length of shortest proofs of valid sentences of first-order logic. Some valid sentences can only have quite long proofs. How hard is it to prove such \u201chard\u201d valid sentences? The polynomial time tractability of this problem would imply the fixed-parameter tractability of the parameterized problem that, given a natural number <jats:italic>n<\/jats:italic> in unary as input and a first-order sentence <jats:italic>\u03c6<\/jats:italic> as parameter, asks whether <jats:italic>\u03c6<\/jats:italic> has a proof of length \u2264 <jats:italic>n<\/jats:italic>. As the underlying classical problem has been considered by G\u00f6del we denote this problem by <jats:italic>p<\/jats:italic>-G\u00f6del. We show that <jats:italic>p<\/jats:italic>-G\u00f6del is not fixed-parameter tractable if DTIME(<jats:italic>h<\/jats:italic><jats:sup>O(1)<\/jats:sup>) \u2260 NTIME(<jats:italic>h<\/jats:italic><jats:sup>O(1)<\/jats:sup>) for all time constructible and increasing functions <jats:italic>h<\/jats:italic>. Moreover we analyze the complexity of the construction problem associated with <jats:italic>p<\/jats:italic>-G\u00f6del.<\/jats:p>","DOI":"10.2178\/jsl\/1264433918","type":"journal-article","created":{"date-parts":[[2010,1,25]],"date-time":"2010-01-25T10:38:59Z","timestamp":1264415939000},"page":"239-254","source":"Crossref","is-referenced-by-count":11,"title":["On the complexity of G\u00f6del's proof predicate"],"prefix":"10.1017","volume":"75","author":[{"given":"Yijia","family":"Chen","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"J\u00f6rg","family":"Flum","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200002929_ref010","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00023-C"},{"key":"S0022481200002929_ref009","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1872-2_10"},{"key":"S0022481200002929_ref008","volume-title":"Collected works, vol. VI","author":"G\u00f6del","year":"2003"},{"key":"S0022481200002929_ref007","volume-title":"Parameterized complexity theory","author":"Flum","year":"2006"},{"key":"S0022481200002929_ref006","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-2355-7"},{"key":"S0022481200002929_ref004","first-page":"40","volume":"1","author":"Church","year":"1936","journal-title":"A note on the Entscheidungsproblem"},{"key":"S0022481200002929_ref002","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-2566-9_4"},{"key":"S0022481200002929_ref001","first-page":"1","volume-title":"Proceedings of the 23rd Annual IEEE Conference on Computational Complexity (CCC'08)","author":"Buhrman","year":"2008"},{"key":"S0022481200002929_ref005","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0515-9"},{"key":"S0022481200002929_ref003","first-page":"397","volume-title":"Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science (LICS '09)","author":"Chen","year":"2009"}],"container-title":["The Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200002929","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T16:37:10Z","timestamp":1556469430000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200002929\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,3]]},"references-count":10,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2010,3]]}},"alternative-id":["S0022481200002929"],"URL":"https:\/\/doi.org\/10.2178\/jsl\/1264433918","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,3]]}}}