{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T20:05:41Z","timestamp":1761941141168,"version":"build-2065373602"},"reference-count":27,"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":6437,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Bull. symb. log."],"published-print":{"date-parts":[[1996,6]]},"abstract":"<jats:p>Apologies. The purpose of the following talk is to give an overview of the present state of aims, methods and results in Pure Proof Theory. Shortage of time forces me to concentrate on my very personal views. This entails that I will emphasize the work which I know best, i.e., work that has been done in the triangle Stanford, Munich and M\u00fcnster. I am of course well aware that there are as important results coming from outside this triangle and I apologize for not displaying these results as well.<\/jats:p><jats:p>Moreover the audience should be aware that in some points I have to oversimplify matters. Those who complain about that are invited to consult the original papers.<\/jats:p><jats:p>1.1. General. Proof theory startedwithHilbert's Programme which aimed at a finitistic consistency proof for mathematics.<\/jats:p><jats:p>By G\u00f6del's Theorems, however, we know that we can neither formalize all mathematics nor even prove the consistency of formalized fragments by finitistic means. Inspite of this fact I want to give some reasons why I consider proof theory in the style of Gentzen's work still as an important and exciting field of Mathematical Logic. I will not go into applications of Gentzen's cut-elimination technique to computer science problems\u2014this may be considered as applied proof theory\u2014but want to concentrate on metamathematical problems and results. In this sense I am talking about <jats:italic>Pure Proof Theory<\/jats:italic>.<\/jats:p><jats:p>Mathematicians are interested in structures. There is only one way to find the theorems of a structure. Start with an axiom system for the structure and deduce the theorems logically. These axiom systems are the objects of proof-theoretical research. Studying axiom systems there is a series of more or less obvious questions.<\/jats:p>","DOI":"10.2307\/421108","type":"journal-article","created":{"date-parts":[[2006,5,7]],"date-time":"2006-05-07T07:08:56Z","timestamp":1146985736000},"page":"159-188","source":"Crossref","is-referenced-by-count":7,"title":["Pure Proof Theory Aims, Methods and Results: Extended Version of Talks Given at Oberwolfach and Haifa"],"prefix":"10.1017","volume":"2","author":[{"given":"Wolfram","family":"Pohlers","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,1,15]]},"reference":[{"key":"S1079898600008738_ref017","unstructured":"[17] Rathjen M. , Untersuchungen zu Teilsystemen der Zahlentheorie zweiter Stufe und der Mengenlehre mit einer zwischen ( -CA) und ( -CA) + (BI) liegenden Beweisst\u00e4rke, Ph.D. thesis, M\u00fcnster, 1989."},{"key":"S1079898600008738_ref019","doi-asserted-by":"publisher","DOI":"10.1007\/BF01275469"},{"key":"S1079898600008738_ref011","first-page":"69","article-title":"Cut elimination for impredicative infinitary systems, Part I","volume":"21","author":"Pohlers","year":"1981","journal-title":"Archive for Mathematical Logic"},{"key":"S1079898600008738_ref008","article-title":"A well-ordering proof for Fefermans theory T0","volume":"22","author":"J\u00e4ger","year":"1983","journal-title":"Archive for Mathematical Logic"},{"volume-title":"Theories for Admissible Sets: A Unifying Approach to Proof Theory","year":"1986","author":"J\u00e4ger","key":"S1079898600008738_ref009"},{"volume-title":"Proof Theory","year":"1975","author":"Takeuti","key":"S1079898600008738_ref026"},{"key":"S1079898600008738_ref018","doi-asserted-by":"publisher","DOI":"10.1007\/BF01621475"},{"key":"S1079898600008738_ref006","doi-asserted-by":"publisher","DOI":"10.2307\/2269764"},{"key":"S1079898600008738_ref027","unstructured":"[27] Weiermann A. , How to characterize provably total functions by local predicativity, to appear in Journal of Symbolic Logic ."},{"key":"S1079898600008738_ref013","first-page":"113","article-title":"Cut elimination for impredicative infinitary systems, Part II","volume":"22","author":"Pohlers","year":"1982","journal-title":"Archive for Mathematical Logic"},{"key":"S1079898600008738_ref002","unstructured":"[2] Blankertz B. and Weiermann A. , A uniform approach for characterizing the provably total number theoretic functions of KPM and its subsystems, to appear."},{"volume-title":"Provability in set theories with reflection","year":"1995","author":"Schl\u00fcter","key":"S1079898600008738_ref022"},{"key":"S1079898600008738_ref004","first-page":"664","article-title":"A uniform approach to fundamental sequences and hierarchies","volume":"58","author":"Buchholz","year":"1993","journal-title":"Mathematical Logic Quarterly"},{"key":"S1079898600008738_ref007","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0062852"},{"key":"S1079898600008738_ref021","unstructured":"[21] Schl\u00fcter A. , Zur Mengenexistenz in formalen Theorien der Mengenlehre, Ph.D. thesis, M\u00fcnster, 1994."},{"volume-title":"Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies","year":"1981","author":"Pohlers","key":"S1079898600008738_ref012"},{"key":"S1079898600008738_ref020","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(94)90074-4"},{"key":"S1079898600008738_ref010","first-page":"1","volume-title":"Sitzungsberichte der Bayerischen Akademie der Wissenschaften, Mathematik-Naturwissenschaft Klasse","author":"J\u00e4ger","year":"1982"},{"volume-title":"Proof Theory","year":"1992","author":"Pohlers","key":"S1079898600008738_ref016"},{"key":"S1079898600008738_ref014","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-46825-7"},{"key":"S1079898600008738_ref025","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-66473-1"},{"key":"S1079898600008738_ref024","first-page":"176","volume-title":"Formal Systems and Recursive Functions","author":"Sch\u00fctte","year":"1965"},{"key":"S1079898600008738_ref023","doi-asserted-by":"publisher","DOI":"10.1007\/BF01972460"},{"volume-title":"Proof Theory","year":"1992","author":"Buchholz","key":"S1079898600008738_ref003"},{"key":"S1079898600008738_ref015","doi-asserted-by":"publisher","DOI":"10.1007\/BF01621474"},{"key":"S1079898600008738_ref001","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-11035-5"},{"key":"S1079898600008738_ref005","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0091894"}],"container-title":["Bulletin of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1079898600008738","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,12]],"date-time":"2019-05-12T21:24:29Z","timestamp":1557696269000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1079898600008738\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,6]]},"references-count":27,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1996,6]]}},"alternative-id":["S1079898600008738"],"URL":"https:\/\/doi.org\/10.2307\/421108","relation":{},"ISSN":["1079-8986","1943-5894"],"issn-type":[{"type":"print","value":"1079-8986"},{"type":"electronic","value":"1943-5894"}],"subject":[],"published":{"date-parts":[[1996,6]]}}}