{"entities":{"Q1192582":{"pageid":1203331,"ns":120,"title":"Item:Q1192582","lastrevid":70244829,"modified":"2026-04-13T13:28:03Z","type":"item","id":"Q1192582","labels":{"en":{"language":"en","value":"Lattice-valued representation of the cut-elimination theorem"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 61131"}},"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":"Q1192582$DBD307B9-6B72-4CE7-A83B-8999D5996BD9","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"2b5dbff66ccaa91e9b625d9e0b77c6c69223d71d","datavalue":{"value":{"text":"Lattice-valued representation of the cut-elimination theorem","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1192582$E61EBAF3-16F0-4404-90EB-3132883F7749","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"4f7944ae2e2ffceee8f5c848c7e8d6dcbd1013ac","datavalue":{"value":"0758.03026","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1192582$70E379ED-6FED-48AB-8429-B7E92F48231D","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e3a0bf1dfe04ad12e1226221d4ab68e1adf5a243","datavalue":{"value":{"entity-type":"item","numeric-id":766668,"id":"Q766668"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1192582$6F975BFC-74ED-4D03-B096-3F6D28BB94B8","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"4644ee9c6c93e22a4aa2641411a372d7ea43bad8","datavalue":{"value":{"entity-type":"item","numeric-id":180651,"id":"Q180651"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1192582$58B02A0E-FC7F-47C1-9F0B-6F6614B3E45D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5fd62271fe98c7ff9916cafed51cf35315eeeb31","datavalue":{"value":{"time":"+1992-09-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":"Q1192582$A4B8A52F-1DBE-44E3-9765-409A2B23D94B","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"72bf42311af3d2ffe0e7762e76fa01092445fd50","datavalue":{"value":"Let \\(L\\) be a relatively pseudo-complemented complete lattice, \\(F\\) a set of formulas of a formal system (classical or intuitionistic). The author considers mappings \\(m,M: F\\to L\\) satisfying a series of conditions. For such pairs of mappings he proves, as his main theorem: \\(m(A)\\leq M(B)\\) for any provable sequent \\(A\\to B\\). In the final section, he uses this result for a proof of the cut-elimination theorem.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1192582$93FE2278-0D32-41EB-9FE0-E33DE50ECF4D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1192582$4B5CC9D1-BA07-41FE-A783-6B18932EA088","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"625495dc8cf796ad780e9da29b6a4a78ebce22b1","datavalue":{"value":"03G10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1192582$769D29FC-F719-4258-A6E2-16D4C17F6A22","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ba131400619cc06511c18b918658536614eadc44","datavalue":{"value":"61131","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1192582$157A38F1-FA91-4C40-92E9-CF575A270E81","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"137c05a8be7886892655f96be1c42040dc46a026","datavalue":{"value":"relatively pseudo-complemented lattice","type":"string"},"datatype":"string"},"type":"statement","id":"Q1192582$436F98BF-0C24-424D-A37F-DCB6E1CF6B88","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f3b508d1c668c3f2ebe0545e823f48d2d5ecfb07","datavalue":{"value":"formal system","type":"string"},"datatype":"string"},"type":"statement","id":"Q1192582$8938BF1C-8FDA-4CFA-9425-0A53648647A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"97cfbdd458b576a7e018dc279ea34c5cb4040b6f","datavalue":{"value":"cut-elimination theorem","type":"string"},"datatype":"string"},"type":"statement","id":"Q1192582$37F63265-B84A-4780-B971-7185207D345C","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":"Q1192582$7E778585-2D21-4AF0-BF25-AF1A195DB2B6","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"eaaa0ded96ea5d2e5236ab02f45c61481f95162f","datavalue":{"value":"https://doi.org/10.21099/tkbjm/1496161672","type":"string"},"datatype":"url"},"type":"statement","id":"Q1192582$B5AB8439-6AE2-4891-8155-BDD73A891C80","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"2992e16acebbe9b3cd88560b1b6a0137fe6deb4e","datavalue":{"value":"W212831703","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1192582$86557673-B39B-4F5F-BE57-5848EB373306","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"674e477a5c98f6421c64ee977fc93c54c12a77df","datavalue":{"value":"10.21099/TKBJM/1496161672","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1192582$DF845666-54AA-4B0D-A482-60BE703CD550","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"46b5a6d83c8bf78c369b5dc9de3fd884d49717fa","datavalue":{"value":{"entity-type":"item","numeric-id":3792660,"id":"Q3792660"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0f59f9db1f6d527efcd6ecab2df57948b2f3fdbe","datavalue":{"value":{"amount":"+0.7501371502876282","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":"Q1192582$A43890EF-ED77-480D-BF3B-422F6BC622BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"def566653383fe43ae785d4d493075f5d38d38ce","datavalue":{"value":{"entity-type":"item","numeric-id":786808,"id":"Q786808"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"15e5b212fbc16595750f8a417ef1bcb5ba899498","datavalue":{"value":{"amount":"+0.7285366058349609","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":"Q1192582$44470959-EE10-4333-A5FE-DB133297BBD4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"68211a7e42d5820c042f0e78f684627476a3887e","datavalue":{"value":{"entity-type":"item","numeric-id":1770974,"id":"Q1770974"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4bf95c48daae3542ec9b5d76d51eef4dc1a346a2","datavalue":{"value":{"amount":"+0.7245081067085266","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":"Q1192582$802CE050-E0E1-430A-9E1F-180C72C0A4C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"24ec36d3999143771f5f3c520416695cda36ba0c","datavalue":{"value":{"entity-type":"item","numeric-id":4818936,"id":"Q4818936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"aa3a25fb326937d7d47553a65d38f1fa66849754","datavalue":{"value":{"amount":"+0.7240205407142639","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":"Q1192582$2C6F65CF-20FF-445E-A20C-25B0E60714C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9ffab1ec510f63ff1e2a9542c3c3be4322ba4905","datavalue":{"value":{"entity-type":"item","numeric-id":5704011,"id":"Q5704011"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"46778bd420e7022081542feea4345a70aabdec62","datavalue":{"value":{"amount":"+0.6976268291473389","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":"Q1192582$2D27A429-8FC9-4BE2-AE30-C20D6D6B6C2F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Lattice-valued representation of the cut-elimination theorem","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Lattice-valued_representation_of_the_cut-elimination_theorem"}}}}}