{"entities":{"Q3984424":{"pageid":6014294,"ns":120,"title":"Item:Q3984424","lastrevid":46226038,"modified":"2025-12-24T08:44:10Z","type":"item","id":"Q3984424","labels":{"en":{"language":"en","value":"The logic of first order intuitionistic type theory with weak sigma-elimination"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 26203"}},"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":"Q3984424$A53A120B-FE11-4AC1-AE8F-2A2FEB446D1E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"7ccba992660f0ad873d62b3249fb9d436a9a7e59","datavalue":{"value":{"text":"The logic of first order intuitionistic type theory with weak sigma-elimination","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3984424$58E334D8-00FF-4A87-ACFF-D64408E993CE","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"8d067204fe15c39ef1ab4da5ec588b655c71873f","datavalue":{"value":"0736.03023","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3984424$22510ECD-42F1-486F-A732-4A50B4626FA0","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"a1dd6809c8e61da37582b97cd1a30ce710877e4e","datavalue":{"value":"10.2307/2274694","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3984424$4848A955-9A96-492E-A7F8-51761D73526B","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"7fb092187e3da8c6f46cf92de2a3d97b047739b1","datavalue":{"value":{"entity-type":"item","numeric-id":3984423,"id":"Q3984423"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3984424$4FBFB725-11C6-48EF-8D42-0A0CC8055C77","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"6218d42f0175ef35f91c4900eb5db86484a9463d","datavalue":{"value":{"entity-type":"item","numeric-id":2710590,"id":"Q2710590"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3984424$04124E31-B1FE-4637-BF5D-73974604F6C5","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"70844ffc4666eabac4e20376c648613dbe8620f7","datavalue":{"value":{"time":"+1992-06-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":"Q3984424$56BE69D5-B13E-4631-9F8A-7E1B5D3388B9","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"c15287dbb142f8dc10ab92a91b8457ac3c169cd3","datavalue":{"value":"03F30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3984424$0EDF97E1-184D-43C9-9C32-AEEE37EE1C90","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"6fea4e1298530f5baafa25e3937047b9bb693440","datavalue":{"value":"26203","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3984424$560CCD36-EF1E-4A17-9BBC-EEC25BDC259E","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1c27aaefaca086e3479197817bf1c432e3cd4a1a","datavalue":{"value":"first order intuitionistic type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q3984424$AAFB9782-184E-4460-BF0C-401E169452D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4dc9d383115e6df8bf87849eca646dc9254ade85","datavalue":{"value":"weak sigma-elimination","type":"string"},"datatype":"string"},"type":"statement","id":"Q3984424$406CD273-5144-45B5-A240-57A699CE4541","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2fe4a9cb5a01575569da056946827705306547cb","datavalue":{"value":"realizing terms","type":"string"},"datatype":"string"},"type":"statement","id":"Q3984424$CA08E2FA-A0D1-42C0-8518-9E7D0A2C243D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"63e775fb86fd9db0cbf6562ca43643106db2e78b","datavalue":{"value":"existence elimination rule","type":"string"},"datatype":"string"},"type":"statement","id":"Q3984424$9FAB8781-6C6A-4EE8-901F-2F9FAF7DE806","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"97c6b970990dab40d69357bafd674174e833bc7d","datavalue":{"value":"Heyting arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q3984424$E31777E0-F890-46EB-B4CE-310A9598EC17","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d636c3e4adbc6194aca5172cbc24461c115e7b9e","datavalue":{"value":"first-order intuitionistic arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q3984424$E564E0D1-BD4A-41EE-8ECA-C13DFF5BE77A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"86883f625eb9ea1d0f9d5e4e00110dbc1e213e44","datavalue":{"value":"conservative extension","type":"string"},"datatype":"string"},"type":"statement","id":"Q3984424$84245D76-9864-4123-AC26-AD27F2FCB81B","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":"Q3984424$3C8476BF-9A66-4672-92AE-CB34851BD2CB","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"16377bdc50f71b8872bd12ee3f7cef30b4e7513a","datavalue":{"value":"https://doi.org/10.2307/2274694","type":"string"},"datatype":"url"},"type":"statement","id":"Q3984424$FBF1EC35-83F9-476C-9541-CB3FB9FC3ACF","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"9c27407987ab08f8213dcaec7088d3e937b293d0","datavalue":{"value":"W2017441861","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3984424$E27A066E-EA48-4670-A508-F87594FDC960","rank":"normal"}],"P223":[{"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":"Q3984424$F8927DD6-B9A0-4A20-BE7B-C5283F5F4156","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d0fb884ac064fe53820dee52be77088fccc117d6","datavalue":{"value":{"entity-type":"item","numeric-id":3160566,"id":"Q3160566"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"50df1c490eec6bdcf6393e25c8f190b9d483f5af","datavalue":{"value":{"amount":"+0.7536851763725281","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":"Q3984424$147E6DA9-34C1-4606-A9EB-91B4D4D6AF01","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"696d83aaec159cdf8ddedd031545e8cc3910de03","datavalue":{"value":{"entity-type":"item","numeric-id":4247306,"id":"Q4247306"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d5e6f78b700523afe9a74721f633f871590c70d7","datavalue":{"value":{"amount":"+0.720390796661377","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":"Q3984424$678DB25F-BC74-47E4-AB2B-41B6BECC56A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"edc0a43a649037aff843d9e62cc66bf2911a8e7b","datavalue":{"value":{"entity-type":"item","numeric-id":3312222,"id":"Q3312222"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f65a250f07b4b337deb6903581c7914885d58d34","datavalue":{"value":{"amount":"+0.718227744102478","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":"Q3984424$ACA5DD80-750E-4726-AD3C-B11C322E6376","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e5c03adfd0d13ffb9cca204894d0f8ede1fe92d2","datavalue":{"value":{"entity-type":"item","numeric-id":3086776,"id":"Q3086776"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"06f151a1b2cf46d6fefd418ecfb3f6195dd8b674","datavalue":{"value":{"amount":"+0.7179197072982788","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":"Q3984424$D1505952-0865-4559-98A3-C54356D56F5A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3984424","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3984424"}}}}}