{"entities":{"Q2785696":{"pageid":2796434,"ns":120,"title":"Item:Q2785696","lastrevid":47422414,"modified":"2026-01-01T17:09:08Z","type":"item","id":"Q2785696","labels":{"en":{"language":"en","value":"Intuitionistic model constructions and normalization proofs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 981837"}},"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":"Q2785696$7E3078C7-B8F3-4E3B-A87D-02589BB582F5","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"5ade22611e497e043fd839d31d4e3fb5b880651e","datavalue":{"value":{"text":"Intuitionistic model constructions and normalization proofs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2785696$6B154405-6EE1-4E33-8FCC-368CC14BB4A9","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"a0b32b4a89270005363f25bf6e20fe1e018653c1","datavalue":{"value":"0883.03009","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2785696$FD61A8F3-F6F7-4995-B2D5-F6A0CA7DC8DA","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"4dfc78d69f40faaa4f4665d5f9f4b71c1776c673","datavalue":{"value":"10.1017/S0960129596002150","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2785696$58BFB4B8-90D3-4C0D-AA3A-6085430BE15E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"5aad179d365c253d181fa8115a831f46e7923370","datavalue":{"value":{"entity-type":"item","numeric-id":375196,"id":"Q375196"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2785696$222CA042-C7E8-4A6C-B2A0-5E361D8CA267","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"1d75275853fb84ac426baf809ec86decf612055f","datavalue":{"value":{"entity-type":"item","numeric-id":651314,"id":"Q651314"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2785696$255890CC-2187-4D0D-AFE4-2E2A85ED5AA3","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"20d9699532b3f4e30cf94a2814dc68ff83c6f6ad","datavalue":{"value":{"time":"+1998-03-23T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2785696$D9E6902D-C151-4B99-94AE-DCB6FFA917DE","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2785696$B33B1ADD-3921-41DA-AB9A-183A4692A691","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2785696$197FDE29-067B-41B3-B58C-000F64154F27","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"4cb4544bfd0397cd4a315ee326499c372f013de5","datavalue":{"value":"03F35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2785696$4A6BD6F8-F85C-4226-A882-D4C6CE7A5A16","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"40d293f5d2161e80872b42afb12a3fc45e5d1401","datavalue":{"value":"68Q55","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2785696$B1324E1D-1E03-4868-8AEF-7570E31DA72E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"675638cd39adb6c14034a9102a7c1aebed580606","datavalue":{"value":"981837","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2785696$896E43AE-6381-4067-9F1E-B357F6FFD1AF","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4296281254337308ad2c5f734043898466afdb58","datavalue":{"value":"normalization","type":"string"},"datatype":"string"},"type":"statement","id":"Q2785696$2F9D58B7-7364-4CD2-9C37-ECE80C76F7A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5d7bfc11de8cab95fd6af201970bd9d16d39bbd0","datavalue":{"value":"semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q2785696$D154339F-3811-4497-8F5F-6B5A2350EBCF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1c921fe1466ebc2433d301059dabf74d60594538","datavalue":{"value":"glueing","type":"string"},"datatype":"string"},"type":"statement","id":"Q2785696$976ACC8E-2252-4635-B5E8-AB12B162594B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"977be43240ff0a597497403ba31bef94a94c1066","datavalue":{"value":"Brouwer ordinals","type":"string"},"datatype":"string"},"type":"statement","id":"Q2785696$B7EEF076-6A89-4639-99FC-C2FCB8F2160B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9a3226108c117e3457b037a1b852cfa9c0275534","datavalue":{"value":"intuitionistic metalanguage","type":"string"},"datatype":"string"},"type":"statement","id":"Q2785696$5C7B5594-9819-4DA2-A0E3-360BE6630945","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"454090389315247a59dda8a7c520ea2795715012","datavalue":{"value":"Martin-L\u00f6f type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q2785696$4F37BA25-FB92-4CC8-9622-CD6E81A12450","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"628486270ea1716fe7f02cac600ffe4439992f99","datavalue":{"value":"proof-assistant ALF","type":"string"},"datatype":"string"},"type":"statement","id":"Q2785696$BC5CCE25-92D5-42F0-B098-A99CB7883D77","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":"Q2785696$D61B5D6B-8D42-4CF5-ACED-4ED8B28236C0","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"069735a2fb0585be45de9d1363f7f87033a6c83b","datavalue":{"value":"Q129355992","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2785696$9B834EDF-CCA9-4C1A-AD63-D8FAF3746B6B","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"7ec159f1e880362cf671a113c6496de63141fbbf","datavalue":{"value":{"entity-type":"item","numeric-id":6768254,"id":"Q6768254"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2785696$8AFAEE76-C649-41C5-9C7B-A4AB7048556D","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"d1f9e0b7d3528d1c8dfdbd905a1737e4c319fc93","datavalue":{"value":"This paper aims at giving a semantical treatment to normalization. The idea is to build a nonstandard model, and besides the interpretation function \\([\\cdot]\\) from terms to the model, to define a function quote assigning each element of the model a normal term. Then the normalization process is obtained by the composition of these two functions \\(a\\to \\text{quote} [a]\\).NEWLINENEWLINENEWLINEThis is first achieved in the case of G\u00f6del system \\({\\mathbf T}\\). After having defined the semantics and the function quote, the authors prove this indeed gives the normal form, using a glueing technique due to Lafont, related to the glueing construction in cateogry theory. This result is extended to languages having disjoint unions and cartesian products, and to Brouwer ordinals.NEWLINENEWLINENEWLINEThis work is done in an intuitionistic metalanguage: the last section justifies this choice, and relates the formalization to Martin-L\u00f6f type theory and to the proof-assistant ALF.","type":"string"},"datatype":"string"},"type":"statement","id":"Q2785696$7330FA22-966D-4A44-A6CA-D48FD4DE5D68","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"be9393a59da8a8d1ea400e796ca1cda2084f6804","datavalue":{"value":{"entity-type":"item","numeric-id":1208424,"id":"Q1208424"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2785696$08E6A877-688D-4212-8393-3EA2F3A49EE5","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e9e0fc5f0014bdd6c8e8417e372280fe791b4099","datavalue":{"value":{"entity-type":"item","numeric-id":1891251,"id":"Q1891251"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b087ccf9380106823c873679025a1b028619debb","datavalue":{"value":{"amount":"+0.7545028328895569","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":"Q2785696$78CBEA8C-B04D-43A6-AE7B-2E4E6F330D30","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c0936483cf1d4bbe312da2105c45d60ab35d4a7d","datavalue":{"value":{"entity-type":"item","numeric-id":5313717,"id":"Q5313717"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"39a92e3e8856ae2be6ce1c15968408c15d9f6b55","datavalue":{"value":{"amount":"+0.7513521909713745","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":"Q2785696$D3A62FAD-7D4C-44A4-B0D6-72FBBA8D56C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a8c39ff1703fa649627f769e20a60cac8c6f394b","datavalue":{"value":{"entity-type":"item","numeric-id":4281467,"id":"Q4281467"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"29956f27a2e3f82f68b50ecec3ae10f75faf85a7","datavalue":{"value":{"amount":"+0.7347297072410583","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":"Q2785696$5020570F-75D0-4608-8B6D-3D037948D4A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a11a1210fbc388975d2c306dcac20ebc18d71c5a","datavalue":{"value":{"entity-type":"item","numeric-id":817701,"id":"Q817701"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a36f97a2cdaa271b3798f966b0d1a0e8b9313454","datavalue":{"value":{"amount":"+0.7293553352355957","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":"Q2785696$A7C088BA-DF53-4D31-8B0A-95B71D7F3D98","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6d4ba777ec3d69929aae1fe702e999be4e6dd481","datavalue":{"value":{"entity-type":"item","numeric-id":5308449,"id":"Q5308449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"04407991104865d392f196393a9f63b40d968783","datavalue":{"value":{"amount":"+0.7284772396087646","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":"Q2785696$344EEEF8-FFCA-4CE0-B30A-95AF44273F93","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2785696","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2785696"}}}}}