{"entities":{"Q5945010":{"pageid":8121812,"ns":120,"title":"Item:Q5945010","lastrevid":47680855,"modified":"2026-01-02T10:16:01Z","type":"item","id":"Q5945010","labels":{"en":{"language":"en","value":"The strength of Martin-L\u00f6f type theory with a superuniverse. II"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1655896"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5945010$08B9B286-F648-4D4C-AF9B-ACB7D02DE29A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"94e0937940a47d5ea1cf1f8a63cea60777fc6b16","datavalue":{"value":{"text":"The strength of Martin-L\u00f6f type theory with a superuniverse. II","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5945010$AA1507D0-06E6-4A8A-872C-3772BD3B69EA","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"3b23bd7f211cff1dc763cbce5ff4007ad9acb0ad","datavalue":{"value":"0990.03048","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5945010$44AB960D-49F2-4E52-8702-8D2506E1B2EF","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e64bf31f7adc7949599b7092674140bc267c6785","datavalue":{"value":{"entity-type":"item","numeric-id":206562,"id":"Q206562"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5945010$71B50DBE-0220-4F5D-BB17-19A5CB4B4713","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"a0a7cd28a9f85b9c6ad57bd5bb1ae477bfe37846","datavalue":{"value":{"entity-type":"item","numeric-id":114337,"id":"Q114337"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5945010$DD46151F-5A43-46AE-A2AC-93DCF66F51D2","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"de0bbc1f0efc0eda52d8a37720ec217ae66c93cd","datavalue":{"value":{"time":"+2002-03-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5945010$A2D48E01-48C1-42E9-B514-7F5CCF953D0D","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"8827ab7199b491020ea675e2bec3522c6a5f593a","datavalue":{"value":"In Part I [ibid. 39, No. 1, 1-39 (2000; Zbl 0953.03065)] a realisability interpretation of \\textbf{MLS}, i.e., type theory with a superuniverse, was given in a classical theory \\({\\mathbf T}^S\\). It was shown that the proof-theoretic ordinal of \\textbf{MLS} is at least \\(\\Phi_{\\Gamma_0}(0)\\), where \\(\\Phi_{\\alpha}(\\beta)\\) is similar to the Veblen hierachy but starts with \\(\\Phi_0(\\xi) = \\Gamma_{\\xi}\\), where \\(\\Gamma_{\\alpha}\\) is the \\(\\alpha\\)th ordinal \\(\\rho>0\\) such that \\(\\phi_{\\delta}(\\xi)<\\rho\\) for all \\(\\xi,\\delta<\\rho\\). In this part, it is proved that the proof-theoretic ordinal of \\({\\mathbf T}^S\\) is at most \\(\\Phi_{\\Gamma_0}(0)\\), thus establishing that \\textbf{MLS} and \\({\\mathbf T}^S\\) have the same strength and that \\(\\Phi_{\\Gamma_0}(0)\\) is their proof-theoretic ordinal. This analysis is obtained using a suitable infinitary proof system. Thus \\textbf{MLS} and \\({\\mathbf T}^S\\) provide examples of theories of strength strictly between the Feferman-Sch\u00fctte ordinal \\(\\Gamma_0\\) and the Bachmann-Howard ordinal.","type":"string"},"datatype":"string"},"type":"statement","id":"Q5945010$5A24565D-333C-4904-A228-85756071FB46","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"256f7e8a78354c9241b063a26583c1bfdf31ddc2","datavalue":{"value":{"entity-type":"item","numeric-id":375196,"id":"Q375196"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5945010$8D2BC73C-5D6F-43BB-9587-6D2A8E1725EF","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"8612eb3fa5372f4e40168b827ed17a01cee8d8f6","datavalue":{"value":"03F50","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5945010$BAE67746-BF42-4FA9-9640-D3E57EB07BB6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"4cb4544bfd0397cd4a315ee326499c372f013de5","datavalue":{"value":"03F35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5945010$3736A07B-6E61-4A97-8423-9FC702E95655","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"23ceee6d3c7c93830578b552513a944677a835cb","datavalue":{"value":"03F15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5945010$EC660272-A726-47E7-8848-04F59CAFF504","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"2b0919c48a255b26fcf065230a9a621cd8c579a3","datavalue":{"value":"03E70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5945010$DE5CCA33-235F-4A38-AA30-7805B22990BD","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"062bea499899228b840291a0059a5ffcb39c7bb8","datavalue":{"value":"1655896","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5945010$13774F15-B9EB-4084-92B4-A5D9148D89A9","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5ea0e35eece84bed33461e424b92d07e45bd0c24","datavalue":{"value":"type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q5945010$67B19272-D4E8-4DCA-87EB-F9BF689A6B44","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"664c217a1a00d62effaec670f5656be452525922","datavalue":{"value":"ordinal analysis","type":"string"},"datatype":"string"},"type":"statement","id":"Q5945010$95C848B3-CF91-45E0-91B0-C659632701D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3f62e8e1c4d7b443eda51b480fa2916beeb866d7","datavalue":{"value":"Kripke-Platek set theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q5945010$A5061BFF-9330-422E-A353-CF5DD7156915","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0d6a889ce77d08e7620d168eac1e4806dfb1819b","datavalue":{"value":"predicative systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q5945010$BF9791AC-4200-489E-AF14-F44C0D1F43B2","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5945010$1CD39D53-5490-461B-9831-1D22A858D1EF","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"71fc18fcb098c8b58e8ee66652ee6c200590e2f2","datavalue":{"value":"https://doi.org/10.1007/s001530000051","type":"string"},"datatype":"url"},"type":"statement","id":"Q5945010$9B7F9F6E-C5FA-4830-98C9-BE7A586AD9CE","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"e71c860adc83c191b9cfa643e07ed94bc9e9a5c0","datavalue":{"value":"W1970430231","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5945010$A5ED41A5-03AF-4708-B577-E2D7E2FB2191","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"11959795e939b63d3c88be8f20cc5167776417ad","datavalue":{"value":"10.1007/S001530000051","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5945010$A21229A6-2B83-42F3-94B7-AB5800E1724A","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2bb277504941c4a8f757fa4055d9a94b5bd7e3f0","datavalue":{"value":{"entity-type":"item","numeric-id":1976875,"id":"Q1976875"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c9fe0bce2dfc22dada174b5384a2fec3d849d97f","datavalue":{"value":{"amount":"+0.8953668475151062","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5945010$9167793A-4008-48FA-898E-E83FD36DB9C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9f909d797baa23e564b49ac086cd4abee13b9158","datavalue":{"value":{"entity-type":"item","numeric-id":4247313,"id":"Q4247313"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c9fe0bce2dfc22dada174b5384a2fec3d849d97f","datavalue":{"value":{"amount":"+0.8953668475151062","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5945010$8A9EB262-9FAA-49D4-B712-FBD2D6132042","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"26c0867e245a452e44f078e1a0c502914012c5dc","datavalue":{"value":{"entity-type":"item","numeric-id":1295372,"id":"Q1295372"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8b3b4a83c97a8f64fbcec85bdc9415190f9dd6fc","datavalue":{"value":{"amount":"+0.8493854403495789","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5945010$B29069E7-DF7C-4726-BD1B-BC0594C2B3EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2c995985ab517bc18c9b297f34f20ce89e9265e4","datavalue":{"value":{"entity-type":"item","numeric-id":5457304,"id":"Q5457304"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8b3b4a83c97a8f64fbcec85bdc9415190f9dd6fc","datavalue":{"value":{"amount":"+0.8493854403495789","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5945010$E141F04A-6BDB-411B-8F7D-F93568FDE375","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c9c700c00cfaf31e5a7d9e0e561fb4b9541cb82b","datavalue":{"value":{"entity-type":"item","numeric-id":4715478,"id":"Q4715478"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b166cf176636fb50f227d4735ffe3b370e38c2e0","datavalue":{"value":{"amount":"+0.8138092756271362","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5945010$48EEA7A8-CB89-4444-A527-719906FDEB3F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5945010","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5945010"}}}}}