{"entities":{"Q1568707":{"pageid":1579447,"ns":120,"title":"Item:Q1568707","lastrevid":43218450,"modified":"2025-07-22T11:59:08Z","type":"item","id":"Q1568707","labels":{"en":{"language":"en","value":"Extending Martin-L\u00f6f type theory by one Mahlo-universe"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1463218"}},"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":"Q1568707$2D72D6A1-A87D-44B1-9B46-EAD98F6A4175","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"cac0d0347ba0e356bc6376bdaae317dcca4bb207","datavalue":{"value":{"text":"Extending Martin-L\u00f6f type theory by one Mahlo-universe","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1568707$48D4431E-0779-4B89-84BF-094B9DEF2CEF","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"742e039bf825a2c02c94a221275394ab18e93b47","datavalue":{"value":"0943.03046","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1568707$B6373018-8AED-4555-8FBD-9DA9458C36D3","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"726d6d17ffd7097481aaa7acac69959461b65139","datavalue":{"value":{"entity-type":"item","numeric-id":587965,"id":"Q587965"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1568707$9BDCA030-5811-4C28-B398-DBD77D67C7E9","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":"Q1568707$F455DD9C-83CB-4F97-B48F-7B9CBEA2B691","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"19945cc67174d34ebbeae4b89d0f3c36236e8191","datavalue":{"value":{"time":"+2000-09-05T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1568707$72253A5A-9516-4532-9258-2E9B0E5417C7","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"fca0d4a7258c86441a26a0044e15a69bc779e407","datavalue":{"value":"We define a type theory \\(\\mathbb{M}\\mathbb{L}\\mathbb{M}\\), which has proof-theoretical strength slightly greater than Rathjen's theory \\(\\mathbb{K}\\mathbb{P}\\mathbb{M}\\). This is achieved by replacing the ordinary universe in Martin-L\u00f6f's type theory by a new universe \\(\\mathbb{V}\\). \\(\\mathbb{V}\\) has the property that for every function \\(f\\), mapping families of sets in \\(\\mathbb{V}\\) to families of sets in \\(\\mathbb{V} \\), there exists a subuniverse of \\(\\mathbb{V}\\) closed under \\(f\\) and represented in \\(\\mathbb{V}\\). We show that the proof-theoretical strength of \\(\\mathbb{M}\\mathbb{L} \\mathbb{M}\\) is \\(\\geq\\psi_{\\Omega_1} \\Omega_{\\mathbb{M} +\\omega}\\). Therefore we reach a strength slightly greater than that of \\(\\mathbb{K}\\mathbb{P}\\mathbb{M}\\) and \\(\\mathbb{V}\\) can be considered as the type-theoretic equivalent of a recursively Mahlo ordinal. Together with the author's ``A model for a type theory with Mahlo universe'' [Draft. Available via \\url{http://www.math.uu.se/~setzer/articles/uppermahlo.dvi.gz}], in which \\(\\mathbb{M} \\mathbb{L} \\mathbb{M}\\) is modelled in a suitable extension of \\(\\mathbb{K}\\mathbb{P}\\mathbb{M}\\), it follows \\(|\\mathbb{M} \\mathbb{L} \\mathbb{M}|= \\psi_{\\Omega_1}(\\Omega_{\\mathbb{M}+\\omega})\\).","type":"string"},"datatype":"string"},"type":"statement","id":"Q1568707$4EFA9A25-CC3D-4319-AD7D-0BF3D9B5EE80","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"df6d145faee35a3a1d4d9e701f68880611a87159","datavalue":{"value":{"entity-type":"item","numeric-id":587965,"id":"Q587965"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1568707$6C5B389A-5825-4605-808B-4B69B020C685","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"4cb4544bfd0397cd4a315ee326499c372f013de5","datavalue":{"value":"03F35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1568707$4DC25D53-D03A-47BE-80D0-E4C119D663A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"23ceee6d3c7c93830578b552513a944677a835cb","datavalue":{"value":"03F15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1568707$7FFCCDCB-DAC0-4431-BEF0-EF893311D2E4","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"0a51d7c77f86e2e480d02901944a9ff5bf3945d8","datavalue":{"value":"1463218","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1568707$8ACF5ACA-58F4-4705-B8FC-D4C5753C1A14","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d6c658f92cfca10399e0b9df9aa408c3bc22cae6","datavalue":{"value":"constructive type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q1568707$C3B35D72-F6ED-4434-B133-291B10E02EE4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"33775f26030d071074f6e677c78b2fdd4159a0c9","datavalue":{"value":"Martin-L\u00f6f's type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q1568707$BBBE9137-4302-4EBF-8A4C-31AC10CBCA5E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"837fc5bf62023271ee428d3915134847c33c3eee","datavalue":{"value":"proof-theoretical strength","type":"string"},"datatype":"string"},"type":"statement","id":"Q1568707$0AB1CDF4-5EFD-4517-9C2E-4F8CB440F4AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"37f7e25387335fe4376618e87e388fa1254d9a0f","datavalue":{"value":"Mahlo ordinal","type":"string"},"datatype":"string"},"type":"statement","id":"Q1568707$0839EC5C-7BB9-48F6-B46A-DFFB23792470","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":"Q1568707$BD9DDC9E-1844-452D-A310-402BD5BB6DBA","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"4380deca1cc6be952789cbda6f8c1e0cdc0e1c05","datavalue":{"value":"https://doi.org/10.1007/s001530050140","type":"string"},"datatype":"url"},"type":"statement","id":"Q1568707$AF785141-5E2A-4701-BB32-5FC4F753B7A4","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"895f1223e8e9b59e22687deb17863c97ab3391e4","datavalue":{"value":"W1968916436","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1568707$FEB53F9C-7912-409A-BA72-E3A455A98303","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"aaf8becd6706280b8e777c8df554fdd8eaef5134","datavalue":{"value":"10.1007/S001530050140","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1568707$AF105C6E-CDFA-46FE-92BE-29DB8AC3B50F","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d8936e2a9e79821aa70feaac1c48a084c0b32335","datavalue":{"value":{"entity-type":"item","numeric-id":3985097,"id":"Q3985097"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"19bda239a13ace2112cecbe9a8323fb210a67525","datavalue":{"value":{"amount":"+0.9116018","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1568707$B6946B09-B9E2-469B-B03B-26BB7E8C4850","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":"76f4c9dfc348546dcbe5641666df6350318b9988","datavalue":{"value":{"amount":"+0.90784603","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1568707$27B29040-7DF3-4B8D-B7BB-40654D339123","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f74c98b5a48e2ad52f2ae1ef2655d9c93c15c5d6","datavalue":{"value":{"entity-type":"item","numeric-id":3322097,"id":"Q3322097"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fec4aca14b3769dbad9f79a712df27355cf51d5f","datavalue":{"value":{"amount":"+0.9021401","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1568707$32FAAFCA-605E-45B1-96DD-AE3D894DFB7F","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":"9cbedc129b05efa9e26389d6af77fcc7a04c0029","datavalue":{"value":{"amount":"+0.9013692","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1568707$48402ABF-B90E-4EF2-ACA5-3F255C0BC23D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b6606d81851a96e083ccf35fd04b37d925d4e60d","datavalue":{"value":{"entity-type":"item","numeric-id":5249247,"id":"Q5249247"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f77a16cacddd4dc85aa2adc6a5e96320cfcc1e4f","datavalue":{"value":{"amount":"+0.9010041","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1568707$1F23EB44-4197-4204-812F-61D820146772","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fc8b48c0acf1d2fd8aee1bcd2f9bf9ae25646286","datavalue":{"value":{"entity-type":"item","numeric-id":5945010,"id":"Q5945010"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c1c3556211526a520fc4a2fb379c7f0fea98f825","datavalue":{"value":{"amount":"+0.90084755","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1568707$1C663010-7C67-4D7D-888E-A6759D3EA478","rank":"normal"},{"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":"3304ce2478f7ec522a0338b29ee6ef36696ff219","datavalue":{"value":{"amount":"+0.8990092","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1568707$63E011CF-D4E3-4B29-903C-3612AEFC2C58","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"da92cb1e0349daf8a78255d0a62e3cc78faa2ea4","datavalue":{"value":{"entity-type":"item","numeric-id":1407579,"id":"Q1407579"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6344e3332c617c048b80b79ede29185088aa71b6","datavalue":{"value":{"amount":"+0.8987471","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1568707$B8F766D5-4D87-4F3E-AF0C-BB6D9228AF5B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e9d57541ec12dfef8cf0cf1a109b1ae5813ffcbc","datavalue":{"value":{"entity-type":"item","numeric-id":5013908,"id":"Q5013908"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"daaadd626aef7c0c9d5700bcb8c2fe88804cd574","datavalue":{"value":{"amount":"+0.89789575","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1568707$6BC7BD66-B89F-42D2-8802-48E6B886A131","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"953159312b7424abe16acfaed309cd34802f4340","datavalue":{"value":{"entity-type":"item","numeric-id":5262927,"id":"Q5262927"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"390a3c2dbf1f66c7663504da181a5bdb3fe7522a","datavalue":{"value":{"amount":"+0.8958082","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1568707$7B1ED735-A6C5-464F-B23F-7C49F52D7735","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1568707","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1568707"}}}}}