{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,3]],"date-time":"2023-01-03T09:15:50Z","timestamp":1672737350292},"reference-count":51,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[1988,4,1]],"date-time":"1988-04-01T00:00:00Z","timestamp":575856000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":9238,"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":[[1988,4]]},"DOI":"10.1016\/0168-0072(88)90055-3","type":"journal-article","created":{"date-parts":[[2002,7,26]],"date-time":"2002-07-26T03:45:40Z","timestamp":1027655140000},"page":"1-121","source":"Crossref","is-referenced-by-count":16,"title":["Proof-theoretical analysis: weak systems of functions and classes"],"prefix":"10.1016","volume":"38","author":[{"given":"L.","family":"Gordeev","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/0168-0072(88)90055-3_BIB1","series-title":"The L.E.J. Brouwer Centenary Symposium","first-page":"1","article-title":"The type theoretic interpretation of constructive set theory: choice principles","author":"Aczel","year":"1982"},{"key":"10.1016\/0168-0072(88)90055-3_BIB2","first-page":"5","article-title":"Die Normalfunktionen und das Problem der ausgezeichneten Folgen von Ordinalzahlen","volume":"95","author":"Bachmann","year":"1950","journal-title":"Vierteljahresschrift der Naturf. Gesellsch. Z\u00fcrich"},{"key":"10.1016\/0168-0072(88)90055-3_BIB3","series-title":"Handbook of Mathematical Logic","first-page":"1091","article-title":"The type free lambda calculus","author":"Barendregt","year":"1977"},{"key":"10.1016\/0168-0072(88)90055-3_BIB4","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1016\/S0003-4843(77)80003-X","article-title":"Principles of continuous choice and continuity of functions in formal systems for constructive mathematics","volume":"12","author":"Beeson","year":"1977","journal-title":"Annals Math. Logic"},{"key":"10.1016\/0168-0072(88)90055-3_BIB5","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2140\/pjm.1979.84.1","article-title":"Goodman's theorem and beyond","volume":"84","author":"Beeson","year":"1979","journal-title":"Pacific J. Math."},{"key":"10.1016\/0168-0072(88)90055-3_BIB6","series-title":"Foundations of Constructive Mathematics","author":"Beeson","year":"1985"},{"key":"10.1016\/0168-0072(88)90055-3_BIB7","doi-asserted-by":"crossref","first-page":"171","DOI":"10.2307\/2271898","article-title":"A simplification of the Bachmann method for generating large countable ordinals","volume":"40","author":"Bridge","year":"1975","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/0168-0072(88)90055-3_BIB8","article-title":"Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-theoretical Studies","volume":"897","author":"Buchholz","year":"1981"},{"key":"10.1016\/0168-0072(88)90055-3_BIB9","article-title":"Normalfunktionen und konstruktive Systeme von Ordinalzahlen","volume":"500","author":"Buchholz","year":"1975"},{"key":"10.1016\/0168-0072(88)90055-3_BIB10","article-title":"The \u03a9\u03bc + 1-rule","volume":"897","author":"Buchholz","year":"1981"},{"key":"10.1016\/0168-0072(88)90055-3_BIB11","article-title":"Ordinal analysis of ID\u03bd","volume":"897","author":"Buchholz","year":"1981"},{"key":"10.1016\/0168-0072(88)90055-3_BIB12","series-title":"To H.B. Curry: Essays on Combinatory Logic Lambda Calculus and Formalism","first-page":"491","article-title":"Modified realization and the formulae-as-types notion","author":"Diller","year":"1980"},{"key":"10.1016\/0168-0072(88)90055-3_BIB13","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1007\/BF00485463","article-title":"Realizability and intuitionistic logic","volume":"60","author":"Diller","year":"1984","journal-title":"Synthese"},{"key":"10.1016\/0168-0072(88)90055-3_BIB14","first-page":"87","article-title":"A language and axioms for explicit mathematics","volume":"450","author":"Feferman","year":"1975"},{"key":"10.1016\/0168-0072(88)90055-3_BIB15","first-page":"159","article-title":"Constructive theories of functions and classes","volume":"78","author":"Feferman","year":"1979"},{"key":"10.1016\/0168-0072(88)90055-3_BIB16","volume":"897","author":"Feferman","year":"1981"},{"key":"10.1016\/0168-0072(88)90055-3_BIB17","first-page":"113","article-title":"Axiomatic recursive function theory","volume":"69","author":"Friedman","year":"1971"},{"key":"10.1016\/0168-0072(88)90055-3_BIB18","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2307\/1971023","article-title":"Set-theoretic foundation for constructive analysis","volume":"105","author":"Friedman","year":"1977","journal-title":"Annals of Math."},{"key":"10.1016\/0168-0072(88)90055-3_BIB19","first-page":"21","article-title":"Classically and intuitionistically provable recursive functions","volume":"669","author":"Friedman","year":"1978"},{"key":"10.1016\/0168-0072(88)90055-3_BIB20","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","article-title":"Untersuchungen \u00fcber das logische Schliessen I, II","volume":"39","author":"Gentzen","year":"1935","journal-title":"Math. Z."},{"issue":"4","key":"10.1016\/0168-0072(88)90055-3_BIB21","doi-asserted-by":"crossref","first-page":"493","DOI":"10.1007\/BF01565428","article-title":"Die Widerspruchsfreiheit der reinen Zahlentheorie","volume":"112","author":"Gentzen","year":"1936","journal-title":"Math. Ann."},{"key":"10.1016\/0168-0072(88)90055-3_BIB22","first-page":"19","article-title":"Neue Fassung des Widerspruchsfreiheitsbeweises f\u00fcr die reine Zahlentheorie","volume":"4","author":"Gentzen","year":"1938","journal-title":"Forschungen zur Logik und zur Grundlegung der exakten Wissenschaften"},{"key":"10.1016\/0168-0072(88)90055-3_BIB23","doi-asserted-by":"crossref","first-page":"140","DOI":"10.1007\/BF01564760","article-title":"Beweisbarkeit und Unbeweisbarkeit von Anfangsf\u00e4llen der transfiniten Induktion in der reinen Zahlentheorie","volume":"119","author":"Gentzen","year":"1943","journal-title":"Math. Ann."},{"key":"10.1016\/0168-0072(88)90055-3_BIB24","doi-asserted-by":"crossref","first-page":"453","DOI":"10.2307\/2273043","article-title":"The faithfulness of the interpretation of arithmetic in the theory of constructions","volume":"38","author":"Goodman","year":"1973","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/0168-0072(88)90055-3_BIB25","doi-asserted-by":"crossref","first-page":"23","DOI":"10.2307\/2271946","article-title":"Relativized realizability in intuitionistic arithmetic of all finite types","volume":"43","author":"Goodman","year":"1978","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/0168-0072(88)90055-3_BIB26","first-page":"38","article-title":"An approach to constructivization of Cantor's theory of sets","volume":"68","author":"Gordeev","year":"1977","journal-title":"Zap. Nauchn. Semin. LOMI"},{"key":"10.1016\/0168-0072(88)90055-3_BIB27","unstructured":"L. Gordeev, A majorizing semantics for hyperarithmetic sentences, ibidem."},{"key":"10.1016\/0168-0072(88)90055-3_BIB28","series-title":"The L.E.J. Brouwer Centenary Symposium","first-page":"123","article-title":"Constructive models for set theory with extensionality","author":"Gordeev","year":"1982"},{"key":"10.1016\/0168-0072(88)90055-3_BIB29","series-title":"To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","first-page":"479","article-title":"The formulae-as-types notion of construction","author":"Howard","year":"1980"},{"key":"10.1016\/0168-0072(88)90055-3_BIB30","doi-asserted-by":"crossref","first-page":"109","DOI":"10.2307\/2269016","article-title":"On the interpretation of intuitionistic number theory","volume":"10","author":"Kleene","year":"1945","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/0168-0072(88)90055-3_BIB31","series-title":"Introduction to Matemathematics","author":"Kleene","year":"1952"},{"key":"10.1016\/0168-0072(88)90055-3_BIB32","doi-asserted-by":"crossref","first-page":"43","DOI":"10.2307\/2267457","article-title":"On the interpretation of non-finitist proofs II","volume":"17","author":"Kreisel","year":"1952","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/0168-0072(88)90055-3_BIB33","doi-asserted-by":"crossref","first-page":"321","DOI":"10.2307\/2270324","article-title":"A survey of proof theory","volume":"33","author":"Kreisel","year":"1968","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/0168-0072(88)90055-3_BIB34","series-title":"Proc. Second Scandinavian Logic Symposium","first-page":"109","article-title":"A survey of proof theory II","author":"Kreisel","year":"1971"},{"key":"10.1016\/0168-0072(88)90055-3_BIB35","doi-asserted-by":"crossref","DOI":"10.1090\/mmono\/060","volume":"60","author":"Kusner","year":"1984","journal-title":"Lectures on Constructive mathematical Analysis"},{"key":"10.1016\/0168-0072(88)90055-3_BIB36","doi-asserted-by":"crossref","first-page":"81","DOI":"10.2307\/2266681","article-title":"Algebraische und logistische Untersuchungen \u00fcber freie Verb\u00e4nde","volume":"16","author":"Lorenzen","year":"1951","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/0168-0072(88)90055-3_BIB37","first-page":"73","article-title":"An intuitionistic theory of types: predicative part","volume":"73","author":"Martin-L\u014df","year":"1975"},{"key":"10.1016\/0168-0072(88)90055-3_BIB38","series-title":"Logic Methodology and Philosophy of Science VI","first-page":"153","article-title":"Constructive mathematics and computer programming","author":"Martin-L\u014df","year":"1982"},{"issue":"4","key":"10.1016\/0168-0072(88)90055-3_BIB39","doi-asserted-by":"crossref","first-page":"548","DOI":"10.1007\/BF01091743","article-title":"Finite investigations of transfinite derivations","volume":"10","author":"Minc","year":"1978","journal-title":"J. Sov. Math."},{"key":"10.1016\/0168-0072(88)90055-3_BIB40","doi-asserted-by":"crossref","first-page":"374","DOI":"10.2307\/2272159","article-title":"Constructive set theory","volume":"40","author":"Myhill","year":"1975","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/0168-0072(88)90055-3_BIB41","article-title":"Proof-theoretical analysis of ID\u03bd by the method of local predicativity","volume":"897","author":"Pohlers","year":"1981"},{"key":"10.1016\/0168-0072(88)90055-3_BIB42","article-title":"Natural Deductions","author":"Prawitz","year":"1965"},{"key":"10.1016\/0168-0072(88)90055-3_BIB43","series-title":"Theory of Recursive Functions and Effective Computability","author":"Rogers","year":"1967"},{"key":"10.1016\/0168-0072(88)90055-3_BIB44","article-title":"Proof Theory and Intuitionistic Systems","volume":"212","author":"Scarpellini","year":"1971"},{"key":"10.1016\/0168-0072(88)90055-3_BIB45","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1007\/BF01342849","article-title":"Beweistheoretische Erfassung der unendlichen Induksion in der reinen Zahlentheorie","volume":"122","author":"Sch\u00fctte","year":"1951","journal-title":"Math. Ann."},{"key":"10.1016\/0168-0072(88)90055-3_BIB46","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/BF01343554","article-title":"Beweistheoretische Untersuchung der verzweigten Analysis","volume":"124","author":"Sch\u00fctte","year":"1952","journal-title":"Math. Ann."},{"key":"10.1016\/0168-0072(88)90055-3_BIB47","series-title":"Beweistheorie","author":"Sch\u00fctte","year":"1960"},{"key":"10.1016\/0168-0072(88)90055-3_BIB48","series-title":"Handbook of Mathematical Logic","article-title":"Proof theory: Some applications of cut-eliminations","author":"Schwichtenberg","year":"1977"},{"key":"10.1016\/0168-0072(88)90055-3_BIB49","series-title":"Proof Theory","author":"Takeuti","year":"1975"},{"key":"10.1016\/0168-0072(88)90055-3_BIB50","article-title":"Matamathematical investigation of Intuitionistic Arithmetic and Analysis","volume":"344","author":"Troelstra","year":"1973"},{"key":"10.1016\/0168-0072(88)90055-3_BIB51","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1090\/S0002-9947-1908-1500814-9","article-title":"Continuous increasing functions of finite and transfinite number classes","volume":"9","author":"Veblen","year":"1908","journal-title":"Trans. Amer. Math. Soc."}],"container-title":["Annals of Pure and Applied Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0168007288900553?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0168007288900553?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,2,5]],"date-time":"2020-02-05T11:12:01Z","timestamp":1580901121000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/0168007288900553"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1988,4]]},"references-count":51,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1988,4]]}},"alternative-id":["0168007288900553"],"URL":"https:\/\/doi.org\/10.1016\/0168-0072(88)90055-3","relation":{},"ISSN":["0168-0072"],"issn-type":[{"value":"0168-0072","type":"print"}],"subject":[],"published":{"date-parts":[[1988,4]]}}}