{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T18:51:27Z","timestamp":1725475887150},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540676973"},{"type":"electronic","value":"9783540450085"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10722086_32","type":"book-chapter","created":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T19:43:15Z","timestamp":1167421395000},"page":"415-430","source":"Crossref","is-referenced-by-count":7,"title":["The Semantic Tableaux Version of the Second Incompleteness Theorem Extends Almost to Robinson\u2019s Arithmetic Q"],"prefix":"10.1007","author":[{"given":"Dan E.","family":"Willard","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"32_CR1","unstructured":"Adamowicz, Z.: On Tableaux consistency in weak theories, circulating manuscript from the Mathematics Institute of the Polish Academy of Sciences (1999)"},{"key":"32_CR2","unstructured":"Benett, J.: Ph. D. Dissertation, Princeton University (1962)"},{"key":"32_CR3","doi-asserted-by":"publisher","first-page":"503","DOI":"10.2307\/2272251","volume":"41","author":"A. Bezboruah","year":"1976","unstructured":"Bezboruah, A., Shepherdson, J.: G\u00f6del\u2019s Second Incompleteness Theorem for Q. Journal of Symbolic Logic\u00a041, 503\u2013512 (1976)","journal-title":"Journal of Symbolic Logic"},{"key":"32_CR4","volume-title":"Bounded Arithmetic, in Proof Theory Lecture Notes","author":"S. Buss","year":"1986","unstructured":"Buss, S.: Bounded Arithmetic, in Proof Theory Lecture Notes, vol.\u00a03. published by Bibliopolis, Naples (1986)"},{"key":"32_CR5","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-0357-2","volume-title":"First Order Logic and Automated Theorem Proving","author":"M. Fitting","year":"1990","unstructured":"Fitting, M.: First Order Logic and Automated Theorem Proving. Springer, Heidelberg (1990)"},{"key":"32_CR6","volume-title":"Metamathematics of First Order Arithmetic","author":"P. H\u00e1jek","year":"1991","unstructured":"H\u00e1jek, P., Pudl\u00e1k, P.: Metamathematics of First Order Arithmetic. Springer, Heidelberg (1991)"},{"key":"32_CR7","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511529948","volume-title":"Bounded Propositional Logic and Complexity Theory","author":"J. Kraj\u00edcek","year":"1995","unstructured":"Kraj\u00edcek, J.: Bounded Propositional Logic and Complexity Theory. Cambridge University Press, Cambridge (1995)"},{"key":"32_CR8","doi-asserted-by":"publisher","first-page":"321","DOI":"10.2307\/2270324","volume":"33","author":"G. Kreisel","year":"1968","unstructured":"Kreisel, G.: A Survey of Proof Theory, Part I. Journal of Symbolic Logic\u00a033, 321\u2013388 (1968); Part II. In: Proceedings of Second Scandinavian Logic Symposium, pp.109\u2013170. North Holland Press, Amsterdam (1971)","journal-title":"Journal of Symbolic Logic"},{"key":"32_CR9","first-page":"1","volume":"118","author":"G. Kreisel","year":"1974","unstructured":"Kreisel, G., Takeuti, G.: Formally Self-Referential Propositions for Cut-Free Classical Analysis and Related Systems. Dissertationes Mathematicae\u00a0118, 1\u201355 (1974)","journal-title":"Dissertationes Mathematicae"},{"key":"#cr-split#-32_CR10.1","doi-asserted-by":"crossref","unstructured":"Mendelson, E.: Introduction to Mathematical Logic. Wadsworth-Brooks-Cole Math Series (1987);","DOI":"10.1007\/978-1-4615-7288-6"},{"key":"#cr-split#-32_CR10.2","unstructured":"See page 157 for Q???s definition"},{"key":"32_CR11","doi-asserted-by":"crossref","DOI":"10.1515\/9781400858927","volume-title":"Predicative Arithmetic","author":"E. Nelson","year":"1986","unstructured":"Nelson, E.: Predicative Arithmetic. Princeton University Press, Princeton (1986)"},{"key":"32_CR12","doi-asserted-by":"publisher","first-page":"494","DOI":"10.2307\/2269958","volume":"36","author":"R. Parikh","year":"1971","unstructured":"Parikh, R.: Existence and Feasibility in Arithmetic. Journal of Symbolic Logic\u00a036, 494\u2013508 (1971)","journal-title":"Journal of Symbolic Logic"},{"key":"32_CR13","unstructured":"Paris, J., Wilkie, A.: \u03940 Sets and Induction. In: Proceedings of the Jadswin Logic Conference (Poland), pp. 237\u2013248. Leeds University Press (1981)"},{"key":"32_CR14","doi-asserted-by":"publisher","first-page":"423","DOI":"10.2307\/2274231","volume":"50","author":"P. Pudl\u00e1k","year":"1985","unstructured":"Pudl\u00e1k, P.: Cuts Consistency Statements and Interpretations. Journal of Symbolic Logic\u00a050, 423\u2013442 (1985)","journal-title":"Journal of Symbolic Logic"},{"key":"32_CR15","doi-asserted-by":"crossref","unstructured":"Pudl\u00e1k, P.: On the Lengths of Proofs of Consistency, in Collegium Logicum: Annals of the Kurt G\u00f6del Society, vol.\u00a02, pp. 65\u201386 (1996); published by Springer- Wien-NewYork in cooperation with Technische Universit\u00e4t Wien","DOI":"10.1007\/978-3-7091-9461-4_5"},{"key":"32_CR16","unstructured":"Robinson, R.: An Essentially Undecidable Axiom System. In: Proceedings of 1950 International Congress on Mathematics, pp. 729\u2013730 (1950); page 157 of ref. [10]"},{"key":"32_CR17","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-86718-7","volume-title":"First Order Logic","author":"R. Smullyan","year":"1968","unstructured":"Smullyan, R.: First Order Logic. Springer, Heidelberg (1968)"},{"key":"32_CR18","unstructured":"Solovay, R.: Private Communications (1994) about Pudl\u00e1k\u2019s main theorem from [14]. See Appendix A of [24] for a 4-page summary of Solovay\u2019s idea"},{"key":"32_CR19","first-page":"897","volume-title":"Handbook on Mathematical Logic","author":"R. Statman","year":"1983","unstructured":"Statman, R.: Herbrand\u2019s theorem and Gentzen\u2019s Notion of a Direct Proof. In: Handbook on Mathematical Logic, pp. 897\u2013913. North Holland, Amsterdam (1983)"},{"key":"32_CR20","doi-asserted-by":"crossref","first-page":"39","DOI":"10.4099\/jjm1924.23.0_39","volume":"23","author":"G. Takeuti","year":"1953","unstructured":"Takeuti, G.: On a Generalized Logical Calculus. Japan. Journal on Mathematics\u00a023, 39\u201396 (1953)","journal-title":"Japan. Journal on Mathematics"},{"key":"32_CR21","volume-title":"Proof Theory, Studies in Logic","author":"G. Takeuti","year":"1987","unstructured":"Takeuti, G.: Proof Theory, Studies in Logic, vol.\u00a081. North Holland, Amsterdam (1987)"},{"key":"32_CR22","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1016\/0168-0072(87)90066-2","volume":"35","author":"A. Wilkie","year":"1987","unstructured":"Wilkie, A., Paris, J.: On the Scheme of Induction for Bounded Arithmetic. Annals on Pure and Applied Logic\u00a035, 261\u2013302 (1987)","journal-title":"Annals on Pure and Applied Logic"},{"key":"32_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/BFb0022580","volume-title":"Computational Logic and Proof Theory","author":"D. Willard","year":"1993","unstructured":"Willard, D.: Self-Verifying Axiom Systems. In: Mundici, D., Gottlob, G., Leitsch, A. (eds.) KGC 1993. LNCS, vol.\u00a0713, pp. 325\u2013336. Springer, Heidelberg (1993); See also [24] for more details"},{"key":"32_CR24","unstructured":"Willard, D.: Self-Verifying Systems, the Incompleteness Theorem & Tangibility Reflection Principle, to appear in the Journal of Symbolic Logic"},{"key":"32_CR25","doi-asserted-by":"crossref","unstructured":"Willard, D.: Self-Reflection Principles and NP-Hardness. Dimacs Series in Discrete Math &Theoretical Comp Science, vol.\u00a039, pp. 297\u2013320. AMS Press (1997)","DOI":"10.1090\/dimacs\/039\/16"},{"key":"32_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/3-540-63385-5_53","volume-title":"Computational Logic and Proof Theory","author":"D. Willard","year":"1997","unstructured":"Willard, D.: The Tangibility Reflection Principle. In: Gottlob, G., Leitsch, A., Mundici, D. (eds.) KGC 1997. LNCS, vol.\u00a01289, pp. 319\u2013334. Springer, Heidelberg (1997)"},{"key":"32_CR27","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1137\/0207018","volume":"7","author":"C. Wrathall","year":"1978","unstructured":"Wrathall, C.: Rudimentary Predicates and Relative Computation. Siam Journal on Computing\u00a07, 194\u2013209 (1978)","journal-title":"Siam Journal on Computing"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10722086_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,23]],"date-time":"2019-04-23T07:47:04Z","timestamp":1556005624000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10722086_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540676973","9783540450085"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/10722086_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}