{"entities":{"Q2478553":{"pageid":2489296,"ns":120,"title":"Item:Q2478553","lastrevid":74360457,"modified":"2026-04-14T19:43:55Z","type":"item","id":"Q2478553","labels":{"en":{"language":"en","value":"Full classical S5 in natural deduction with weak normalization"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5255280"}},"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":"Q2478553$896CC9E2-48FE-40F0-A9F5-37DCD062F74E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f4d8ff285b4eae2d5a857378df76c26bb1b6082c","datavalue":{"value":{"text":"Full classical S5 in natural deduction with weak normalization","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2478553$B5234220-3E7C-44FD-9BD3-1F1E61946856","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"01dfce9a4e3e97b407b2e324b0b4c60c42be921a","datavalue":{"value":"1137.03011","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2478553$31687B8D-4D4A-4F86-A647-412B6735C334","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"a4e29a6551ed654b95caa163f18d6589ab9dd41e","datavalue":{"value":{"entity-type":"item","numeric-id":654909,"id":"Q654909"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2478553$5E7203DE-BB31-40AE-905C-A323A7DD7CAB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"0ade6822716119172a1ac7ace87519af4c88505f","datavalue":{"value":{"entity-type":"item","numeric-id":2478552,"id":"Q2478552"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2478553$27DE52BC-6EAC-4129-87DD-0487A712FCE3","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f91a4bcbc93435aed71775d25a4c5cd09e26f12d","datavalue":{"value":{"entity-type":"item","numeric-id":122505,"id":"Q122505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2478553$590262ED-16DA-4047-B0EA-1F62C6B7A556","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"19b8f2af7f0986c9c462b75f4a8bfb541c843b8d","datavalue":{"value":{"time":"+2008-03-28T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2478553$EE711484-FC2C-4C4A-95F4-E7C0B6794E6C","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"b628739c9bf825cacffc5c22d80fa8ea67c089da","datavalue":{"value":"The paper investigates natural deduction systems for the classical first-order modal logic S5. Several natural deduction systems for S4 were presented in the literature, but none of them admits normalization in the full language including \\(\\lor\\), \\(\\exists\\), and \\(\\lozenge\\). In the present paper a new natural deduction system is introduced, based on a system investigated by \\textit{D. Prawitz} [Natural deduction. A proof-theoretic study. Stockholm-G\u00f6teborg-Uppsala: Almqvist and Wiksell (1965; Zbl 0173.00205)], but using a new version of the \\(\\lozenge\\text{E}\\) rule involving the notion of modally independent formulas. The authors present reduction rules for the system, including a detailed proof of correctness. The main result is a proof of weak normalization for the system, and the subformula property for normal deductions.","type":"string"},"datatype":"string"},"type":"statement","id":"Q2478553$EC25473D-A623-4F01-AB49-E703846A9613","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"bf05c748b19f894b0cb445a65a1da1ca24dbc809","datavalue":{"value":{"entity-type":"item","numeric-id":331053,"id":"Q331053"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2478553$2E69EE30-A159-42D8-81DA-AA85D7ACD714","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"74a6cec96241e450625296e63e8dd539239d7104","datavalue":{"value":"03B45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2478553$E718ADE6-50B8-47C7-9DB8-EBEE5523961A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2478553$8D337099-2330-4616-86BA-1EB1B70C859A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"d84a96964dba5f99e8e555154ac62eec443f8a07","datavalue":{"value":"5255280","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2478553$A0944815-B2C3-47CF-B77A-23ED34B5C7C9","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a7245057d33d9a959e820bafe53b372c083536e6","datavalue":{"value":"natural deduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q2478553$F7A97D16-DA1F-4F1B-93A7-980769DD9521","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4296281254337308ad2c5f734043898466afdb58","datavalue":{"value":"normalization","type":"string"},"datatype":"string"},"type":"statement","id":"Q2478553$3394162A-3C98-4485-9B43-182C6E831CB2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f1dda010537b7b36bd45151721146f720815706e","datavalue":{"value":"modal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2478553$4F17C86E-E30B-44E1-AF1D-3D8926AF8A51","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"69b31587c96a5c5ccf3b12532333e2056e86a541","datavalue":{"value":"S5","type":"string"},"datatype":"string"},"type":"statement","id":"Q2478553$F848E3EB-204D-41D0-863C-7E202703758B","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":"Q2478553$ADAC0406-14BE-4F4D-979C-5665718F69CD","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b510acd792b43e4dd165c97470158752ab68c2b9","datavalue":{"value":"https://doi.org/10.1016/j.apal.2007.11.007","type":"string"},"datatype":"url"},"type":"statement","id":"Q2478553$78A6DED8-7B2E-4F81-B660-39A65B5F1C46","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"03762e58b7493642359aa0534909d18035fe2714","datavalue":{"value":"W2024316283","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2478553$F56C94AD-E800-451F-9C99-D3091C45D1B5","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"811458264a650a109340a5030fad038d17897be7","datavalue":{"value":{"entity-type":"item","numeric-id":4511541,"id":"Q4511541"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2478553$5619CE35-3A13-4B7C-97DF-78492C0639DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ec2935c4b500510e6236922988f2719b77d5497a","datavalue":{"value":{"entity-type":"item","numeric-id":4286223,"id":"Q4286223"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2478553$4E7E53D8-2DD4-445A-B887-67F3F600CB6F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dd19a4e2034c91a5498cdb406e681e58c88076cf","datavalue":{"value":{"entity-type":"item","numeric-id":3410675,"id":"Q3410675"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2478553$38F373FC-0A96-47FC-8CE3-14A3A52C07CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4809852e773671781a76300a7acfb1d5b189851e","datavalue":{"value":{"entity-type":"item","numeric-id":5598335,"id":"Q5598335"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2478553$89E1B645-2AB7-4425-97C2-E7893E2557D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c8546dfa3ee45536454a034a5905b0e5f07e2b82","datavalue":{"value":{"entity-type":"item","numeric-id":812101,"id":"Q812101"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2478553$61AC0D78-A941-4935-9E3C-A18C92173E3D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7b193fe960fc7f19e24d6d068b46e526b1b801aa","datavalue":{"value":{"entity-type":"item","numeric-id":3247119,"id":"Q3247119"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2478553$67A8F878-124C-4C0E-847C-71F70EDCFEAD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"626844e9f28589d93bd8625672a9cd46823c520a","datavalue":{"value":{"entity-type":"item","numeric-id":3262211,"id":"Q3262211"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2478553$FDB7B23A-B17D-4F23-BEE1-6C758894D546","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b8d95625ec9e5b7c46cee42d87256157d982706a","datavalue":{"value":{"entity-type":"item","numeric-id":5559220,"id":"Q5559220"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2478553$F23A6C6A-F3B3-4E64-8C0F-D285F7A7DE34","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0c232a4ac94055e2cc6462047a2680a2578759dc","datavalue":{"value":{"entity-type":"item","numeric-id":3887437,"id":"Q3887437"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2478553$09BF0612-A095-4B97-91A7-397B8980F061","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"05bb3cb718675c3fe3133c1db7ce063709950989","datavalue":{"value":{"entity-type":"item","numeric-id":583185,"id":"Q583185"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2478553$0B6C3E0C-A667-4491-ACD4-7D3F016AB032","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"19bda7bf2b683d32fb9bd0a60fb1ebf165437c69","datavalue":{"value":{"entity-type":"item","numeric-id":3832540,"id":"Q3832540"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2478553$31E9C7BD-C915-4626-BDB3-B4890B3DCE9A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e9b533f9290e16b7753893188b8dbe265e96125e","datavalue":{"value":{"entity-type":"item","numeric-id":3981450,"id":"Q3981450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2478553$FA938480-BF10-4982-A756-E25D57A4F3CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"556c63d3d5fbb69adda2aaeb321f31370f38a3b9","datavalue":{"value":{"entity-type":"item","numeric-id":4716271,"id":"Q4716271"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2478553$C6ADF789-D23E-4B6A-87BC-DB51E6682E65","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4b364519c59a0fab47d2f80de511d01e3b117502","datavalue":{"value":{"entity-type":"item","numeric-id":4291036,"id":"Q4291036"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2478553$ECE6ABDB-C28A-495C-A154-FDAFCE9FF010","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"89b4494896a4b99b3600c3c74b96d1c1426ce339","datavalue":{"value":"10.1016/J.APAL.2007.11.007","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2478553$120396A7-9CEF-4299-8CD6-A051CA096461","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2b0346cb07c892f61a7f5b431ff4ebc45d81b80c","datavalue":{"value":{"entity-type":"item","numeric-id":3410675,"id":"Q3410675"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"109df556c90121145edc8e98b2ae89555813c4a2","datavalue":{"value":{"amount":"+0.8458924889564514","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":"Q2478553$15C9B553-93B8-448C-AEF8-4EDA7D684257","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9f9f633fbfc462c62fc2b5a1a1bd52c4b4f11392","datavalue":{"value":{"entity-type":"item","numeric-id":2890694,"id":"Q2890694"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"03ca68de50b9f182efbac085825a04c2f2739676","datavalue":{"value":{"amount":"+0.8322320580482483","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":"Q2478553$7903A100-01F6-4A7C-B5FE-8C1166286F4E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a236dd4a950afbad6ad4fd292dfce0becd66ca84","datavalue":{"value":{"entity-type":"item","numeric-id":1758660,"id":"Q1758660"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9c7e4bc51e59e5a63c8e9221f0942e9a724b1edf","datavalue":{"value":{"amount":"+0.8137553930282593","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":"Q2478553$34581FE5-63F3-445E-8D99-A59D813FD72E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fd0408c0d7dfc173c00f52df72da5ff9eeb3b8e2","datavalue":{"value":{"entity-type":"item","numeric-id":3981450,"id":"Q3981450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"09f0f682d6aaa3cae76b471a282aceae718c5fb4","datavalue":{"value":{"amount":"+0.807379424571991","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":"Q2478553$B34B4C90-1494-4D30-8D22-BEA852E89260","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7aa2766298d4a67b56a1f300df3b109a9b40f45f","datavalue":{"value":{"entity-type":"item","numeric-id":5704814,"id":"Q5704814"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e90e101160e64b0df37ead4e0609c631708872d6","datavalue":{"value":{"amount":"+0.8073787093162537","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":"Q2478553$0389B0C7-DD5C-42C9-8EDB-9311EA9111B4","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Full classical S5 in natural deduction with weak normalization","badges":[]}}}}}