{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T16:33:39Z","timestamp":1742920419777,"version":"3.40.3"},"publisher-location":"Cham","reference-count":55,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030367541"},{"type":"electronic","value":"9783030367558"}],"license":[{"start":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T00:00:00Z","timestamp":1576800000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-36755-8_17","type":"book-chapter","created":{"date-parts":[[2019,12,16]],"date-time":"2019-12-16T15:05:16Z","timestamp":1576508716000},"page":"268-286","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["On the Tender Line Separating Generalizations and Boundary-Case Exceptions for the Second Incompleteness Theorem Under Semantic Tableaux Deduction"],"prefix":"10.1007","author":[{"given":"Dan E.","family":"Willard","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,12,20]]},"reference":[{"issue":"1","key":"17_CR1","first-page":"349","volume":"66","author":"Z Adamowicz","year":"2001","unstructured":"Adamowicz, Z., Bigorajska, T.: Existentially closed structures and G\u00f6del\u2019s second incompleteness theorem. JSL 66(1), 349\u2013356 (2001)","journal-title":"JSL"},{"issue":"6","key":"17_CR2","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/s001530000072","volume":"40","author":"Z Adamowicz","year":"2001","unstructured":"Adamowicz, Z., Zbierski, P.: On Herbrand consistency in weak theories. Arch. Math. Log. 40(6), 399\u2013413 (2001)","journal-title":"Arch. Math. Log."},{"issue":"1","key":"17_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2307\/2687821","volume":"7","author":"S Artemov","year":"2001","unstructured":"Artemov, S.: Explicit provablity and constructive semantics. Bull. Symb. Log. 7(1), 1\u201336 (2001)","journal-title":"Bull. Symb. Log."},{"unstructured":"Artemov, S.: The provability of consistency. Cornell Archives arXiv Report 1902.07404v4 (2019)","key":"17_CR4"},{"doi-asserted-by":"crossref","unstructured":"Artemov, S., Beklemishev, L.D.: Provability logic. In: Handbook on Philosophical Logic, 2nd edn, pp. 189-360 (2005)","key":"17_CR5","DOI":"10.1007\/1-4020-3521-7_3"},{"issue":"2","key":"17_CR6","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1070\/RM2005v060n02ABEH000823","volume":"60","author":"LD Beklemishev","year":"2005","unstructured":"Beklemishev, L.D.: Reflection principles and provability algebras in formal arithmetic. Russ. Math. Surv. 60(2), 197\u2013268 (2005)","journal-title":"Russ. Math. Surv."},{"issue":"1","key":"17_CR7","first-page":"82","volume":"165","author":"LD Beklemishev","year":"2014","unstructured":"Beklemishev, L.D.: Positive provability for uniform reflection principles. APAL 165(1), 82\u2013105 (2014)","journal-title":"APAL"},{"issue":"2","key":"17_CR8","first-page":"503","volume":"41","author":"A Bezboruah","year":"1976","unstructured":"Bezboruah, A., Shepherdson, J.C.: G\u00f6del\u2019s second incompleteness theorem for Q. JSL 41(2), 503\u2013512 (1976)","journal-title":"JSL"},{"unstructured":"Buss, S.R.: Bounded arithmetic. Studies in Proof Theory, Lecture Notes 3, disseminated by Bibliopolis as revised version of Ph.D. thesis (1986)","key":"17_CR9"},{"issue":"3","key":"17_CR10","first-page":"221","volume":"74","author":"SR Buss","year":"1995","unstructured":"Buss, S.R., Ignjatovi\u0107, A.: Unprovability of consistency statements in fragments of bounded arithmetic. APAL 74(3), 221\u2013244 (1995)","journal-title":"APAL"},{"doi-asserted-by":"crossref","unstructured":"Dawson, J.W.: Logical Dilemmas: The Life and Work of Kurt G\u00f6del. AKPeters Press (1997)","key":"17_CR11","DOI":"10.1201\/9780429294884"},{"doi-asserted-by":"crossref","unstructured":"Enderton, H.B.: A Mathematical Introduction to Logic. Academic Press (2001)","key":"17_CR12","DOI":"10.1016\/B978-0-08-049646-7.50005-9"},{"key":"17_CR13","first-page":"35","volume":"49","author":"S Feferman","year":"1960","unstructured":"Feferman, S.: Arithmetization of mathematics in a general setting. FundMath 49, 35\u201392 (1960)","journal-title":"FundMath"},{"issue":"2","key":"17_CR14","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1305\/ndjfl\/1093894722","volume":"13","author":"M Fitting","year":"1972","unstructured":"Fitting, M.: Tableau methods of proofs for modal logics. Notre Dame J. Form. Log. 13(2), 237\u2013247 (1972)","journal-title":"Notre Dame J. Form. Log."},{"key":"17_CR15","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-2360-3","volume-title":"First Order Logic and Automated Theorem Proving","author":"M Fitting","year":"1996","unstructured":"Fitting, M.: First Order Logic and Automated Theorem Proving. Springer, New York (1996). https:\/\/doi.org\/10.1007\/978-1-4612-2360-3"},{"unstructured":"Friedman, H.M.: On the consistency, completeness and correctness problems. Ohio State Tech Report (1979). See also Pudl\u00e1k [36]\u2019s summary of this result","key":"17_CR16"},{"unstructured":"Friedman, H.M.: Translatability and relative consistency. Ohio State Tech Report (1979). See also Pudl\u00e1k [36]\u2019s summary of this result","key":"17_CR17"},{"unstructured":"Friedman, H.M.: G\u00f6del\u2019s blessing and G\u00f6del\u2019s curse. (This is \u201cLecture 4\u201d within a 5-part Ohio State YouTube lecture series, dated 14 March 2014)","key":"17_CR18"},{"key":"17_CR19","doi-asserted-by":"publisher","first-page":"439","DOI":"10.1007\/BF01565428","volume":"112","author":"G Gentzen","year":"1936","unstructured":"Gentzen, G.: Die Wiederpruchsfreiheit der reinen Zahlentheorie. Math. Ann. 112, 439\u2013565 (1936)","journal-title":"Math. Ann."},{"key":"17_CR20","first-page":"349","volume":"38","author":"K G\u00f6del","year":"1931","unstructured":"G\u00f6del, K.: \u00dcber formal unentscheidbare s\u00e4tze der Principia Mathematica und verwandte systeme I. Monatshefte f\u00fcr Mathematik und Physik 38, 349\u2013360 (1931)","journal-title":"Monatshefte f\u00fcr Mathematik und Physik"},{"unstructured":"G\u00f6del, K.: The present situation in the foundations of mathematics. In: Feferman, S., Dawson, J. W., Goldfarb, W., Parsons, C., Solovay, R.M. (eds.) Collected Works Volume III: Unpublished Essays and Lectures, pp. 45\u201353, Oxford University Press (2004)","key":"17_CR21"},{"doi-asserted-by":"crossref","unstructured":"Goldstein, R.: Incompleteness: The Proof and Paradox of Kurt G\u00f6del. Norton Press (2005)","key":"17_CR22","DOI":"10.1007\/BF02984710"},{"key":"17_CR23","first-page":"155","volume":"81","author":"P H\u00e1jek","year":"2007","unstructured":"H\u00e1jek, P.: Mathematical fuzzy logic and natural numbers. FundMath 81, 155\u2013163 (2007)","journal-title":"FundMath"},{"key":"17_CR24","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1093\/jigpal\/jzp091","volume":"19","author":"P H\u00e1jek","year":"2011","unstructured":"H\u00e1jek, P.: Towards metamathematics of weak arithmetics over fuzzy logics. Log. J. IPL 19, 467\u2013475 (2011)","journal-title":"Log. J. IPL"},{"key":"17_CR25","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":"17_CR26","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/BF01206605","volume":"95","author":"D Hilbert","year":"1926","unstructured":"Hilbert, D.: \u00dcber das unendliche. Math. Ann. 95, 161\u2013191 (1926)","journal-title":"Math. Ann."},{"key":"17_CR27","first-page":"17","volume":"72","author":"R Jeroslow","year":"1971","unstructured":"Jeroslow, R.: Consistency statements in formal theories. FundMath 72, 17\u201340 (1971)","journal-title":"FundMath"},{"issue":"1","key":"17_CR28","first-page":"150","volume":"3","author":"SC Kleene","year":"1938","unstructured":"Kleene, S.C.: On notation for ordinal numbers. JSL 3(1), 150\u2013155 (1938)","journal-title":"JSL"},{"key":"17_CR29","first-page":"1","volume":"118","author":"G Kreisel","year":"1974","unstructured":"Kreisel, G., Takeuti, G.: Formally self-referential propositions for cut-free classical analysis. Dissertationes Mathematicae 118, 1\u201350 (1974)","journal-title":"Dissertationes Mathematicae"},{"unstructured":"Mendelson, E.: Introduction to Mathematical Logic. CRC Press (2010)","key":"17_CR30"},{"key":"17_CR31","doi-asserted-by":"publisher","DOI":"10.1515\/9781400858927","volume-title":"Predicative Arithmetic. Mathematics Notes","author":"E Nelson","year":"1986","unstructured":"Nelson, E.: Predicative Arithmetic. Mathematics Notes. Princeton University Press, Princeton (1986)"},{"issue":"3","key":"17_CR32","first-page":"494","volume":"36","author":"R Parikh","year":"1971","unstructured":"Parikh, R.: Existence and feasibility in arithmetic. JSL 36(3), 494\u2013508 (1971)","journal-title":"JSL"},{"issue":"3","key":"17_CR33","first-page":"564","volume":"48","author":"JB Paris","year":"1983","unstructured":"Paris, J.B., Dimitracopoulos, C.: A note on the undefinability of cuts. JSL 48(3), 564\u2013569 (1983)","journal-title":"JSL"},{"issue":"3","key":"17_CR34","first-page":"466","volume":"37","author":"C Parsons","year":"1972","unstructured":"Parsons, C.: On $$n-$$quantifier elimination. JSL 37(3), 466\u2013482 (1972)","journal-title":"JSL"},{"issue":"2","key":"17_CR35","first-page":"423","volume":"50","author":"P Pudl\u00e1k","year":"1985","unstructured":"Pudl\u00e1k, P.: Cuts, consistency statements and interpretations. JSL 50(2), 423\u2013441 (1985)","journal-title":"JSL"},{"key":"17_CR36","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/978-3-7091-9461-4_5","volume-title":"Collegium Logicum: 1996 Annals of the Kurt G\u00f6del Society","author":"P Pudl\u00e1k","year":"1996","unstructured":"Pudl\u00e1k, P.: On the lengths of proofs of consistency. In: Pudl\u00e1k, P. (ed.) Collegium Logicum: 1996 Annals of the Kurt G\u00f6del Society, vol. 2, pp. 65\u201386. Springer, NewYork (1996). https:\/\/doi.org\/10.1007\/978-3-7091-9461-4_5"},{"unstructured":"Rogers, H.A.: Theory of Recursive Functions and Effective Compatibility. McGrawHill (1967)","key":"17_CR37"},{"unstructured":"Sacks, G.: Some detailed recollections about Kurt G\u00f6del during a June 2, 2014 YouTube lecture given by Gerald Sacks at the University of Pennsylvania. This lecture records the experiences of Sacks when he was a 1-year assistant for G\u00f6del at the Institute of Advanced Studies. Some quotes from this talk are that G\u00f6del \u201cdid not think\u201d the goals of Hilbert\u2019s Consistency Program \u201cwere erased\u201d by the Incompleteness Theorem, and that G\u00f6del believed (according to Sacks) that it left Hilbert\u2019s program \u201cvery much alive and even more interesting than it initially was\u201d","key":"17_CR38"},{"unstructured":"Smullyan, R.: First Order Logic. Dover Books (1995)","key":"17_CR39"},{"issue":"1\u20132","key":"17_CR40","first-page":"102","volume":"44","author":"RM Solovay","year":"1989","unstructured":"Solovay, R.M.: Injecting Inconsistencies into models of PA. APAL 44(1\u20132), 102\u2013132 (1989)","journal-title":"APAL"},{"unstructured":"Solovay, R.M.: Private Telephone conversations during April of 1994 between Dan Willard and Robert M. Solovay. During those conversations Solovay described an unpublished generalization of one of Pudl\u00e1k\u2019s theorems [35], using some methods of Nelson and Wilkie-Paris [31,44]. (The Appendix A of [46] offers a 4-page summary of our interpretation of Solovay\u2019s remarks. Several other articles [10,25,31,33,35,44] have also noted that Solovay often has chosen to privately communicate noteworthy insights that he has elected not to formally publish)","key":"17_CR41"},{"key":"17_CR42","first-page":"347","volume":"81","author":"V \u0160vejdar","year":"2007","unstructured":"\u0160vejdar, V.: An interpretation of Robinson arithmetic in its Grzegorczjk\u2019s weaker variant. Fundamenta Informaticae 81, 347\u2013354 (2007)","journal-title":"Fundamenta Informaticae"},{"issue":"1\u20133","key":"17_CR43","first-page":"103","volume":"131","author":"A Visser","year":"2005","unstructured":"Visser, A.: Faith and falsity. APAL 131(1\u20133), 103\u2013131 (2005)","journal-title":"APAL"},{"key":"17_CR44","first-page":"261","volume":"35","author":"AJ Wilkie","year":"1987","unstructured":"Wilkie, A.J., Paris, J.B.: On the scheme of induction for bounded arithmetic. APAL 35, 261\u2013302 (1987)","journal-title":"APAL"},{"key":"17_CR45","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":"E Willard","year":"1993","unstructured":"Willard, E.: Self-verifying axiom systems. In: Gottlob, G., Leitsch, A., Mundici, D. (eds.) KGC 1993. LNCS, vol. 713, pp. 325\u2013336. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/BFb0022580"},{"issue":"2","key":"17_CR46","first-page":"536","volume":"66","author":"DE Willard","year":"2001","unstructured":"Willard, D.E.: Self-verifying systems, the incompleteness theorem and the tangibiltiy reflection principle. JSL 66(2), 536\u2013596 (2001)","journal-title":"JSL"},{"issue":"1","key":"17_CR47","first-page":"465","volume":"67","author":"DE Willard","year":"2002","unstructured":"Willard, D.E.: How to extend the semantic tableaux and cut-free versions of the second incompleteness theorem almost to Robinson\u2019s arithmetic Q. JSL 67(1), 465\u2013496 (2002)","journal-title":"JSL"},{"unstructured":"Willard, D.E.: A version of the second incompleteness theorem for axiom systems that recognize addition but not multiplication as a total function. In: Hendricks, V., Neuhaus, F., Pedersen, S.A., Sheffler, U., Wansing, H. (eds.) First Order Logic Revisited, pp. 337\u2013368, Logos Verlag, Berlin (2004)","key":"17_CR48"},{"issue":"4","key":"17_CR49","first-page":"1171","volume":"70","author":"DE Willard","year":"2005","unstructured":"Willard, D.E.: An exploration of the partial respects in which an axiom system recognizing solely addition as a total function can verify its own consistency. JSL 70(4), 1171\u20131209 (2005)","journal-title":"JSL"},{"issue":"3","key":"17_CR50","first-page":"472","volume":"141","author":"DE Willard","year":"2006","unstructured":"Willard, D.E.: A generalization of the second incompleteness theorem and some exceptions to it. APAL 141(3), 472\u2013496 (2006)","journal-title":"APAL"},{"issue":"4","key":"17_CR51","first-page":"1189","volume":"71","author":"DE Willard","year":"2006","unstructured":"Willard, D.E.: On the available partial respects in which an axiomatization for real valued arithmetic can recognize its consistency. JSL 71(4), 1189\u20131199 (2006)","journal-title":"JSL"},{"issue":"2","key":"17_CR52","first-page":"124","volume":"146","author":"DE Willard","year":"2007","unstructured":"Willard, D.E.: Passive induction and a solution to a Paris-Wilkie open question. APAL 146(2), 124\u2013149 (2007)","journal-title":"APAL"},{"issue":"10","key":"17_CR53","doi-asserted-by":"publisher","first-page":"1078","DOI":"10.1016\/j.ic.2008.11.007","volume":"207","author":"DE Willard","year":"2009","unstructured":"Willard, D.E.: Some specially formulated axiomizations for I$$\\Sigma _0$$ manage to evade the Herbrandized version of the second incompleteness theorem. Inf. Comput. 207(10), 1078\u20131093 (2009)","journal-title":"Inf. Comput."},{"unstructured":"Willard, D.E.: On how the introducing of a new $$~\\theta ~$$ function symbol into arithmetic\u2019s formalism is germane to devising axiom systems that can appreciate fragments of their own Hilbert consistency. Cornell Archives arXiv Report 1612.08071 (2016)","key":"17_CR54"},{"doi-asserted-by":"crossref","unstructured":"Yourgrau, P.: A World Without Time: The Forgotten Legacy of G\u00f6del and Einstein. (See page 58 for the passages we have quoted.) Basic Books (2005)","key":"17_CR55","DOI":"10.1063\/1.2169448"}],"container-title":["Lecture Notes in Computer Science","Logical Foundations of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-36755-8_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,24]],"date-time":"2023-09-24T02:36:51Z","timestamp":1695523011000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-36755-8_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,20]]},"ISBN":["9783030367541","9783030367558"],"references-count":55,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-36755-8_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019,12,20]]},"assertion":[{"value":"20 December 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"LFCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Logical Foundations of Computer Science","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Deerfield Beach, FL","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 January 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 January 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"lfcs2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/lfcs.ws.gc.cuny.edu\/lfcs-2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"17","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"57% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.7","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}