{"entities":{"Q1344548":{"pageid":1355287,"ns":120,"title":"Item:Q1344548","lastrevid":67662807,"modified":"2026-04-12T19:12:58Z","type":"item","id":"Q1344548","labels":{"en":{"language":"en","value":"The strength of some Martin-L\u00f6f type theories"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 722179"}},"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":"Q1344548$920D12AA-58FE-4030-B1A0-ECB9DAE4CE11","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a12979f495c02faa065243d1a00a79185f38e692","datavalue":{"value":{"text":"The strength of some Martin-L\u00f6f type theories","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1344548$A7594CAC-4408-4134-9BFD-1F8EA298AB4C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"9c27a966bd1b75ecd03e8242eea15b09e785da72","datavalue":{"value":"0819.03047","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1344548$C8EDF790-8A2C-4429-A548-AB2F9338B245","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"a3fa513733744beb8bdb9fa8b4657dc40f821af9","datavalue":{"value":"10.1007/BF01278464","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1344548$A2072800-F7BE-4B69-9603-679E1A8219DF","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"9fe3c77477a57e28f661a034dc3966dc0afa9a91","datavalue":{"value":{"entity-type":"item","numeric-id":1295395,"id":"Q1295395"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1344548$774E3411-1317-456B-9326-663E5B722CAA","rank":"normal"},{"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":"Q1344548$F729E98E-6ECD-48B2-A860-EB455EBF9FDD","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":"Q1344548$E2FFCD7A-5323-4263-9B7F-D9236FAFC6A0","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"130e39adf7d31aeb394dfacb8a12a0f0ed2af467","datavalue":{"value":{"time":"+1995-08-27T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1344548$50A6A729-BDD3-421D-A59F-035DD1F244B4","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"793405b4667e58b060e3e408dbc9cfa204322054","datavalue":{"value":"The main result of this paper shows that the classical second-order arithmetic of \\(\\Delta^ 1_ 2- \\text{CA}+ \\text{BI}\\) (bar induction) is reducible to \\(\\text{ML}_ 1 \\text{W}\\), Martin-L\u00f6f's type theory with one universe and the type of well-founded trees. The method used is, in the authors' parlance, a ``soft'' proof theory, like the interpretation of one theory into another, and no (hard) ordinal analysis is employed. The paper has the character of a survey, and many constructive theories are discussed, compared, and interpreted, on the way to achieving the above result. They include KP (Kripke-Platek set theory), CZF (constructive ZF of Aczel), \\(\\text{T}_ 0\\) (of Feferman), and IARI (intuitionistic second order arithmetic). KP, CZF, \\(\\text{ML}_ 1 \\text{V}\\) (here, V is Aczel's set of iterative sets) and ten or so other theories are shown to be mutually interpretable. A second group contains \\(\\text{T}_ 0\\), \\(\\Delta^ 1_ 2- \\text{CA}+ \\text{BI}\\), KPi (i for inaccessible ordinal) and \\(\\text{ML}_{1 \\text{W}} \\text{V}\\) (the subscript W indicates W-formation for small types). In the `Conclusions', the authors announce that they will consider intuitionistic transfinite types in the future.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1344548$095ADDB8-816F-4D0C-BBA6-ED2F7DAD8820","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"4cb4544bfd0397cd4a315ee326499c372f013de5","datavalue":{"value":"03F35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1344548$64E3DA30-4772-4D1F-87B4-E08A05CAAF39","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"8612eb3fa5372f4e40168b827ed17a01cee8d8f6","datavalue":{"value":"03F50","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1344548$D36CBB1D-7A40-4771-A825-4AAD016D8778","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"5782d4e69f02bf487f73e99e1c88e88fdc85f730","datavalue":{"value":"722179","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1344548$F5B7C0DB-3D9B-4474-BF0C-D54DB512C4F5","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5893888217fbc85bee928df15c2ccb99d477e846","datavalue":{"value":"constructive systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q1344548$C210C2DF-5A40-44BA-B207-8E37F186F6A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3f62e8e1c4d7b443eda51b480fa2916beeb866d7","datavalue":{"value":"Kripke-Platek set theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q1344548$F7078A4F-B871-4CCA-856E-B6B2EC8E490B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b61d24ae28fe71c44dd77856a1991f4fb054cfae","datavalue":{"value":"constructive ZF","type":"string"},"datatype":"string"},"type":"statement","id":"Q1344548$AC16E7A9-F0FA-45B3-8A74-3D6F0D393C16","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bded246a734ce499b119400eda073f30a31cc63f","datavalue":{"value":"intuitionistic second order arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1344548$58A1F9B8-5152-491F-9AF7-AD8634D55277","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9a21aa51170f0ff89b295995a6751a8a56aa14c1","datavalue":{"value":"classical second-order arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1344548$A1D587A2-5147-4A2A-9FB7-CD8B41E3C478","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"33775f26030d071074f6e677c78b2fdd4159a0c9","datavalue":{"value":"Martin-L\u00f6f's type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q1344548$71F7E4ED-68F7-490D-9F74-EC9C685AEAB9","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":"Q1344548$F803121E-B5B3-439F-8F94-9D08C9E1B0D5","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"67e43cd194146fff0fb8e4b0aacca2f4f32e42e3","datavalue":{"value":{"entity-type":"item","numeric-id":3937387,"id":"Q3937387"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1344548$769A4ACE-9806-458F-BAF9-87A13C819B3C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9779d2f20504dba38f482f942c0abc04f8e04e14","datavalue":{"value":{"entity-type":"item","numeric-id":3310616,"id":"Q3310616"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1344548$35C69C15-68BB-41BB-8B7D-6209BF436764","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e21df1d3055daa4725f01a29fad1e4853704fa4c","datavalue":{"value":{"entity-type":"item","numeric-id":3762311,"id":"Q3762311"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1344548$F24B5FA9-0C64-4FF5-844F-B26D8E67D319","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8973abb951181b5865d7e8e53e525f0e4b9b6f41","datavalue":{"value":{"entity-type":"item","numeric-id":4075450,"id":"Q4075450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1344548$5ABE5064-8B64-4831-8D68-60DA6F417CB7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4d8f68f9e78bb6a5d59f21b1f2cddad1744eb2f2","datavalue":{"value":{"entity-type":"item","numeric-id":3659782,"id":"Q3659782"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1344548$9B24DAC8-FABE-434F-B1D0-C0FA9735B11E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1b2e1ab8d6c4a6ea4362f203e5137d4541ef80eb","datavalue":{"value":{"entity-type":"item","numeric-id":3679172,"id":"Q3679172"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1344548$4A3319C0-A12F-4296-B47A-06D3C334E1AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b822b85db8677253a219ea1a385eddacb5927738","datavalue":{"value":{"entity-type":"item","numeric-id":1166517,"id":"Q1166517"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1344548$62082352-09A0-4417-AB53-BDA9A17488A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"51fdc6e6c91c016e9985f506925ea38ed52ac667","datavalue":{"value":{"entity-type":"item","numeric-id":4128540,"id":"Q4128540"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1344548$189DACDE-266A-4E73-804E-19E4BC782F75","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5a105535a0b4cf840366405592d4900ef990604f","datavalue":{"value":{"entity-type":"item","numeric-id":3882452,"id":"Q3882452"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1344548$85834B7A-E18C-40D5-92A8-DFBDEB867EBA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7ddcae75623ad27e45f301cf7aa223ba87bd8584","datavalue":{"value":{"entity-type":"item","numeric-id":3968911,"id":"Q3968911"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1344548$24948020-DDD2-40C9-91E3-FB559897B1F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"397e4e2ee65292a376a8df287bc918d9ec760e88","datavalue":{"value":{"entity-type":"item","numeric-id":4749835,"id":"Q4749835"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1344548$A401EE15-F50B-4EFF-A5CC-F92343379ED8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"499a95bca207fbf8c7061b1c293c572cca9800de","datavalue":{"value":{"entity-type":"item","numeric-id":3041187,"id":"Q3041187"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1344548$AA2EBBA0-5878-43A5-8DB3-3D315D3E1506","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"47b0ec3118c55b6f3ab232f29debefc8c9d383a9","datavalue":{"value":{"entity-type":"item","numeric-id":3688389,"id":"Q3688389"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1344548$54E2EFA1-D049-4E9E-B3D3-F8C9EADEDB55","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"74605135c388db78d4d0ca86dc0cd54881585bea","datavalue":{"value":{"entity-type":"item","numeric-id":4073362,"id":"Q4073362"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1344548$84ED3D32-64FE-40F1-BF78-7A99A6854AA9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3ab5d7b35f67f940445411fa45c1b02bcb40d39f","datavalue":{"value":{"entity-type":"item","numeric-id":3999860,"id":"Q3999860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1344548$3B0ACA01-E538-440C-8931-A70571EA3E7C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5d583a014f94ffbe5c2d58985db23d4061ed52f5","datavalue":{"value":{"entity-type":"item","numeric-id":688845,"id":"Q688845"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1344548$19FE0766-C866-43EA-933F-DE3189037353","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4ec6af83f9a6c90ef054757ef63aea9bbf0884e2","datavalue":{"value":{"entity-type":"item","numeric-id":803124,"id":"Q803124"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1344548$76BD962A-5B91-4A62-A18F-DCCBA889ED38","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7f26adabcc39dd027a7ac9b73459f012db8e58f7","datavalue":{"value":{"entity-type":"item","numeric-id":4715478,"id":"Q4715478"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1344548$587141D0-98F7-4FDB-9534-5F16FE77D69E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"25fc0f83d5ec3109942a6da644b57709f31b1dc6","datavalue":{"value":{"entity-type":"item","numeric-id":1188522,"id":"Q1188522"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1344548$32DBD193-8DA0-4701-84F7-D71AD6B636DA","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9b1e3fef7a91f717d982de5af60bbc76f7514a80","datavalue":{"value":{"entity-type":"item","numeric-id":4944846,"id":"Q4944846"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1538aa0370f76b0a9ed3b9644a6f5bdf276c7c0d","datavalue":{"value":{"amount":"+0.8236945867538452","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":"Q1344548$4396D10D-C433-4E0A-AC76-9C31C8F17768","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":"1538aa0370f76b0a9ed3b9644a6f5bdf276c7c0d","datavalue":{"value":{"amount":"+0.8236945867538452","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":"Q1344548$438DF39F-50E7-421F-9D21-50DA4E257D56","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":"0d41da4545268ea4f75fb9fa4835e6c2c0550c22","datavalue":{"value":{"amount":"+0.8074709177017212","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":"Q1344548$4C590E19-DA10-4156-8FD3-0FD0941B8E5D","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":"0d41da4545268ea4f75fb9fa4835e6c2c0550c22","datavalue":{"value":{"amount":"+0.8074709177017212","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":"Q1344548$7CE3F09A-F31D-4807-A948-7885A2958726","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c6e3531ca5baa0e71d970e1f7742f2d4f1bea84d","datavalue":{"value":{"entity-type":"item","numeric-id":2500469,"id":"Q2500469"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4c9864c1ad190c19ec157901548f292282e884f4","datavalue":{"value":{"amount":"+0.7909785509109497","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":"Q1344548$1EF9F855-6492-46A6-9D4D-19291201F3B3","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"The strength of some Martin-L\u00f6f type theories","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/The_strength_of_some_Martin-L%C3%B6f_type_theories"}}}}}