{"entities":{"Q813417":{"pageid":815265,"ns":120,"title":"Item:Q813417","lastrevid":64533057,"modified":"2026-04-11T20:31:30Z","type":"item","id":"Q813417","labels":{"en":{"language":"en","value":"The constructive Hilbert program and the limits of Martin-L\u00f6f type theory"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5005189"}},"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":"Q813417$E9E6810D-095F-40EC-BF42-5857039E940A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"4603daaed073b39dbac83c3ab1fc855d85387b52","datavalue":{"value":{"text":"The constructive Hilbert program and the limits of Martin-L\u00f6f type theory","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q813417$C142DCAA-F3EF-4E05-8E97-28838C3FDB7D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"e759b550dd3b0605d97067b7c2e7887c56016463","datavalue":{"value":"1108.03056","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q813417$7A099939-5879-497C-87C3-55E05DC295D6","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":"Q813417$9D075322-5644-40D0-932B-CD18E8802F02","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"28921346d64a666ce2dd47540df2f388e07634f5","datavalue":{"value":{"entity-type":"item","numeric-id":162813,"id":"Q162813"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q813417$7D6A9B17-A593-42FF-BB93-057E2CD597E9","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7be842e5bc1b54667cb2f669eb29d91c2f271633","datavalue":{"value":{"time":"+2006-02-08T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q813417$18FACCA2-987E-4349-AD91-D6F681F20BCD","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"2dc53fe03d1531d574263bf4b5078b12682ed8da","datavalue":{"value":"This is a survey of proof-theoretic investigations of Martin-L\u00f6f type theory. Hilbert's original program aimed at a consistency proof for the systems of working mathematics in finitistic systems. Constructive Hilbert's program allows for systems which are constructive and predicative. In this connection the author studies constructive type theories due to Martin-L\u00f6f and their extensions. After a general discussion of the theory of meaning due to Prawitz and Martin-L\u00f6f, some specific systems and their connection with popular subsystems of classical analysis are discussed. The system \\textbf{MLF}, introduced by Rathjen, extends original Martin-L\u00f6f type theory by an operation producing a new universe operator \\textbf{S(F)} from each operator \\textbf{F} from families of types to families of types. A stronger system, \\textbf{MLQ}, introduced independently by Rathjen and Palmgren, has universes of type two. It contains a universe \\textbf{M} and a universe \\textbf{Q} of codes for type constructors like \\textbf{S}.   A. Setzer gave a formalization \\textbf{TTM} of a Mahlo universe in constructive type theory. This addition is fundamentally different (``not foreshadowed in Martin-L\u00f6f's original papers''): models of such a Mahlo universe are generated by a nonmonotonic inductive definition. Moreover, \\textbf{TTM} is incompatible with elimination rules for the universe. This prompted Martin-L\u00f6f to respond that universes need not be equipped with elimination rules. Original Martin-L\u00f6f type theory is equiconsistent with the subsystem \\((\\Sigma^1_2\\text{-AC})+\\text{TI}\\) of analysis. In a less formalized section, the author argues that everything a Martin-L\u00f6f type theorist can ever develop can be emulated in a system \\(\\mathbf{KP}^r+\\forall x \\exists M(x\\in M\\and M\\prec_1 V)\\) where \\(\\mathbf{KP}^r\\)is \\(\\mathbf{KP}\\) with foundation scheme restricted to sets and \\(\\prec_1\\) means \\(\\Sigma_1\\)-substructure.","type":"string"},"datatype":"string"},"type":"statement","id":"Q813417$A7F14450-2E96-42FF-A7E5-56779397C382","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"4cb4544bfd0397cd4a315ee326499c372f013de5","datavalue":{"value":"03F35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q813417$FB34F1BA-9F41-4C0B-9665-433BEBC77C8A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"8612eb3fa5372f4e40168b827ed17a01cee8d8f6","datavalue":{"value":"03F50","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q813417$27CEEFFF-28EC-4DA6-BCE4-018BBEF828E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"48a2830216eefdc24b89ba9895c8f20366f6740d","datavalue":{"value":"03A05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q813417$FBD1B8D0-10DE-4BED-999A-CFB1AFD7C4EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"920d53b3830654b0eb4e3a87ec3396145f924723","datavalue":{"value":"03-03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q813417$43AF1A21-1162-4D04-9A90-F69BA2CEE2F4","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"8264ce15cb173f8a4dfa34ee19ea4ef5b68c3f24","datavalue":{"value":"5005189","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q813417$AEA51EA0-0FE1-4992-A714-E421CD461288","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ac29fe212ac0c4f3218093771cefb4e2fa0aea78","datavalue":{"value":"Hilbert's program","type":"string"},"datatype":"string"},"type":"statement","id":"Q813417$6EC4BFFB-EE6C-4B9C-8C6E-39B500F785EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d6c658f92cfca10399e0b9df9aa408c3bc22cae6","datavalue":{"value":"constructive type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q813417$70242F41-1D87-4461-8CEB-A2B92AB43FBC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"45c78721141b4f13208948b9a581723f4d49bc35","datavalue":{"value":"subsystems of analysis","type":"string"},"datatype":"string"},"type":"statement","id":"Q813417$EFDE5574-8C1E-4824-A7A3-8966384272CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"421a43f4b0e8832a026eaa34353c95869f115bee","datavalue":{"value":"survey","type":"string"},"datatype":"string"},"type":"statement","id":"Q813417$87FE513E-0AE1-459E-9E15-586032F636DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0535bcb18ede0a0dbe099058fe51799ceb86ee00","datavalue":{"value":"proof-theoretic investigations","type":"string"},"datatype":"string"},"type":"statement","id":"Q813417$CF97BC38-50A1-4B83-8B37-5D2DBE83E001","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":"Q813417$227E5425-5212-4934-B55B-B8FD28E4BF43","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":"Q813417$57E26BAC-1609-429C-AA3B-2F29ED555A0F","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"db72a2e45a047909ba7abb86192d328e5fb7cdc2","datavalue":{"value":"https://doi.org/10.1007/s11229-004-6208-4","type":"string"},"datatype":"url"},"type":"statement","id":"Q813417$79560456-D702-472C-A432-2C2AC87843EA","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"cfba6922233e38f670b2ad0d6a8168386d3766ed","datavalue":{"value":"W4234140767","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q813417$4015EAAD-28BA-48D1-BBCA-50E541B79D53","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"c04eefff02b2e316a44c6dd3a4910700df42c66c","datavalue":{"value":{"entity-type":"item","numeric-id":1820779,"id":"Q1820779"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q813417$959D3C58-5446-4AA1-A66D-11DDB6C123F2","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":"Q813417$4ED6B1DC-85DB-4598-8141-2CDD6598204D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"13fccbe088f7c3a8c169e6f089f70d6b7da507d4","datavalue":{"value":{"entity-type":"item","numeric-id":3803081,"id":"Q3803081"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q813417$CF5A2672-8A95-44D1-9F93-80BBC0FE08B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f55cb26be29174b1de9acca41e4f1d834db6623c","datavalue":{"value":{"entity-type":"item","numeric-id":4893132,"id":"Q4893132"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q813417$3CD174E3-0F6B-401A-9AB4-CDF676CD3252","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"648a78dd07e758495f78e108cd4a99a5515a6bc4","datavalue":{"value":{"entity-type":"item","numeric-id":5890203,"id":"Q5890203"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q813417$893CABB7-B207-43CE-B631-0D06A83195E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5e74a7a357b1b46dc042b2194329594218f6b370","datavalue":{"value":{"entity-type":"item","numeric-id":1840142,"id":"Q1840142"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q813417$57EA93B3-F140-485A-A220-BB9AF584CEF5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"25eaa6c3e9bb9d8953ff182f9af4a923fe4aa505","datavalue":{"value":{"entity-type":"item","numeric-id":5925300,"id":"Q5925300"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q813417$6D276663-B95C-4953-8D87-1226D19B9268","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":"Q813417$4E098847-17EC-40C0-BE17-ACDD96B7E789","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"492c87567f6dc4126c57966fd5903e66ca640c7e","datavalue":{"value":{"entity-type":"item","numeric-id":5513756,"id":"Q5513756"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q813417$CB17A8FA-D03A-4E0A-BE52-1076D86D8DA4","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":"Q813417$803C5193-ABA3-4146-994B-71270A633A8E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"be12dc0099cec47daf5a4f027d23a1115d169d87","datavalue":{"value":{"entity-type":"item","numeric-id":1317509,"id":"Q1317509"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q813417$CF7D1D40-B564-45B8-BE3F-93C1C649E26B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ecf5e3fed59037f31ea2ef2c7bc3296cc41b0e25","datavalue":{"value":{"entity-type":"item","numeric-id":1308982,"id":"Q1308982"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q813417$575B8948-2A17-4B7A-8606-3BB5186A3A8B","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":"Q813417$B07A2DE5-2E6F-4F1E-948F-BC1DB5E7784D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"442321204f0846e6d42ccce9aff806849d058e00","datavalue":{"value":{"entity-type":"item","numeric-id":1332853,"id":"Q1332853"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q813417$18038E34-E2B0-48F8-A54D-DA36227F08DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5f3cecb3289da431f7f998a9c5561a2c40c346a4","datavalue":{"value":{"entity-type":"item","numeric-id":4868241,"id":"Q4868241"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q813417$2FFA7811-07B7-408D-93A4-47ED5822AE07","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7399a1989b7371f5be019e41f394e87e42894303","datavalue":{"value":{"entity-type":"item","numeric-id":1295396,"id":"Q1295396"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q813417$7902BAE6-83B0-4DFC-B7D9-3F91BE81261F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b27d6328a8e957c4e03f846607d83586f006ef66","datavalue":{"value":{"entity-type":"item","numeric-id":4262568,"id":"Q4262568"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q813417$90B414A5-99C4-4466-AEE7-A64EAC0934F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4d42c52ae3783e5ce29cf68e93f7a7754ce504da","datavalue":{"value":{"entity-type":"item","numeric-id":4944921,"id":"Q4944921"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q813417$55F72F74-7123-4715-AA28-8616DED4B73B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c3079da3af2b234923858f163a08f884ec7b1303","datavalue":{"value":{"entity-type":"item","numeric-id":1407579,"id":"Q1407579"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q813417$27B8280C-FBF3-445F-87DB-E323AE777DF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4961374e6ddb708111e6f7dc9bd89efaafa073e9","datavalue":{"value":{"entity-type":"item","numeric-id":1295372,"id":"Q1295372"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q813417$2DF51F72-1B8B-46E0-813B-E2E14F8C6B1C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1fc1ad39823e87bfa0461332d92468ea40681b5f","datavalue":{"value":{"entity-type":"item","numeric-id":1568707,"id":"Q1568707"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q813417$3E9FFC54-6986-4285-BC39-8ED67B338F73","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d4d64bbc8c36466cd75ac5f7c3e1e13abe00124c","datavalue":{"value":{"entity-type":"item","numeric-id":3731598,"id":"Q3731598"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q813417$36F2B00C-F772-41CC-944A-0C463488E949","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"134f2ad3455f970d41791f7dee3c85343a081049","datavalue":{"value":{"entity-type":"item","numeric-id":3799998,"id":"Q3799998"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q813417$35AA1D36-302C-4EFC-A394-D825F111FF97","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"12e1d8b33ae7c0909dca772fe4ebeb9610db8385","datavalue":{"value":"10.1007/S11229-004-6208-4","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q813417$EB0D145A-22DF-4523-865D-5FA436E11C40","rank":"normal"}],"P1643":[{"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":"746ebd0e780ea526859d86620783a0f9b8010ecb","datavalue":{"value":{"amount":"+0.8885849118232727","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":"Q813417$2F420822-950B-4C3D-AB04-6D3469F6CD91","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":"07a9978b16d414e667d6ee4272a0dc5855edf46b","datavalue":{"value":{"amount":"+0.8678650259971619","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":"Q813417$221E58BF-C5A1-4C47-B4CA-C4278B45DE2E","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":"c14cec61675dc401a7acc20af40d84cfa05146ce","datavalue":{"value":{"amount":"+0.8322589993476868","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":"Q813417$E743A8B1-A03C-4F3D-8B17-6A24199CAAE6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2b3d9899bdce2c77c703aa5bb266fb0dd8900d9f","datavalue":{"value":{"entity-type":"item","numeric-id":1568707,"id":"Q1568707"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"875eae0924d704a7fd43b1c243d28d0e1a6555f3","datavalue":{"value":{"amount":"+0.8286409378051758","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":"Q813417$F4555EC9-8146-4C89-8545-49387348D6BC","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":"d44fc83b23357f9cef014d25bd0b84d44b02fca0","datavalue":{"value":{"amount":"+0.8282896280288696","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":"Q813417$5498AE70-8CD6-4DCE-B2E7-B94D9E2AD595","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"The constructive Hilbert program and the limits of Martin-L\u00f6f type theory","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/The_constructive_Hilbert_program_and_the_limits_of_Martin-L%C3%B6f_type_theory"}}}}}