{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:14:00Z","timestamp":1725455640824},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540571841"},{"type":"electronic","value":"9783540479437"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/bfb0022580","type":"book-chapter","created":{"date-parts":[[2005,11,13]],"date-time":"2005-11-13T06:14:45Z","timestamp":1131862485000},"page":"325-336","source":"Crossref","is-referenced-by-count":8,"title":["Self-verifying axiom systems"],"prefix":"10.1007","author":[{"given":"E.","family":"Dan Willard","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,11]]},"reference":[{"key":"34_CR1","unstructured":"G. Boolos, The Unprovability of Consistency: An Essay on Modal Logic Cambridge University Press, 1979."},{"key":"34_CR2","doi-asserted-by":"crossref","first-page":"503","DOI":"10.2307\/2272251","volume":"41","author":"A. Bezboruah","year":"1976","unstructured":"A. Bezboruah and J. Shepherdson, Godel's Second Incompleteness Theorem for Q, Journal of Symbolic Logic 41 (1976) pp. 503\u2013512.","journal-title":"Journal of Symbolic Logic"},{"key":"34_CR3","unstructured":"S. Buss, Polynomial Hierarchy and Fragments of Bounded, Proceedings of 17th Annual ACM Symposium on Theory of Computing (1985) pp. 285\u2013290"},{"key":"34_CR4","unstructured":"S. Buss, Bounded Arithmetic, Princeton Ph. D. dissertation published in Proof Theory Lecture Notes #3 by Bibliopolic (1986), see also [Bu85]."},{"key":"34_CR5","unstructured":"S. Buss, private communications."},{"key":"34_CR6","unstructured":"H. Enderton A Mathematical Introduction to Logic Academic Press 1972."},{"key":"34_CR7","doi-asserted-by":"crossref","first-page":"35","DOI":"10.4064\/fm-49-1-35-92","volume":"49","author":"S. Feferman","year":"1960","unstructured":"S. Feferman, Arithmetization of Metamathematics in a General Setting, Fundamenta Mathematicae 49 (1960) pp. 35\u201392.","journal-title":"Fundamenta Mathematicae"},{"key":"34_CR8","doi-asserted-by":"crossref","unstructured":"S. Feferman, Finitary Inductively Presented Logics, in Proceedings of Logic Colloquium 88, North Holland Publishing House (1989) pp. 191\u2013220.","DOI":"10.1016\/S0049-237X(08)70270-2"},{"key":"34_CR9","doi-asserted-by":"crossref","unstructured":"M. Fitting, First Order Logic and Automated Theorem Proving, Springer Verlag Monograph in Computer Science, 1990.","DOI":"10.1007\/978-1-4684-0357-2"},{"key":"34_CR10","unstructured":"G. Gentzen Collected Papers, translated by M.E. Szabo, North Holland, 1969."},{"key":"34_CR11","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/BF01700692","volume":"38","author":"K. Godel","year":"1931","unstructured":"K. Godel, Uber formal unentscheidbare Satze der Principia Mathematica und verwandter Systeme, I, Monatsh Math Phys, 38, (1931) pp. 173\u2013198.","journal-title":"Monatsh Math Phys"},{"key":"34_CR12","unstructured":"D. Hilbert and B. Bernays, Grundlager der Mathematik Volume 1 (1934) and Volume 2 (1939), Springer."},{"key":"34_CR13","doi-asserted-by":"crossref","first-page":"17","DOI":"10.4064\/fm-72-1-17-40","volume":"51","author":"R. Jeroslow","year":"1971","unstructured":"R. Jeroslow, Consistency Statements in Formal Mathematics, Fundamentae Mathematicae 51 (1971) pp. 17\u201340.","journal-title":"Fundamentae Mathematicae"},{"key":"34_CR14","doi-asserted-by":"crossref","first-page":"321","DOI":"10.2307\/2270324","volume":"33","author":"G. Kriesel","year":"1968","unstructured":"G. Kriesel, A Survey of Proof Theory, Part I in Journal of Symbolic Logic 33 (1968) pp. 321\u2013388 (see especially footnote 8 and page 349); Part II in Proceedings of Second Scandinavian Logic Symposium (1971) North Holland Press (with Fenstad ed.), Amsterdam (see especially pp. 117(d) & 166).","journal-title":"Journal of Symbolic Logic"},{"key":"34_CR15","first-page":"1","volume":"118","author":"G. Kriesel","year":"1974","unstructured":"G. Kriesel and G. Takeuti, Formally self-referential propositions for cut-free classical analysis and related systems, Dissertations Mathematica 118, 1974 pp. 1\u201355.","journal-title":"Dissertations Mathematica"},{"key":"34_CR16","doi-asserted-by":"crossref","first-page":"115","DOI":"10.2307\/2266895","volume":"20","author":"M. Lob","year":"1955","unstructured":"M. Lob, Solution of a Problem of Leon Henkin, Journal of Symbolic Logic 20 (1955) pp. 115\u2013118.","journal-title":"Journal of Symbolic Logic"},{"key":"34_CR17","doi-asserted-by":"crossref","unstructured":"E. Mendelson, Introduction to Mathematical Logic, Wadsworth & Brooks\/Cole Mathematics Series, 1987.","DOI":"10.1007\/978-1-4615-7288-6"},{"key":"34_CR18","unstructured":"H. Rogers, Theory of Recursive Functions and Effective Compatibility, McGraw Hill 1967, see especially pp. 186\u2013188."},{"key":"34_CR19","unstructured":"H. Schwichteberg, Proof Theory: Some Applications of Cut Elimination, in Handbook on Mathematical Logic, North Holland Publishing House (1983) pp. 867\u2013896."},{"key":"34_CR20","unstructured":"R. Statman, Herbrand's theorem and Gentzen's Notion of a Direct Proof, in Handbook on Mathematical Logic, North Holland Publishing House (1983) pp. 897\u2013913."},{"key":"34_CR21","doi-asserted-by":"crossref","unstructured":"R. Smullyan, The Theory of Formal Systems, Princeton University Press, 1961.","DOI":"10.1515\/9781400882007"},{"key":"34_CR22","doi-asserted-by":"crossref","unstructured":"R. Smullyan, First Order Logic, Springer-Verlag, 1968.","DOI":"10.1007\/978-3-642-86718-7"},{"key":"34_CR23","doi-asserted-by":"crossref","unstructured":"C. Smorynski, The Incompleteness Theorem Handbook on Mathematical Logic, pp. 821\u2013866, 1983.","DOI":"10.1016\/S0049-237X(08)71123-6"},{"key":"34_CR24","doi-asserted-by":"crossref","first-page":"39","DOI":"10.4099\/jjm1924.23.0_39","volume":"23","author":"G. Takeuti","year":"1953","unstructured":"G. Takeuti, On a Generalized Logical Calculus, Japan Journal on Mathematics 23 (1953) pp. 39\u201396.","journal-title":"Japan Journal on Mathematics"},{"key":"34_CR25","unstructured":"G. Takeuti, Proof Theory, Studies in Logic Volume 81, North Holland, 1987."},{"key":"34_CR26","doi-asserted-by":"crossref","unstructured":"D. Willard, Quasi-Linear Algorithms for Processing Relational Calculus Expressions, Proc of ACM's PODS-1990 Conf, pp 243\u2013257. This reference may be helpful as an optimization technique to help render an efficient computer implementation of IS. (Much further optimization will clearly be greatly needed.)","DOI":"10.1145\/298514.298570"},{"key":"34_CR27","doi-asserted-by":"crossref","unstructured":"D. Willard, Self-Verifying Axiom Systems and their Implications, (the unabrideged version of the present article), SUNY-Albany Tech Report, 1993.","DOI":"10.1007\/BFb0022580"}],"container-title":["Lecture Notes in Computer Science","Computational Logic and Proof Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0022580","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,5]],"date-time":"2023-05-05T10:56:22Z","timestamp":1683284182000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0022580"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540571841","9783540479437"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/bfb0022580","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1993]]}}}