{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,27]],"date-time":"2023-09-27T16:46:39Z","timestamp":1695833199126},"reference-count":19,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":8412,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1991,3]]},"abstract":"<jats:p>In this paper, we show the normalization of proofs of NF (Quine's <jats:italic>New Foundations<\/jats:italic>; see [15]) minus extensionality. This system, called SF (<jats:italic>Stratified Foundations<\/jats:italic>) differs in many respects from the associated system of simple type theory. It is written in a first order language and not in a multi-sorted one, and the formulas need not be stratifiable, except in the instances of the comprehension scheme. There is a universal set, but, for a similar reason as in type theory, the paradoxical sets cannot be formed.<\/jats:p><jats:p>It is not immediately apparent, however, that SF is essentially richer than type theory. But it follows from Specker's celebrated result (see [16] and [4]) that the stratifiable formula (<jats:italic>extensionality \u2192 the universe is not well-orderable<\/jats:italic>) is a theorem of SF.<\/jats:p><jats:p>It is known (see [11]) that this set theory is consistent, though the consistency of NF is still an open problem.<\/jats:p><jats:p>The connections between consistency and cut-elimination are rather loose. Cut-elimination generally implies consistency. But the converse is not true. In the case of set theory, for example, ZF-like systems, though consistent, cannot be freed of cuts because the separation axioms allow the formation of sets from unstratifiable formulas. There are nevertheless interesting partial results obtained when restrictions are imposed on the removable cuts (see [1] and [9]). The systems with stratifiable comprehension are the only known set-theoretic systems that enjoy full cut-elimination.<\/jats:p>","DOI":"10.2307\/2274915","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T18:38:25Z","timestamp":1146940705000},"page":"213-226","source":"Crossref","is-referenced-by-count":6,"title":["Stratification and cut-elimination"],"prefix":"10.1017","volume":"56","author":[{"given":"Marcel","family":"Crabb\u00e9","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200025019_ref015","doi-asserted-by":"publisher","DOI":"10.2307\/2300564"},{"key":"S0022481200025019_ref004","first-page":"1074","volume":"49","author":"Crabb\u00e9","year":"1984","journal-title":"Typical ambiguity and the axiom of choice"},{"key":"S0022481200025019_ref005","volume-title":"Combinatory logic","author":"Curry","year":"1968"},{"key":"S0022481200025019_ref012","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70848-6"},{"key":"S0022481200025019_ref017","first-page":"117","volume-title":"Logic, methodology and the philosophy of science","author":"Specker","year":"1962"},{"key":"S0022481200025019_ref019","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0064875"},{"key":"S0022481200025019_ref013","volume-title":"Natural deduction","author":"Prawitz","year":"1965"},{"key":"S0022481200025019_ref008","unstructured":"Girard J. Y. , Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures de l'arithm\u00e9tique d'ordre sup\u00e9rieur, Th\u00e8se, Universit\u00e9 Paris-VII, Paris, 1972."},{"key":"S0022481200025019_ref018","first-page":"198","volume":"32","author":"Tait","year":"1967","journal-title":"Intensional interpretation of functionals of finite type"},{"key":"S0022481200025019_ref009","unstructured":"Halln\u00e4s L. , On normalization of proofs in set theory, Ph.D. thesis, University of Stockholm, Stockholm, 1983."},{"key":"S0022481200025019_ref003","doi-asserted-by":"crossref","first-page":"11","DOI":"10.4064\/fm-101-1-11-17","article-title":"Ambiguity and stratification","volume":"101","author":"Crabb\u00e9","year":"1978","journal-title":"Fundamenta Mathematicae"},{"key":"S0022481200025019_ref010","first-page":"479","volume-title":"To H. B. Curry: essays on combinatory logic, lambda calculus and formalism","author":"Howard","year":"1980"},{"key":"S0022481200025019_ref002","volume-title":"\u00c9l\u00e9ments de math\u00e9matique. Livre I: Th\u00e9orie des ensembles","author":"Bourbaki","year":"1958"},{"key":"S0022481200025019_ref011","doi-asserted-by":"publisher","DOI":"10.1007\/BF00568059"},{"key":"S0022481200025019_ref001","first-page":"673","volume":"53","author":"Bailin","year":"1988","journal-title":"A normalization theorem for set theory"},{"key":"S0022481200025019_ref016","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.39.9.972"},{"key":"S0022481200025019_ref006","first-page":"391","article-title":"Lambda calculus notation with nameless dummies, a tool for automatic manipulation, with application to the Church-Rosser theorem","volume":"34","author":"de Bruijn","year":"1972","journal-title":"Indagationes Mathematicae"},{"key":"S0022481200025019_ref007","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70843-7"},{"key":"S0022481200025019_ref014","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70849-8"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200025019","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,17]],"date-time":"2019-05-17T18:36:05Z","timestamp":1558118165000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200025019\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991,3]]},"references-count":19,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1991,3]]}},"alternative-id":["S0022481200025019"],"URL":"https:\/\/doi.org\/10.2307\/2274915","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1991,3]]}}}