{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,26]],"date-time":"2026-02-26T15:32:40Z","timestamp":1772119960106,"version":"3.50.1"},"reference-count":12,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2021,6,9]],"date-time":"2021-06-09T00:00:00Z","timestamp":1623196800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,6,9]],"date-time":"2021-06-09T00:00:00Z","timestamp":1623196800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100002345","name":"Eberhard Karls Universit\u00e4t T\u00fcbingen","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100002345","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Log. Univers."],"published-print":{"date-parts":[[2021,12]]},"abstract":"Abstract<\/jats:title>\n \n We study the decidability of\n k<\/jats:italic>\n -provability in\n \n \n $$\\hbox {PA}$$<\/jats:tex-math>\n \n PA<\/mml:mtext>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n \u2014the relation \u2018being provable in\n \n \n $$\\hbox {PA}$$<\/jats:tex-math>\n \n PA<\/mml:mtext>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n with at most\n k<\/jats:italic>\n steps\u2019\u2014and the decidability of the proof-skeleton problem\u2014the problem of deciding if a given formula has a proof that has a given skeleton (the list of axioms and rules that were used). The decidability of\n k<\/jats:italic>\n -provability for the usual Hilbert-style formalisation of\n \n \n $$\\hbox {PA}$$<\/jats:tex-math>\n \n PA<\/mml:mtext>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n is still an open problem, but it is known that the proof-skeleton problem is undecidable for that theory. Using new methods, we present a characterisation of some numbers\n k<\/jats:italic>\n for which\n k<\/jats:italic>\n -provability is decidable, and we present a characterisation of some proof-skeletons for which one can decide whether a formula has a proof whose skeleton is the considered one. These characterisations are natural and parameterised by unification algorithms.\n <\/jats:p>","DOI":"10.1007\/s11787-021-00278-1","type":"journal-article","created":{"date-parts":[[2021,6,9]],"date-time":"2021-06-09T10:27:45Z","timestamp":1623234465000},"page":"477-516","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["k-Provability in $$\\hbox {PA}$$"],"prefix":"10.1007","volume":"15","author":[{"given":"Paulo Guilherme","family":"Santos","sequence":"first","affiliation":[]},{"given":"Reinhard","family":"Kahle","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,6,9]]},"reference":[{"key":"278_CR1","first-page":"29","volume-title":"Arithmetic, Proof Theory and Computational Complexity","author":"M Baaz","year":"1993","unstructured":"Baaz, M., Pudl\u00e1k, P.: Kreisel\u2019s conjecture for L$$\\exists $$1. In: Clote, P., Kraji\u0107ek, J. (eds.) Arithmetic, Proof Theory and Computational Complexity, pp. 29\u201359. Oxford University, Oxford (1993)"},{"issue":"1","key":"278_CR2","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1016\/0168-0072(91)90059-U","volume":"53","author":"SR Buss","year":"1991","unstructured":"Buss, S.R.: The undecidability of k-provability. Ann. Pure Appl. Logic 53(1), 75\u2013102 (1991)","journal-title":"Ann. Pure Appl. Logic"},{"issue":"5","key":"278_CR3","doi-asserted-by":"publisher","first-page":"689","DOI":"10.1007\/s10958-009-9408-0","volume":"158","author":"S Cavagnetto","year":"2009","unstructured":"Cavagnetto, S.: The lengths of proofs: Kreisel\u2019s conjecture and G\u00f6del\u2019s speed-up theorem. J. Math. Sci. 158(5), 689\u2013707 (2009)","journal-title":"J. Math. Sci."},{"key":"278_CR4","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1093\/oso\/9780198536901.001.0001","volume-title":"Arithmetic, Proof Theory and Computational Complexity","author":"P Clote","year":"1993","unstructured":"Clote, P., Kraj\u00ed\u010dek, J.: Open problems. In: Clote, P., Kraj\u00ed\u010dek, J. (eds.) Arithmetic, Proof Theory and Computational Complexity, pp. 1\u201319. Oxford University, Oxford (1993)"},{"key":"278_CR5","volume-title":"A Mathematical Introduction to Logic","author":"HB Enderton","year":"2001","unstructured":"Enderton, H.B.: A Mathematical Introduction to Logic. Elsevier, Amsterdam (2001)"},{"issue":"3","key":"278_CR6","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1016\/0168-0072(91)90015-E","volume":"51","author":"WM Farmer","year":"1991","unstructured":"Farmer, W.M.: A unification-theoretic method for investigating the k-provability problem. Ann. Pure Appl. Logic 51(3), 173\u2013214 (1991)","journal-title":"Ann. Pure Appl. Logic"},{"issue":"1\u20133","key":"278_CR7","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/BF01531022","volume":"6","author":"WM Farmer","year":"1992","unstructured":"Farmer, W.M.: The Kreisel length-of-proof problem. Ann. Math. Artif. Intell. 6(1\u20133), 27\u201355 (1992)","journal-title":"Ann. Math. Artif. Intell."},{"issue":"1","key":"278_CR8","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/BF01625836","volume":"27","author":"J Kraj\u00ed\u010dek","year":"1988","unstructured":"Kraj\u00ed\u010dek, J., Pavel, P.: The number of proof lines and the size of proofs in first order logic. Arch. Math. Logic 27(1), 69\u201384 (1988)","journal-title":"Arch. Math. Logic"},{"issue":"1","key":"278_CR9","doi-asserted-by":"publisher","first-page":"115","DOI":"10.21099\/tkbjm\/1496158798","volume":"4","author":"T Miyatake","year":"1980","unstructured":"Miyatake, T.: On the length of proofs in a formal systems. Tsukuba J. Math. 4(1), 115\u2013125 (1980)","journal-title":"Tsukuba J. Math."},{"key":"278_CR10","series-title":"Translations of Mathematical Monographs","doi-asserted-by":"publisher","DOI":"10.1090\/mmono\/128","volume-title":"Complexity of Proofs and Their Transformations in Axiomatic Theories","author":"VP Orevkov","year":"1993","unstructured":"Orevkov, V.P.: Complexity of Proofs and Their Transformations in Axiomatic Theories. Translations of Mathematical Monographs, vol. 128. American Mathematical Society, Providence (1993)"},{"key":"278_CR11","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1090\/S0002-9947-1973-0432416-X","volume":"177","author":"RJ Parikh","year":"1973","unstructured":"Parikh, R.J.: Some results on the length of proofs. Trans. Am. Math. Soc. 177, 29\u201336 (1973)","journal-title":"Trans. Am. Math. Soc."},{"issue":"1","key":"278_CR12","doi-asserted-by":"publisher","first-page":"123","DOI":"10.2178\/jsl\/1174668388","volume":"72","author":"H Pavel","year":"2007","unstructured":"Pavel, H.: Theories very close to $$PA$$ where Kreisel\u2019s Conjecture is false. J. Symb. Log. 72(1), 123\u2013137 (2007)","journal-title":"J. Symb. Log."}],"container-title":["Logica Universalis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11787-021-00278-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11787-021-00278-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11787-021-00278-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,1]],"date-time":"2024-09-01T09:46:51Z","timestamp":1725184011000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11787-021-00278-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,6,9]]},"references-count":12,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2021,12]]}},"alternative-id":["278"],"URL":"https:\/\/doi.org\/10.1007\/s11787-021-00278-1","relation":{"is-basis-for":[{"id-type":"doi","id":"10.52843\/cassyni.dqql1v","asserted-by":"object"}]},"ISSN":["1661-8297","1661-8300"],"issn-type":[{"value":"1661-8297","type":"print"},{"value":"1661-8300","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,6,9]]},"assertion":[{"value":"20 September 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"1 May 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"9 June 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}