{"entities":{"Q1295372":{"pageid":1306122,"ns":120,"title":"Item:Q1295372","lastrevid":70613802,"modified":"2026-04-13T15:45:11Z","type":"item","id":"Q1295372","labels":{"en":{"language":"en","value":"Well-ordering proofs for Martin-L\u00f6f type theory"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1308059"}},"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":"Q1295372$632F731C-5519-469C-A68B-17E8F7A3DB61","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c6581dd1d173e5874d8c7aa9ee7684b954534172","datavalue":{"value":{"text":"Well-ordering proofs for Martin-L\u00f6f type theory","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1295372$8CCF3BAA-65C7-43CC-A368-78255C50DFFA","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"812be382797314bba6e0d09db739db6f3523339e","datavalue":{"value":"0928.03067","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1295372$59585758-5835-4847-9C28-E470E78E6FAF","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"b3aa0fca4622059854a92d7ff33c40e1ec042893","datavalue":{"value":"10.1016/S0168-0072(97)00078-X","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1295372$25469B82-5093-4F0F-8CCB-4D8791C71D4D","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":"Q1295372$5A10180B-1160-4817-B8BF-25EDD49E9D8A","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f91a4bcbc93435aed71775d25a4c5cd09e26f12d","datavalue":{"value":{"entity-type":"item","numeric-id":122505,"id":"Q122505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1295372$0ADFABD1-437C-47F1-A173-935113240BE5","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"bfc696b995d8319fe0260180a1cd6c4dc4a5d24c","datavalue":{"value":{"time":"+1999-08-16T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1295372$9B94BDBA-965E-4E98-B485-C57C0DA1A0A9","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"b6fffee78da4245e652337d7c23cf223cb77dcf8","datavalue":{"value":"In his Ph.D. thesis [Proof theoretical strength of Martin-L\u00f6f type theory with \\(W\\)-type and one universe, Diss., Univ. M\u00fcnchen (1993; Zbl 0863.03029)], the author proved an upper bound \\(\\alpha= \\psi_{\\Omega_1} \\Omega_{I+\\omega}\\) for the proof-theoretic ordinal of Martin-L\u00f6f's intuitionistic type theory with \\(W\\)-type and one universe. In the present paper he proves in this system transfinite induction up to every ordinal less than \\(\\alpha\\). This determines the proof-theoretic strength of the theory and shows that it is slightly stronger than Feferman's theory \\(T_0\\) and \\((\\Delta^1_2- \\text{CA})+ (\\text{BI})\\). The author points out that the proof extends to show that the strength of Martin-L\u00f6f's type theory with \\(n\\) universes is \\(\\psi_{\\Omega_1} \\Omega_{I_n+ \\omega}\\) where \\(I_n\\) is the \\(n\\)th inaccessible, and this implies that the strength of the theory with arbitrary finitely iterated universes is \\(\\psi_{\\Omega_1} I_\\omega\\) where \\(I_\\omega= \\sup\\{I_n\\mid n\\in\\omega\\}\\).","type":"string"},"datatype":"string"},"type":"statement","id":"Q1295372$60E4D660-EE38-43AD-84B3-E3311B5A79C9","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"8612eb3fa5372f4e40168b827ed17a01cee8d8f6","datavalue":{"value":"03F50","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1295372$79372B7B-7605-4195-8C07-F4623552D728","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"4cb4544bfd0397cd4a315ee326499c372f013de5","datavalue":{"value":"03F35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1295372$9FDF9685-B692-4443-A327-B65E72A10F3B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"23ceee6d3c7c93830578b552513a944677a835cb","datavalue":{"value":"03F15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1295372$E763F7BF-1FF5-4036-9ECA-37155A92A910","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"8a938b610a40bd640b3fec30e702b010e242876c","datavalue":{"value":"1308059","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1295372$46DF4651-6FF0-4629-BE92-910A427B9839","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e93a1bc476bf1b0792416e3dee5ed7406bec2ad8","datavalue":{"value":"Martin-L\u00f6f's intuitionistic type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q1295372$352BCD55-8E36-4961-9D21-E9CF7492DFF1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b8cc87407ab9572d85505f2cace7811c9ecc29db","datavalue":{"value":"transfinite induction","type":"string"},"datatype":"string"},"type":"statement","id":"Q1295372$CA7F8DF8-DD2D-4E19-89E1-A803456D2496","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7c9d42b2a8e8f10bc0defb7ff4991bcf0f90417e","datavalue":{"value":"proof-theoretic strength","type":"string"},"datatype":"string"},"type":"statement","id":"Q1295372$A5B5C6A6-3787-4414-B524-2C330CDB2D09","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4d6c911c4b5bb4c706b0759ca781c9c90f902bb0","datavalue":{"value":"finitely iterated universes","type":"string"},"datatype":"string"},"type":"statement","id":"Q1295372$7082D2E6-6EE1-4EC9-BE62-364E3488823B","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"8f432bccb81d11b6d0c5be5373ba82abf19c1967","datavalue":{"value":{"entity-type":"item","numeric-id":454365,"id":"Q454365"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1295372$AF8A460A-5AE4-4721-83B3-31BC157303A8","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":"Q1295372$DF0EA723-BB02-41FA-BF52-82171F6D08B8","rank":"normal"}],"P223":[{"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":"Q1295372$34207B65-522B-4D2E-8DC4-9D153285F121","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a02ebf0568f47635f182c488d881f7744ddea83e","datavalue":{"value":{"entity-type":"item","numeric-id":3803111,"id":"Q3803111"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1295372$5952A5D3-1AEC-47C8-9B55-8B00E7C80519","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":"Q1295372$2817EB39-6B1E-4611-BEDC-7DA4BB87E64F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d231028a06b9247fe4eceef543855a118cf2b5f1","datavalue":{"value":{"entity-type":"item","numeric-id":4109654,"id":"Q4109654"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1295372$94903FE7-F3DC-469B-8E19-2B965BB69979","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"559d023d291e446bba13d5979c34214548a51934","datavalue":{"value":{"entity-type":"item","numeric-id":1109029,"id":"Q1109029"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1295372$EE418D5A-0996-4BDA-BDBE-425FA7611B40","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f43c482b602f05488701d197a989abad413a86d3","datavalue":{"value":{"entity-type":"item","numeric-id":3138829,"id":"Q3138829"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1295372$7907F11F-2954-4045-A849-4F80E20FA8F2","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":"Q1295372$AD75A847-21B5-48FC-B6C0-348518D1ED49","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3d94759bbc52803d92b95b89ff212691baddbc00","datavalue":{"value":{"entity-type":"item","numeric-id":4106173,"id":"Q4106173"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1295372$E19DFE35-5606-4447-B3F1-964424889348","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f4a41e51759b03d93fbc94ef3ba8acf0dd412666","datavalue":{"value":{"entity-type":"item","numeric-id":4040375,"id":"Q4040375"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1295372$EF94060F-00D1-4416-BCAD-1B69F7ACE2FC","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":"Q1295372$EF23EC17-92C8-4354-BCB4-E597FF93C46C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1c97a7b6faf562e1c5b09260906a1f00f35a77b0","datavalue":{"value":{"entity-type":"item","numeric-id":3773876,"id":"Q3773876"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1295372$08913152-B440-4FA7-B640-134D32A3E1D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"772f22db8726abc1b17c66467dc58d8102a542e4","datavalue":{"value":{"entity-type":"item","numeric-id":1344548,"id":"Q1344548"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1295372$EE6D63EB-1834-4E2C-8381-FD65E45E45DA","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":"Q1295372$986E6B5D-1AF7-4405-8219-5CC2F77CD5CD","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":"Q1295372$A615ED0E-C913-49A5-9FAE-B8CB16A58536","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ae94f828af67e50fecbc9e4b645ed6964977b9db","datavalue":{"value":{"entity-type":"item","numeric-id":4099613,"id":"Q4099613"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1295372$304968AE-0F20-47A8-B7DA-8E608C93E010","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"86f69e4e3c6e6db6273645f322c23116e1ad1c80","datavalue":{"value":{"entity-type":"item","numeric-id":3343983,"id":"Q3343983"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1295372$7D3617B0-0AB9-4308-8DE8-51C251EAFEAA","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":"Q1295372$200F4738-EABD-4DA9-ADAC-F8DF1A45343D","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":"Q1295372$B2BFB3EA-0F91-4766-9884-2F2A9019EE65","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":"Q1295372$F3DC6CB6-1B8F-4E0F-8CEE-E82E75D8C4BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6956a12199d710944333687ed9f973870967e27d","datavalue":{"value":{"entity-type":"item","numeric-id":916656,"id":"Q916656"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1295372$46F80785-82AB-43CE-BE01-96976FB21A23","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b24b5b561cde7a5eef6f6e87df461bfda495bb00","datavalue":{"value":{"entity-type":"item","numeric-id":3773877,"id":"Q3773877"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1295372$70D6A858-ACF4-4C58-A83C-BE99598365EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a019f48c952acfae395126bfe7d30ae0e9f39f91","datavalue":{"value":{"entity-type":"item","numeric-id":4304798,"id":"Q4304798"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1295372$4E128EAC-F43F-44C7-AEA5-DAFF355F4448","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b7c3e6815cd921fc7767de9db6783bde242a686c","datavalue":{"value":{"entity-type":"item","numeric-id":4143279,"id":"Q4143279"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1295372$923BF528-7053-4C94-BED5-6481138AC4EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6a24170d46521c68959354fc7defb44afe4797f5","datavalue":{"value":{"entity-type":"item","numeric-id":3800031,"id":"Q3800031"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1295372$81E5BC7D-642A-4BDA-8CE9-A31A7896CE9E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"67fac3d055d90ee3aafe3674088228fa265868c9","datavalue":{"value":{"entity-type":"item","numeric-id":3138828,"id":"Q3138828"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1295372$534489E4-AC07-4E4F-8E51-8CEF71094FD3","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":"Q1295372$ADF2A2EC-06C5-496B-A320-4884D6C4A8BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4ce3cca12d71cb4f11b87288184fa45ce0ffa6ba","datavalue":{"value":{"entity-type":"item","numeric-id":4364521,"id":"Q4364521"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1295372$8A432A19-946C-42D4-98D1-CA51656B0488","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b01f3c9efa192a49157794cc5646843be5e89451","datavalue":{"value":{"entity-type":"item","numeric-id":1086559,"id":"Q1086559"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1295372$FFDC0099-A23D-496B-A84D-C5FDCE60041D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"20f26a27356d39f30de150c562ffeee04fbf14f0","datavalue":{"value":{"entity-type":"item","numeric-id":1099173,"id":"Q1099173"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1295372$A33C7CCE-818F-465C-AFBB-98680252DAD9","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":"Q1295372$70782909-BF65-4545-8612-6BF172BF1E87","rank":"normal"}],"P1643":[{"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":"b6178f4dcaf2e7455254d331f27dfaba893147af","datavalue":{"value":{"amount":"+0.97440994","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":"Q1295372$07B9D7AD-2224-467A-AF64-E89B5FCD5B93","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"558451d5bf72b591e0effe1a25fb9587ce756dcb","datavalue":{"value":{"entity-type":"item","numeric-id":5438968,"id":"Q5438968"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ef2187faaf684fba2560a7b5670068e625454d16","datavalue":{"value":{"amount":"+0.9252803","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":"Q1295372$A536BB27-36AE-4FBD-9F00-3FE3D1AD2BE5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"10136e455743e3ade83a7e267fb95936edac7bd9","datavalue":{"value":{"entity-type":"item","numeric-id":1392287,"id":"Q1392287"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"54c65e2814db5226a0e5619ff3e979157d5d23c9","datavalue":{"value":{"amount":"+0.92417157","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":"Q1295372$BCE7FC4E-65CA-46DD-93A4-BD795705F537","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"071577697c11a2c9b8cea4d5bf370cc8ab8c50a2","datavalue":{"value":{"entity-type":"item","numeric-id":4236885,"id":"Q4236885"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9708a1bd785fc6c739d61c1348f5cce1cfe4135c","datavalue":{"value":{"amount":"+0.91996753","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":"Q1295372$C7C2A81B-4CBB-4057-B099-19BA8437C523","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"192339a8e85b2c1008bfe0c5389600bd3bd66642","datavalue":{"value":{"entity-type":"item","numeric-id":3612443,"id":"Q3612443"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"31225e4c09776df0801e8fa5bf5543ba1c7140c7","datavalue":{"value":{"amount":"+0.9121234","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":"Q1295372$A2182DDC-31A1-4063-81F7-F43E23EA5932","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1023319a3c923778a20db752caf09082c25636df","datavalue":{"value":{"entity-type":"item","numeric-id":688850,"id":"Q688850"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"13c13f9bd525804e86957e45963f39c2114e15f3","datavalue":{"value":{"amount":"+0.908052","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":"Q1295372$E638D60C-FD5D-4A6C-9269-57B055048513","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a86783be468d2adab8db2bcfe00a00cc438adddd","datavalue":{"value":{"entity-type":"item","numeric-id":813417,"id":"Q813417"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6a3dc6e03650bacd480639bb409f0f60bf6a8001","datavalue":{"value":{"amount":"+0.8999336","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":"Q1295372$99E031CC-86D1-4E1F-895F-D41D64E91E6C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bc640084c58d56128b6c439ca219936b0844bd22","datavalue":{"value":{"entity-type":"item","numeric-id":3613313,"id":"Q3613313"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4f9d6af7e38105932bb870776dfbb275696cd3b1","datavalue":{"value":{"amount":"+0.89993346","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":"Q1295372$81E039EB-2262-401A-9EF0-7C3A456EB272","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"259b5fd7a0f989fc0d40f257fa5f1477fdb4f3f7","datavalue":{"value":{"entity-type":"item","numeric-id":5055281,"id":"Q5055281"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f8785934fb175f3faa39555f491d09cbc7b2d911","datavalue":{"value":{"amount":"+0.89956194","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":"Q1295372$28584579-2D91-4278-B762-71BCC0E7CBFE","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":"d93683f821bb7c4126343802be211473ed66e652","datavalue":{"value":{"amount":"+0.89695585","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":"Q1295372$904E5693-480A-4020-9D3E-DB30DB4A146A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Well-ordering proofs for Martin-L\u00f6f type theory","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Well-ordering_proofs_for_Martin-L%C3%B6f_type_theory"}}}}}