caa a22 4500 469126922 CHVBK 20180323133153.0 cr unu---uuuuu 170328e19920301xx s 000 0 eng 10.1007/BF01269951 doi (NATIONALLICENCE)springer-10.1007/BF01269951 Palmgren Erik Department of Mathematics, Uppsala University, P.O. Box 480, S-75106, Uppsala, Sweden aut Type-theoretic interpretation of iterated, strictly positive inductive definitions [Elektronische Daten] [Erik Palmgren] Summary: We interpret intuitionistic theories of (iterated) strictly positive inductive definitions (s.p.-ID i′ s) into Martin-Löf's type theory. The main purpose being to obtain lower bounds of the proof-theoretic strength of type theories furnished with means for transfinite induction (W-type, Aczel's set of iterative sets or recursion on (type) universes). Thes.p.-ID i′ s are essentially the wellknownID i -theories, studied in ordinal analysis of fragments of second order arithmetic, but the set variable in the operator form is restricted to occur only strictly positively. The modelling is done by constructivizing continuity notions for set operators at higher number classes and proving that strictly positive set operators are continuous in this sense. The existence of least fixed points, or more accurately, least sets closed under the operator, then easily follows. Springer-Verlag, 1992 Archive for Mathematical Logic Springer-Verlag 32/2(1992-03-01), 75-99 0933-5846 32:2<75 1992 32 153 https://doi.org/10.1007/BF01269951 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1007/BF01269951 text/html Onlinezugriff via DOI NATIONALLICENCE 100 1- Palmgren Erik Department of Mathematics, Uppsala University, P.O. Box 480, S-75106, Uppsala, Sweden aut NATIONALLICENCE 773 0- Archive for Mathematical Logic Springer-Verlag 32/2(1992-03-01), 75-99 0933-5846 32:2<75 1992 32 153 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer