{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T15:33:40Z","timestamp":1726068820921},"reference-count":62,"publisher":"Elsevier BV","issue":"1-3","license":[{"start":{"date-parts":[[2003,2,1]],"date-time":"2003-02-01T00:00:00Z","timestamp":1044057600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,8,22]],"date-time":"2013-08-22T00:00:00Z","timestamp":1377129600000},"content-version":"vor","delay-in-days":3855,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Annals of Pure and Applied Logic"],"published-print":{"date-parts":[[2003,2]]},"DOI":"10.1016\/s0168-0072(02)00040-4","type":"journal-article","created":{"date-parts":[[2002,10,10]],"date-time":"2002-10-10T17:33:13Z","timestamp":1034271193000},"page":"191-223","source":"Crossref","is-referenced-by-count":5,"title":["Universes over Frege structures"],"prefix":"10.1016","volume":"119","author":[{"given":"Reinhard","family":"Kahle","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S0168-0072(02)00040-4_BIB1","unstructured":"P. Aczel, The strength of Martin L\u00f6f's intuitionistic type theory with one universe, in: S. Miettinen, J. V\u00e4\u00e4n\u00e4nen (Eds.), Proceedings of the Symposiums on Mathematical Logic in Oulo 1974 and in Helsinki 1975, Report No. 2, Department of Philosophy, University of Helsinki, 1977."},{"key":"10.1016\/S0168-0072(02)00040-4_BIB2","series-title":"The Kleene Symposium","first-page":"31","article-title":"Frege structures and the notion of proposition, truth and set","author":"Aczel","year":"1980"},{"key":"10.1016\/S0168-0072(02)00040-4_BIB3","series-title":"Admissible Sets and Structures","author":"Barwise","year":"1975"},{"key":"10.1016\/S0168-0072(02)00040-4_BIB4","unstructured":"M. Beeson, Foundations of Constructive Mathematics, Ergebnisse der Mathematik und ihrer Grenzgebiete; 3.Folge, Bd. 6, Springer, Berlin, 1985."},{"key":"10.1016\/S0168-0072(02)00040-4_BIB5","article-title":"Iterated Inductive Definitions and Subsystems of Analysis: recent Proof-Theoretical Studies","volume":"Vol. 897","author":"Buchholz","year":"1981"},{"key":"10.1016\/S0168-0072(02)00040-4_BIB6","unstructured":"A. Cantini, A note on a predicatively reducible theory of iterated elementary induction, Bull. Unione Math. Italiana, Serie VI, IV-B (2) (1985) 413\u2013430."},{"key":"10.1016\/S0168-0072(02)00040-4_BIB7","doi-asserted-by":"crossref","first-page":"360","DOI":"10.2307\/2274059","article-title":"On the relationship between choice and comprehension principles in second order arithmetic","volume":"51","author":"Cantini","year":"1986","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S0168-0072(02)00040-4_BIB8","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1002\/malq.19890350202","article-title":"Notes on formal theories of truth","volume":"35","author":"Cantini","year":"1989","journal-title":"Z. Math. Logik Grundlag. Math."},{"issue":"1","key":"10.1016\/S0168-0072(02)00040-4_BIB9","doi-asserted-by":"crossref","first-page":"244","DOI":"10.2307\/2274965","article-title":"A theory of formal truth arithmetically equivalent to ID1","volume":"55","author":"Cantini","year":"1990","journal-title":"J. Symbolic Logic"},{"issue":"2","key":"10.1016\/S0168-0072(02)00040-4_BIB10","doi-asserted-by":"crossref","first-page":"477","DOI":"10.2307\/2275216","article-title":"Extending the first-order theory of combinators with self-referential truth","volume":"58","author":"Cantini","year":"1993","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S0168-0072(02)00040-4_BIB11","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1305\/ndjfl\/1040248454","article-title":"Levels of truth","volume":"36","author":"Cantini","year":"1995","journal-title":"Notre Dame J. Formal Logic"},{"key":"10.1016\/S0168-0072(02)00040-4_BIB12","series-title":"Logical Frameworks for Truth and Abstraction","author":"Cantini","year":"1996"},{"key":"10.1016\/S0168-0072(02)00040-4_BIB13","series-title":"Algebra and Logic","first-page":"87","article-title":"A language and axioms for explicit mathematics","volume":"Vol. 450","author":"Feferman","year":"1975"},{"key":"10.1016\/S0168-0072(02)00040-4_BIB14","series-title":"Logic Colloquium 78","first-page":"159","article-title":"Constructive theories of functions and classes","author":"Feferman","year":"1979"},{"key":"10.1016\/S0168-0072(02)00040-4_BIB15","series-title":"Patras Logic Symposion","first-page":"171","article-title":"Iterated inductive fixed-point theories","author":"Feferman","year":"1982"},{"issue":"2","key":"10.1016\/S0168-0072(02)00040-4_BIB16","doi-asserted-by":"crossref","first-page":"364","DOI":"10.2307\/2274509","article-title":"Hilbert's program relativized","volume":"53","author":"Feferman","year":"1988","journal-title":"J. Symbolic Logic"},{"issue":"1\u20132","key":"10.1016\/S0168-0072(02)00040-4_BIB17","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1023\/A:1005622403850","article-title":"Does reductive proof theory have a viable rationale?","volume":"53","author":"Feferman","year":"2000","journal-title":"Erkenntnis"},{"issue":"3","key":"10.1016\/S0168-0072(02)00040-4_BIB18","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1016\/0168-0072(93)90013-4","article-title":"Systems of explicit mathematics with non-constructive \u03bc-operator. Part I","volume":"65","author":"Feferman","year":"1993","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/S0168-0072(02)00040-4_BIB19","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1016\/0168-0072(95)00028-3","article-title":"Systems of explicit mathematics with non-constructive \u03bc-operator. Part II","volume":"79","author":"Feferman","year":"1996","journal-title":"Ann. Pure Appl. Logic"},{"issue":"1\u20133","key":"10.1016\/S0168-0072(02)00040-4_BIB20","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1016\/S0168-0072(00)00008-7","article-title":"The unfolding of non-finitist arithmetic","volume":"104","author":"Feferman","year":"2000","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/S0168-0072(02)00040-4_BIB21","series-title":"Mathematical Logic and Theoretical Computer Science","first-page":"197","article-title":"An extension of Frege structures","author":"Flagg","year":"1987"},{"key":"10.1016\/S0168-0072(02)00040-4_BIB22","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1016\/0168-0072(87)90040-6","article-title":"Implication and analysis in classical Frege structures","volume":"34","author":"Flagg","year":"1987","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/S0168-0072(02)00040-4_BIB23","unstructured":"T. Gla\u00df, Standardstrukturen f\u00fcr Systeme Expliziter Mathematik, Ph.D. Thesis, Westf\u00e4lische Wilhelms-Universit\u00e4t M\u00fcnster, 1993."},{"issue":"1\u20132","key":"10.1016\/S0168-0072(02)00040-4_BIB24","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1016\/0168-0072(94)00058-B","article-title":"Understanding uniformity in Feferman's explicit mathematics","volume":"75","author":"Gla\u00df","year":"1995","journal-title":"Ann. Pure Appl. Logic"},{"issue":"2","key":"10.1016\/S0168-0072(02)00040-4_BIB25","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1016\/S0168-0072(96)00005-X","article-title":"Systems of explicit mathematics with non-constructive \u03bc-operator and join","volume":"82","author":"Gla\u00df","year":"1996","journal-title":"Ann. Pure Appl. Logic"},{"issue":"3","key":"10.1016\/S0168-0072(02)00040-4_BIB26","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1142\/S0129054195000135","article-title":"A new formulation of Feferman's system of functions and classes and its relation to Frege structures","volume":"6","author":"Hayashi","year":"1995","journal-title":"Internat. J. Found. Comput. Sci."},{"key":"10.1016\/S0168-0072(02)00040-4_BIB27","series-title":"Recursion-Theoretic Hierarchies","author":"Hinman","year":"1978"},{"key":"10.1016\/S0168-0072(02)00040-4_BIB28","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/BF02011138","article-title":"Beweistheorie von KPN","volume":"20","author":"J\u00e4ger","year":"1980","journal-title":"Arch. Math. Logik Grundlag."},{"issue":"3","key":"10.1016\/S0168-0072(02)00040-4_BIB29","doi-asserted-by":"crossref","first-page":"867","DOI":"10.2307\/2274140","article-title":"The strength of admissibility without foundation","volume":"49","author":"J\u00e4ger","year":"1984","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S0168-0072(02)00040-4_BIB30","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1016\/0168-0072(93)90039-G","article-title":"Fixed points in Peano arithmetic with ordinals","volume":"60","author":"J\u00e4ger","year":"1993","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/S0168-0072(02)00040-4_BIB31","unstructured":"G. J\u00e4ger, Metapredicative and explicit Mahlo: a proof-theoretic perspective, in: Logic Colloquium 2000, Lecture Note in Logic, ed., A.K. Peters, Natick, 200x, to appear."},{"issue":"1","key":"10.1016\/S0168-0072(02)00040-4_BIB32","doi-asserted-by":"crossref","first-page":"53","DOI":"10.2307\/2586750","article-title":"The proof-theoretic analysis of transfinitely iterated fixed point theories","volume":"64","author":"J\u00e4ger","year":"1999","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S0168-0072(02)00040-4_BIB33","series-title":"Logic and Foundation of Mathematics","first-page":"88","article-title":"On applicative theories","author":"J\u00e4ger","year":"1999"},{"issue":"3","key":"10.1016\/S0168-0072(02)00040-4_BIB34","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1016\/S0168-0072(00)00057-9","article-title":"Universes in explicit mathematics","volume":"109","author":"J\u00e4ger","year":"2001","journal-title":"Ann. Pure Appl. Logic"},{"issue":"6","key":"10.1016\/S0168-0072(02)00040-4_BIB35","doi-asserted-by":"crossref","first-page":"345","DOI":"10.1007\/BF02391553","article-title":"Second order theories with ordinals and elementary comprehension","volume":"34","author":"J\u00e4ger","year":"1995","journal-title":"Arch. Math. Logic"},{"key":"10.1016\/S0168-0072(02)00040-4_BIB36","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1016\/0168-0072(94)00037-4","article-title":"Totality in applicative theories","volume":"74","author":"J\u00e4ger","year":"1995","journal-title":"Ann. Pure Appl. Logic"},{"issue":"3","key":"10.1016\/S0168-0072(02)00040-4_BIB37","doi-asserted-by":"crossref","first-page":"818","DOI":"10.2307\/2275787","article-title":"Some theories with positive induction of ordinal strength \u03d5\u03c9 0","volume":"61","author":"J\u00e4ger","year":"1996","journal-title":"J. Symbolic Logic"},{"issue":"2","key":"10.1016\/S0168-0072(02)00040-4_BIB38","doi-asserted-by":"crossref","first-page":"935","DOI":"10.2307\/2695054","article-title":"Upper bounds for metapredicative Mahlo in explicit mathematics and admissible set theory","volume":"66","author":"J\u00e4ger","year":"2001","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S0168-0072(02)00040-4_BIB39","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1016\/S0168-0072(01)00076-8","article-title":"Extending the system T0 of explicit mathematics: the limit and Mahlo axioms","volume":"114","author":"J\u00e4ger","year":"2002","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/S0168-0072(02)00040-4_BIB40","unstructured":"R. Kahle, Applikative Theorien und Frege-Strukturen, Ph.D. Thesis, Institut f\u00fcr Informatik und angewandte Mathematik, Universit\u00e4t Bern, 1997."},{"key":"10.1016\/S0168-0072(02)00040-4_BIB41","unstructured":"R. Kahle, Uniform limit in explicit mathematics with universes, Technical Report IAM-97-002, IAM, Universit\u00e4t Bern, 1997."},{"issue":"5","key":"10.1016\/S0168-0072(02)00040-4_BIB42","doi-asserted-by":"crossref","first-page":"683","DOI":"10.1093\/logcom\/9.5.683","article-title":"Frege structures for partial applicative theories","volume":"9","author":"Kahle","year":"1999","journal-title":"J. Logic Comput."},{"issue":"1","key":"10.1016\/S0168-0072(02)00040-4_BIB43","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1023\/A:1011954206722","article-title":"Truth in applicative theories","volume":"68","author":"Kahle","year":"2001","journal-title":"Stud. Logica"},{"key":"10.1016\/S0168-0072(02)00040-4_BIB44","series-title":"Intuitionistic Type Theory","author":"Martin-L\u00f6f","year":"1984"},{"key":"10.1016\/S0168-0072(02)00040-4_BIB45","series-title":"Computer Science Logic \u201992","first-page":"340","article-title":"Universes in the theory of types and names","volume":"Vol. 702","author":"Marzetta","year":"1993"},{"key":"10.1016\/S0168-0072(02)00040-4_BIB46","unstructured":"M. Marzetta, Predicative theories of types and names, Ph.D. Thesis, Universti\u00e4t Bern, Institut f\u00fcr Informatik und angewandte Mathematik, 1994."},{"issue":"5\u20136","key":"10.1016\/S0168-0072(02)00040-4_BIB47","doi-asserted-by":"crossref","first-page":"391","DOI":"10.1007\/s001530050105","article-title":"The \u03bc quantification operator in explicit mathematics with universes and iterated fixed point theories with ordinals","volume":"37","author":"Marzetta","year":"1998","journal-title":"Arch. Math. Logic"},{"key":"10.1016\/S0168-0072(02)00040-4_BIB48","article-title":"Proof Theory","volume":"Vol. 1407","author":"Pohlers","year":"1989"},{"issue":"1","key":"10.1016\/S0168-0072(02)00040-4_BIB49","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s001530050001","article-title":"The strength of Martin-L\u00f6f type theory with a superuniverse. Part I","volume":"39","author":"Rathjen","year":"2000","journal-title":"Arch. Math. Logic"},{"issue":"3","key":"10.1016\/S0168-0072(02)00040-4_BIB50","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1007\/s001530000051","article-title":"The strength of Martin-L\u00f6f type theory with a superuniverse. Part II","volume":"40","author":"Rathjen","year":"2001","journal-title":"Arch. Math. Logic"},{"key":"10.1016\/S0168-0072(02)00040-4_BIB51","unstructured":"C. R\u00fcede, Metapredicative subsystems of analysis, Ph.D. Thesis, Universit\u00e4t Bern, Institut f\u00fcr Informatik und angewandte Mathematik, 2000."},{"key":"10.1016\/S0168-0072(02)00040-4_BIB52","unstructured":"C. R\u00fcede, Dependent choice and \u03c9 model reflection, J. Symbolic Logic, 200x, to appear."},{"key":"10.1016\/S0168-0072(02)00040-4_BIB53","unstructured":"C. R\u00fcede, Universes in metapredicative analysis, Arch. Math. Logic, 200x, to appear."},{"key":"10.1016\/S0168-0072(02)00040-4_BIB54","article-title":"Proof Theory","volume":"Vol. 225","author":"Sch\u00fctte","year":"1977"},{"key":"10.1016\/S0168-0072(02)00040-4_BIB55","series-title":"\u03bb-Calculus and Computer Science Theory","first-page":"1","article-title":"Combinators and classes","volume":"Vol. 37","author":"Scott","year":"1975"},{"key":"10.1016\/S0168-0072(02)00040-4_BIB56","series-title":"Sets and Proofs","first-page":"301","article-title":"Ordinal systems","volume":"Vol. 258","author":"Setzer","year":"1999"},{"key":"10.1016\/S0168-0072(02)00040-4_BIB57","series-title":"Subsystems of Second Order Arithmetic, Perspectives in Mathematical Logic","author":"Simpson","year":"1999"},{"key":"10.1016\/S0168-0072(02)00040-4_BIB58","unstructured":"T. Strahm, On the proof theory of applicative theories, Ph.D. Thesis, Universit\u00e4t Bern, Institut f\u00fcr Informatik und angewandte Mathematik, 1996."},{"key":"10.1016\/S0168-0072(02)00040-4_BIB59","series-title":"Sets and Proofs","first-page":"383","article-title":"First steps into metapredicativity in explicit mathematics","volume":"Vol. 258","author":"Strahm","year":"1999"},{"key":"10.1016\/S0168-0072(02)00040-4_BIB60","series-title":"Logic Colloquium \u201998","first-page":"449","article-title":"Autonomous fixed point progressions and fixed point transfinite recursion","volume":"Vol. 13","author":"Strahm","year":"2000"},{"issue":"1\u20133","key":"10.1016\/S0168-0072(02)00040-4_BIB61","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1016\/S0168-0072(00)00016-6","article-title":"The non-constructive \u03bc-operator, fixed point theories with ordinals, and the bar rule","volume":"104","author":"Strahm","year":"2000","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/S0168-0072(02)00040-4_BIB62","series-title":"The Syntax and Semantic of Infinitary Languages","first-page":"204","article-title":"Normal derivability in classical logic","volume":"Vol. 72","author":"Tait","year":"1968"}],"container-title":["Annals of Pure and Applied Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0168007202000404?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0168007202000404?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2023,4,18]],"date-time":"2023-04-18T20:27:03Z","timestamp":1681849623000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0168007202000404"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,2]]},"references-count":62,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2003,2]]}},"alternative-id":["S0168007202000404"],"URL":"https:\/\/doi.org\/10.1016\/s0168-0072(02)00040-4","relation":{},"ISSN":["0168-0072"],"issn-type":[{"value":"0168-0072","type":"print"}],"subject":[],"published":{"date-parts":[[2003,2]]}}}