{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,8,12]],"date-time":"2022-08-12T11:51:44Z","timestamp":1660305104009},"reference-count":30,"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":4394,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[2002,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Let us recall that Raphael Robinson's Arithmetic Q is an axiom system that differs from Peano Arithmetic essentially by containing no Induction axioms [13], [18]. We will generalize the semantic-tableaux version of the Second Incompleteness Theorem <jats:italic>almost to the level<\/jats:italic> of System Q. We will prove that there exists a single rather long \u03a0<jats:sub>1<\/jats:sub> sentence, valid in the standard model of the Natural Numbers and denoted as <jats:italic>V<\/jats:italic>. such that if <jats:italic>\u03b1<\/jats:italic> is <jats:italic>any<\/jats:italic> finite consistent extension of <jats:italic>Q<\/jats:italic> + <jats:italic>V<\/jats:italic> then <jats:italic>\u03b1<\/jats:italic> will be unable to prove its Semantic Tableaux consistency. The same result will also apply to axiom systems <jats:italic>\u03b1<\/jats:italic> with infinite cardinality when these infinite-sized axiom systems satisfy a minor additional constraint, called the <jats:italic>Conventional Encoding Property<\/jats:italic>.<\/jats:p><jats:p>Our formalism will also imply that the semantic-tableaux version of the Second Incompleteness Theorem generalizes for the axiom system I\u03a3<jats:sub>0<\/jats:sub>, as well as for all its natural extensions. (This answers an open question raised twenty years ago by Paris and Wilkie [15].)<\/jats:p>","DOI":"10.2178\/jsl\/1190150055","type":"journal-article","created":{"date-parts":[[2007,12,13]],"date-time":"2007-12-13T19:12:10Z","timestamp":1197573130000},"page":"465-496","source":"Crossref","is-referenced-by-count":20,"title":["How to extend the semantic tableaux and cut-free versions of the second incompleteness theorem almost to Robinson's arithmetic q"],"prefix":"10.1017","volume":"67","author":[{"given":"Dan E.","family":"Willard","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200010100_ref030","doi-asserted-by":"publisher","DOI":"10.1137\/0207018"},{"key":"S0022481200010100_ref029","first-page":"536","volume":"66","author":"Willard","year":"2001","journal-title":"Self-verifying systems, the incompleteness theorem and tangibility reflection principle"},{"key":"S0022481200010100_ref027","first-page":"319","volume-title":"Fifth Kurt G\u00f6del Colloquium","author":"Willard","year":"1997"},{"key":"S0022481200010100_ref026","first-page":"297","volume-title":"Dimacs series in discrete mathematics and theoretical computer science #39","author":"Willard","year":"1997"},{"key":"S0022481200010100_ref024","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(87)90066-2"},{"key":"S0022481200010100_ref022","doi-asserted-by":"publisher","DOI":"10.4099\/jjm1924.23.0_39"},{"key":"S0022481200010100_ref021","unstructured":"Solovay R. , Private communications (1994) about Pudl\u00e1k's main theorem from [16], See Appendix A of [29] for a 4-page summary of Solovay's idea."},{"key":"S0022481200010100_ref020","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-86718-7"},{"key":"S0022481200010100_ref019","volume-title":"Annals of Math Studies","volume":"47","author":"Smullyan","year":"1961"},{"key":"S0022481200010100_ref018","first-page":"729","volume-title":"Proceedings of 1950 International Congress on Mathematics","author":"Robinson"},{"key":"S0022481200010100_ref016","first-page":"423","volume":"50","author":"Pudl\u00e1k","year":"1985","journal-title":"Cuts consistency statements and interpretations"},{"key":"S0022481200010100_ref014","doi-asserted-by":"publisher","DOI":"10.1515\/9781400858927"},{"key":"S0022481200010100_ref013","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-7288-6"},{"key":"S0022481200010100_ref012","first-page":"1","article-title":"Formally self-referential propositions for cut-free classical analysis and related systems","volume":"118","author":"Kreisel","year":"1974","journal-title":"Dissertationes Mathematicae"},{"key":"S0022481200010100_ref011","first-page":"321","volume":"33","author":"Kreisel","year":"1968","journal-title":"A survey of proof theory, part I"},{"key":"S0022481200010100_ref007","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-0357-2"},{"key":"S0022481200010100_ref005","first-page":"503","volume":"41","author":"Bezboruah","year":"1976","journal-title":"G\u00d6del's second incompleteness theorem for Q"},{"key":"S0022481200010100_ref003","doi-asserted-by":"publisher","DOI":"10.1007\/s001530000072"},{"key":"S0022481200010100_ref002","volume-title":"On Tableaux consistency in weak theories","author":"Adamowicz","year":"1999"},{"key":"S0022481200010100_ref028","first-page":"415","volume-title":"The Semantic Tableaux version of the Second Incompleteness Theorem extends almost to Robinsons Arithmetic Q","volume":"1847","author":"Willard"},{"key":"S0022481200010100_ref023","volume-title":"Studies in logic","volume":"81","author":"Takeuti","year":"1987"},{"key":"S0022481200010100_ref017","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-7091-9461-4_5"},{"key":"S0022481200010100_ref006","volume-title":"Proof theory lecture notes","volume":"3","author":"Buss","year":"1986"},{"key":"S0022481200010100_ref004","unstructured":"Benett J. , Ph. D. Dissertation, 1962, Princeton University."},{"key":"S0022481200010100_ref008","volume-title":"Collected papers of Gerhard Gentzen","author":"Gentzen","year":"1969"},{"key":"S0022481200010100_ref025","first-page":"325","volume-title":"Third Kurt G\u00f6del Symposium","author":"Willard","year":"1993"},{"key":"S0022481200010100_ref001","unstructured":"Adamowicz Z. , Herbrand consistency and bounded arithmetic, to appear in Fundamental Mathematica."},{"key":"S0022481200010100_ref010","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511529948"},{"key":"S0022481200010100_ref015","first-page":"237","volume-title":"Proceedings of the Jadswin Logic Conference (Poland)","author":"Paris","year":"1981"},{"key":"S0022481200010100_ref009","volume-title":"Metamathematics of first order arithmetic","author":"H\u00e1jek","year":"1991"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200010100","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,7]],"date-time":"2019-05-07T01:34:26Z","timestamp":1557192866000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200010100\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,3]]},"references-count":30,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2002,3]]}},"alternative-id":["S0022481200010100"],"URL":"https:\/\/doi.org\/10.2178\/jsl\/1190150055","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[2002,3]]}}}