{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T11:54:07Z","timestamp":1759146847626},"reference-count":45,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2014,1,15]],"date-time":"2014-01-15T00:00:00Z","timestamp":1389744000000},"content-version":"unspecified","delay-in-days":6620,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Bull. symb. log."],"published-print":{"date-parts":[[1995,12]]},"abstract":"<jats:p><jats:bold>\u00a71. Introduction<\/jats:bold>. The purpose of this paper is, in general, to report the state of the art of ordinal analysis and, in particular, the recent success in obtaining an ordinal analysis for the system of<jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S1079898600008039_inline1\" \/>-analysis, which is the subsystem of formal second order arithmetic, Z<jats:sub>2<\/jats:sub>, with comprehension confined to<jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S1079898600008039_inline1\" \/>-formulae. The same techniques can be used to provide ordinal analyses for theories that are reducible to iterated<jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S1079898600008039_inline1\" \/>-comprehension, e.g.,<jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S1079898600008039_inline2\" \/>-comprehension. The details will be laid out in [28].<\/jats:p><jats:p>Ordinal-theoretic proof theory came into existence in 1936, springing forth from Gentzen's head in the course of his consistency proof of arithmetic. Gentzen fostered hopes that with sufficiently large constructive ordinals one could establish the consistency of analysis, i.e., Z<jats:sub>2<\/jats:sub>. Considerable progress has been made in proof theory since Gentzen's tragic death on August 4th, 1945, but an ordinal analysis of Z<jats:sub>2<\/jats:sub>is still something to be sought. However, for reasons that cannot be explained here,<jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S1079898600008039_inline1\" \/>-comprehension appears to be the main stumbling block on the road to understanding full comprehension, giving hope for an ordinal analysis of Z<jats:sub>2<\/jats:sub>in the foreseeable future.<\/jats:p><jats:p>Roughly speaking,<jats:italic>ordinally informative<\/jats:italic>proof theory attaches ordinals in a recursive representation system to proofs in a given formal system; transformations on proofs to certain canonical forms are then partially mirrored by operations on the associated ordinals. Among other things, ordinal analysis of a formal system serves to characterize its provably recursive ordinals, functions and functionals and can yield both conservation and combinatorial independence results.<\/jats:p>","DOI":"10.2307\/421132","type":"journal-article","created":{"date-parts":[[2006,5,7]],"date-time":"2006-05-07T07:08:20Z","timestamp":1146985700000},"page":"468-485","source":"Crossref","is-referenced-by-count":39,"title":["Recent Advances in Ordinal Analysis: \u03a0<sup>1<\/sup><sub>2<\/sub>\u2014 CA and Related Systems"],"prefix":"10.1017","volume":"1","author":[{"given":"Michael","family":"Rathjen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,1,15]]},"reference":[{"key":"S1079898600008039_ref018","doi-asserted-by":"publisher","DOI":"10.1007\/BF02297652"},{"key":"S1079898600008039_ref006","doi-asserted-by":"publisher","DOI":"10.2307\/2269764"},{"key":"S1079898600008039_ref031","doi-asserted-by":"publisher","DOI":"10.1007\/BF01275469"},{"key":"S1079898600008039_ref016","doi-asserted-by":"publisher","DOI":"10.1007\/BF01457953"},{"key":"S1079898600008039_ref011","first-page":"361","volume-title":"Logic colloquium '88","author":"Feferman","year":"1989"},{"key":"S1079898600008039_ref024","first-page":"261","volume-title":"Proof-theoretical analysis of IDv by the method of localpredicativity","author":"Pohlers","year":"1981"},{"key":"S1079898600008039_ref009","first-page":"445","volume-title":"Proof theory","author":"Feferman","year":"1987"},{"key":"S1079898600008039_ref026","first-page":"113","article-title":"Cut elimination for impredicative infinitary systems, part II: Ordinal analysis for iterated inductive definitions","volume":"22","author":"Pohlers","year":"1982","journal-title":"Archiv f\u00fcr Mathematische Logik und Grundlagenforschung"},{"key":"S1079898600008039_ref020","volume-title":"Eine beweistheoretische Untersuchung von \u2014 CA + BI und verwandter Systeme","author":"J\u00e4ger","year":"1982"},{"key":"S1079898600008039_ref034","unstructured":"Schl\u00fcter A. , Provability in set theories with reflection, submitted."},{"key":"S1079898600008039_ref039","unstructured":"Setzer T. , Proof theoretical strength of Martin-l\u00f6f type theory with w-type and one universe, Thesis, University of Munich, 1993."},{"key":"S1079898600008039_ref001","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-11035-5"},{"key":"S1079898600008039_ref041","doi-asserted-by":"publisher","DOI":"10.1016\/0003-4843(78)90031-1"},{"key":"S1079898600008039_ref025","doi-asserted-by":"publisher","DOI":"10.1007\/BF02011638"},{"key":"S1079898600008039_ref012","doi-asserted-by":"publisher","DOI":"10.1090\/conm\/065\/891251"},{"key":"S1079898600008039_ref044","doi-asserted-by":"crossref","first-page":"1","DOI":"10.4099\/jjm1924.41.0_1","article-title":"The ordinals of the systems of second order arithmetic with the provably \u2013comprehension and the \u2013comprehension axiom respectively","volume":"41","author":"Takeuti","year":"1973","journal-title":"Japanese Journal of Mathematics"},{"key":"S1079898600008039_ref014","first-page":"374","volume-title":"K. G\u00f6del, Collected works, vol. III","author":"G\u00f6del","year":"1995"},{"key":"S1079898600008039_ref027","doi-asserted-by":"publisher","DOI":"10.1007\/BF01621474"},{"key":"S1079898600008039_ref002","volume-title":"Eine Erweiterung der Schnitteliminationsmethode","author":"Buchholz","year":"1977"},{"key":"S1079898600008039_ref003","first-page":"115","volume-title":"Leeds proof theory 1991","author":"Buchholz","year":"1993"},{"key":"S1079898600008039_ref028","unstructured":"Rathjen M. , An ordinal analysis of comprehension and related systems, in preparation."},{"key":"S1079898600008039_ref013","doi-asserted-by":"publisher","DOI":"10.1007\/BF00486046"},{"key":"S1079898600008039_ref042","doi-asserted-by":"publisher","DOI":"10.2307\/1970691"},{"key":"S1079898600008039_ref021","doi-asserted-by":"publisher","DOI":"10.1016\/0003-4843(72)90001-0"},{"key":"S1079898600008039_ref004","volume-title":"Iterated inductive definitions and subsystems of analysis","author":"Buchholz","year":"1981"},{"key":"S1079898600008039_ref015","doi-asserted-by":"publisher","DOI":"10.1007\/BF01278464"},{"key":"S1079898600008039_ref036","volume-title":"Beweistheorie","author":"Sch\u00fctte","year":"1960"},{"key":"S1079898600008039_ref038","first-page":"176","volume-title":"Formal systems and recursive functions","author":"Sch\u00fctte","year":"1965"},{"key":"S1079898600008039_ref035","doi-asserted-by":"publisher","DOI":"10.1007\/BF01342849"},{"key":"S1079898600008039_ref032","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(94)90074-4"},{"key":"S1079898600008039_ref033","first-page":"301","volume-title":"Generalized recursion theory","author":"Richter","year":"1973"},{"key":"S1079898600008039_ref017","doi-asserted-by":"publisher","DOI":"10.1007\/BF02011138"},{"key":"S1079898600008039_ref010","doi-asserted-by":"crossref","first-page":"364","DOI":"10.2307\/2274509","article-title":"Hilbert's program relativized: Proof-theoretical and foundational reductions","volume":"53","author":"Feferman","year":"1988","journal-title":"Journal of Symbolic Logic"},{"key":"S1079898600008039_ref007","first-page":"87","volume-title":"Lecture notes in mathematics 450","author":"Feferman","year":"1975"},{"key":"S1079898600008039_ref023","volume-title":"Intuitionistic type theory","author":"Martin-L\u00f6f","year":"1984"},{"key":"S1079898600008039_ref043","doi-asserted-by":"publisher","DOI":"10.1007\/BF00486049"},{"key":"S1079898600008039_ref019","doi-asserted-by":"publisher","DOI":"10.1007\/BF02023014"},{"key":"S1079898600008039_ref029","doi-asserted-by":"publisher","DOI":"10.1007\/BF01621475"},{"key":"S1079898600008039_ref008","first-page":"159","volume-title":"Logic colloquium '78","author":"Feferman","year":"1979"},{"key":"S1079898600008039_ref037","doi-asserted-by":"publisher","DOI":"10.1007\/BF01972460"},{"key":"S1079898600008039_ref022","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.85.18.6582"},{"key":"S1079898600008039_ref005","volume-title":"Proof theory of impredicative subsystems of analysis","author":"Buchholz","year":"1988"},{"key":"S1079898600008039_ref040","doi-asserted-by":"publisher","DOI":"10.1007\/BF02007556"},{"key":"S1079898600008039_ref030","first-page":"47","article-title":"How to develop proof\u2013theoretic ordinal f unctions on the basis of admissible sets","volume":"39","author":"Rathjen","year":"1993","journal-title":"Mathematical Quarterly"},{"key":"S1079898600008039_ref045","first-page":"31","volume-title":"Mathematical Intelligencer","author":"Woodin","year":"1994"}],"container-title":["Bulletin of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1079898600008039","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,7]],"date-time":"2023-05-07T10:15:57Z","timestamp":1683454557000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1079898600008039\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,12]]},"references-count":45,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1995,12]]}},"alternative-id":["S1079898600008039"],"URL":"https:\/\/doi.org\/10.2307\/421132","relation":{},"ISSN":["1079-8986","1943-5894"],"issn-type":[{"value":"1079-8986","type":"print"},{"value":"1943-5894","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995,12]]}}}