{"entities":{"Q1820157":{"pageid":1830899,"ns":120,"title":"Item:Q1820157","lastrevid":71358630,"modified":"2026-04-13T21:43:01Z","type":"item","id":"Q1820157","labels":{"en":{"language":"en","value":"Embedding intuitionistic-type theory in negationless-type theory"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 3993583"}},"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":"Q1820157$61B4740D-3A88-4EF2-BB52-08271B3B80DF","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"cc2e034d9029115f524d8be3af460e693960ccb8","datavalue":{"value":{"text":"Embedding intuitionistic-type theory in negationless-type theory","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1820157$1CFD9854-756D-4781-A11D-8D9A6A2DF465","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"e8e8f527833df7a0efbf7f84698bab27634a47b1","datavalue":{"value":"0614.03057","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1820157$841E4C07-1FDD-4ECA-93DB-B6B0C76BA677","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"5e8030cb9d057d205994e6d5f9ffafddab99e312","datavalue":{"value":"10.1007/BF01647635","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1820157$4DE34C7B-9669-4DCE-841D-CD2C2386B9E8","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"00de3e6b6cfff0576fe0e1d6bc63c05579d2cb43","datavalue":{"value":{"entity-type":"item","numeric-id":173953,"id":"Q173953"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1820157$DB3D8BBB-B83C-4ACB-ABB4-27A5AF73026D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"63df7153432d81fa42019fcabb076c89649b0b5b","datavalue":{"value":{"time":"+1986-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1820157$F55BA6F1-93C1-4B11-A281-48ECC11B72B9","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"053b6c6ce040dd2a632490741f44880b5a9733bc","datavalue":{"value":"In ''A formal system of negationless arithmetic that is consistent with respect to Heyting arithmetic'' [Mat. Zametki 36, No.4, 583-592 (1984; Zbl 0576.03037)] the author shows that Heyting arithmetic is a conservative extension of \\(HA^ N\\)- a system of negationless arithmetic, under certain interpretation. Here he extends this result to the case of intuitionistic type theory HATT and a system of negationless type theory HATTN.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1820157$023DD301-0720-4AD0-AF37-0A2561062894","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"3068729a394ad5bf58a1a3e5b5d24254d962e1a7","datavalue":{"value":"03F55","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1820157$AE4623A5-EEDA-4B4D-91BE-84F99593BA8B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"4dd17e948ef0e266d136e969bf8283741afbd898","datavalue":{"value":"03F25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1820157$92CB36B4-BDBC-434A-A52D-922BCCB9AE45","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"30a52282cc33797e116b5ae405090640737ec048","datavalue":{"value":"3993583","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1820157$C91E9A73-150F-43B4-8CD3-EFB6EBD326E6","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"97c6b970990dab40d69357bafd674174e833bc7d","datavalue":{"value":"Heyting arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1820157$A4D66E9C-9E94-45DD-B8E2-B827A9622BB5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"486173fdea484958e371bcc478b16d274811d71a","datavalue":{"value":"intuitionistic type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q1820157$03C3C6B1-D560-4F88-8A59-36903964AB2B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9ee4330d294b86136ba38f14b168d8a24addfa33","datavalue":{"value":"negationless type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q1820157$3E8F3B43-DE07-4CED-9153-AE7C6C426942","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"6ab8df4cb13a509b9920268449820b6d1c56d9fb","datavalue":{"value":{"entity-type":"item","numeric-id":708926,"id":"Q708926"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1820157$380B85DC-B408-42CB-AA56-1DEEA3BDA11C","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"cc2fe705c7d582d4c8ad19b50ec74a3e6e0c8ae1","datavalue":{"value":{"entity-type":"item","numeric-id":384285,"id":"Q384285"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1820157$51338C41-7E6D-48F9-A6F1-25C8884174B8","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":"Q1820157$93F2AC76-A38D-46EA-8E52-522F051A8220","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"5e544c5a1043464872c16e5abf16d98383bc192e","datavalue":{"value":{"entity-type":"item","numeric-id":1064322,"id":"Q1064322"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1820157$8DD0D5F2-C691-4637-8567-928B68415C2B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"915e0053bd453fe55614285248cc714c3d3631eb","datavalue":{"value":{"entity-type":"item","numeric-id":5798786,"id":"Q5798786"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1820157$06BD9D42-D006-4294-A2D5-D8C35CEBF5AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1b0d374a436b3eff4a0fc4a6b0d2d906601e7f54","datavalue":{"value":{"entity-type":"item","numeric-id":4175544,"id":"Q4175544"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1820157$D2529D14-4AD9-405F-98E5-5503E6318FDB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"384c88ee747368e498e55b1ebc22017816448ffc","datavalue":{"value":{"entity-type":"item","numeric-id":2265415,"id":"Q2265415"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1820157$83B14386-EF13-475B-9EE8-2F1B1C5AD761","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bde49d340fc11ee93ba23ea9f0306fc1d0f12d42","datavalue":{"value":{"entity-type":"item","numeric-id":1064322,"id":"Q1064322"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9dbcfa2efd9802c77437f33a3d0c4c292d3c8bde","datavalue":{"value":{"amount":"+0.8692122101783752","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":"Q1820157$8A1AB607-9203-40D9-B490-3DBC7AE7A4B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6b6e9bdf0351f174bb4b113f793f9c84aea20849","datavalue":{"value":{"entity-type":"item","numeric-id":3710527,"id":"Q3710527"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b3e5e4a1bcee7bec97b1f065f56a62ad4c599a91","datavalue":{"value":{"amount":"+0.8226082921028137","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":"Q1820157$2F4CAE25-6665-4339-B7BD-2B3A7D0DCBD8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c78d250f210d712df110178ea581fe6231fd5f37","datavalue":{"value":{"entity-type":"item","numeric-id":1841006,"id":"Q1841006"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8fb08a0db8e06a0935e9f59ee86cc211bf92ec69","datavalue":{"value":{"amount":"+0.8166217803955078","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":"Q1820157$0E4B8C08-E08E-4514-97D8-A777B4B26C6B","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":"8fb08a0db8e06a0935e9f59ee86cc211bf92ec69","datavalue":{"value":{"amount":"+0.8166217803955078","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":"Q1820157$63F739AC-24BB-4264-83A0-32FD23D09149","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1924603f46c222f8c941729d07d9f284a3dcbd13","datavalue":{"value":{"entity-type":"item","numeric-id":1582305,"id":"Q1582305"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"298c03ae9e29c890be5c580cb6665a7bbf616e2a","datavalue":{"value":{"amount":"+0.8152740001678467","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":"Q1820157$B64F534A-81BF-40EC-8157-B10935A3C24A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Embedding intuitionistic-type theory in negationless-type theory","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Embedding_intuitionistic-type_theory_in_negationless-type_theory"}}}}}