{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,17]],"date-time":"2025-09-17T16:16:57Z","timestamp":1758125817760},"reference-count":20,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2014,1,15]],"date-time":"2014-01-15T00:00:00Z","timestamp":1389744000000},"content-version":"unspecified","delay-in-days":3150,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Bull. symb. log."],"published-print":{"date-parts":[[2005,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The last section of \u201cLecture at Zilsel's\u201d [9, \u00a74] contains an interesting but quite condensed discussion of Gentzen's first version of his consistency proof for<jats:italic>PA<\/jats:italic>[8], reformulating it as what has come to be called the<jats:italic>no-counterexample interpretation<\/jats:italic>. I will describe Gentzen's result (in game-theoretic terms), fill in the details (with some corrections) of G\u00f6del's reformulation, and discuss the relation between the two proofs.<\/jats:p>","DOI":"10.2178\/bsl\/1120231632","type":"journal-article","created":{"date-parts":[[2005,7,1]],"date-time":"2005-07-01T15:42:07Z","timestamp":1120232527000},"page":"225-238","source":"Crossref","is-referenced-by-count":19,"title":["G\u00f6del's Reformulation of Gentzen's First Consistency Proof For Arithmetic: The No-Counterexample Interpretation"],"prefix":"10.1017","volume":"11","author":[{"given":"W. W.","family":"Tait","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,1,15]]},"reference":[{"key":"S1079898600003322_ref011","volume-title":"Gesammelte Abhandlungen","volume":"3","author":"Hilbert","year":"1935"},{"key":"S1079898600003322_ref013","first-page":"241","article-title":"On the interpretation of non-finitist proofs-Part I","volume":"16","author":"Kreisel","year":"1951","journal-title":"The Journal of Symbolic Logic"},{"key":"S1079898600003322_ref005","doi-asserted-by":"publisher","DOI":"10.2307\/2275524"},{"key":"S1079898600003322_ref008","doi-asserted-by":"publisher","DOI":"10.1007\/BF01565428"},{"key":"S1079898600003322_ref010","doi-asserted-by":"publisher","DOI":"10.1007\/BF01457953"},{"key":"S1079898600003322_ref004","doi-asserted-by":"publisher","DOI":"10.1007\/s001530000064"},{"key":"S1079898600003322_ref002","doi-asserted-by":"publisher","DOI":"10.1002\/1521-3870(200201)48:1<3::AID-MALQ3>3.0.CO;2-6"},{"key":"S1079898600003322_ref001","doi-asserted-by":"publisher","DOI":"10.1007\/BF01450016"},{"key":"S1079898600003322_ref018","doi-asserted-by":"publisher","DOI":"10.2307\/2270133"},{"key":"S1079898600003322_ref003","first-page":"409","volume-title":"Institutionism and proof theory","author":"Bernays","year":"1970"},{"key":"S1079898600003322_ref006","doi-asserted-by":"publisher","DOI":"10.1090\/pspum\/005"},{"key":"S1079898600003322_ref009","unstructured":"G\u00f6del K. , Lecture at Zilsel's, In Feferman et al. [7], pp. 87\u2013133."},{"key":"S1079898600003322_ref020","unstructured":"Tait W. W. , The no counterexample interpretation for arithmetic, unpublished manuscript."},{"key":"S1079898600003322_ref014","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-0348-8325-2"},{"key":"S1079898600003322_ref007","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780195072556.001.0001","volume-title":"Kurt Godel: Collected works, Vol. III","author":"Feferman","year":"1995"},{"key":"S1079898600003322_ref015","doi-asserted-by":"publisher","DOI":"10.1007\/BF01342849"},{"key":"S1079898600003322_ref012","doi-asserted-by":"publisher","DOI":"10.2307\/2586791"},{"key":"S1079898600003322_ref016","doi-asserted-by":"crossref","unstructured":"Spector C. , Provably recursive functionals of analysis: a consistency proof of analysis by an extension of the principles formulated in current intuitionistic mathematics, In Dekker , pp. 1\u201327.","DOI":"10.1090\/pspum\/005\/0154801"},{"key":"S1079898600003322_ref017","doi-asserted-by":"publisher","DOI":"10.2307\/2270132"},{"key":"S1079898600003322_ref019","doi-asserted-by":"publisher","DOI":"10.1093\/philmat\/9.1.87"}],"container-title":["Bulletin of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1079898600003322","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,1,27]],"date-time":"2024-01-27T15:24:08Z","timestamp":1706369048000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1079898600003322\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,6]]},"references-count":20,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2005,6]]}},"alternative-id":["S1079898600003322"],"URL":"https:\/\/doi.org\/10.2178\/bsl\/1120231632","relation":{},"ISSN":["1079-8986","1943-5894"],"issn-type":[{"value":"1079-8986","type":"print"},{"value":"1943-5894","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,6]]}}}