{"entities":{"Q1024553":{"pageid":1026401,"ns":120,"title":"Item:Q1024553","lastrevid":66568164,"modified":"2026-04-12T10:59:59Z","type":"item","id":"Q1024553","labels":{"en":{"language":"en","value":"Syntactic cut-elimination for common knowledge"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5565760"}},"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":"Q1024553$F4FA88AA-C7C7-4CE7-A45E-B3091FA0D1DF","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d41a9d10df3762e92e534132769a6cb7b635e859","datavalue":{"value":{"text":"Syntactic cut-elimination for common knowledge","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1024553$1D7F648B-C2BD-4C85-83EB-0EE43190B2BD","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"033e74317c4afe643fd39007008456be402a12e4","datavalue":{"value":"1170.03007","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1024553$E538B8A3-842C-4454-A4CB-3AC3A5514FA6","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"1a4b8e93464bd8436b70044ab37bdd425a7513d2","datavalue":{"value":{"entity-type":"item","numeric-id":714716,"id":"Q714716"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1024553$26908FDF-D428-48C9-92A1-B4B97854223B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"6a23089233c6f9a342152a9a3a402eea56cc40e3","datavalue":{"value":{"entity-type":"item","numeric-id":194999,"id":"Q194999"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1024553$5DC1B270-9B2C-4A47-BBC7-E07A2666A1F8","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":"Q1024553$5A52CEEB-316C-4E52-A112-1C2977F58995","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b56d9fd9827ead92e1d841b592f7852bcfece777","datavalue":{"value":{"time":"+2009-06-17T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1024553$BFF14FBB-D5E7-4E08-AF6E-BEF6F91ECB86","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"9a5eeeda563cf1fae121af1ebb187af59bb6b700","datavalue":{"value":"The logic of common knowledge has been formulated by Alberucci and J\u00e4ger in a sequential system with a rule of infinite premises so as to enjoy completeness, from which then follows the cut-elimination theorem indirectly. There are also several variations of the logic formulated in cut-free sequential systems but a syntactical cut-elimination proof has not been shown for any of them.  In this paper, the authors formulate the logic in a system on nested sequents (i.e., trees of sequents), featuring inference rules to apply inside of such trees like a Sch\u00fctte-type formulation, and show that the system allows a straightforward syntactical cut-elimination procedure establishing at the same time a non-trivial bound on the proof-depth charaterized by the Veblen function. The co-embeddability between the system and that of Alberucci and J\u00e4ger is also proved, which therefore gives rise to a syntactical proof of cut-elimination for the system of Alberucci and J\u00e4ger as well as a non-trivial bound of the proof-depth characterized similarly. It is also noted that the method works for many variations of the logic.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1024553$6D9DD34C-AEC9-4EF1-92D7-2F4849BC6D6A","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"e3f06c5cc154fad665bbd7bfe01f3fd2207302a9","datavalue":{"value":{"entity-type":"item","numeric-id":588143,"id":"Q588143"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1024553$88A0D815-0C16-4980-BAA4-69E0E71EC1AE","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"19e8b53914fe36a939b2f687be46776db2609217","datavalue":{"value":"03B42","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1024553$A46FE87F-B3AE-4D0E-8D4C-1293A07A3595","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"74a6cec96241e450625296e63e8dd539239d7104","datavalue":{"value":"03B45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1024553$AAF7F52A-0937-4C83-8020-60306E26F44D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1024553$E2D02F18-8602-4E69-B859-C558A20ADA60","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"bc64a6b73dabafe9454a90549b917096c2cb879b","datavalue":{"value":"5565760","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1024553$7F97FE5C-1B97-45A3-A005-D2FBA5F51ABF","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e36213b5c1732724f34d421ccd475622cf5927f5","datavalue":{"value":"logic of common kowledge","type":"string"},"datatype":"string"},"type":"statement","id":"Q1024553$98E05AF7-0EF0-43F1-943D-0CC18719D6CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c1daa16a491d50927c503e32bb88ee60a8cc92e9","datavalue":{"value":"logic of common belief","type":"string"},"datatype":"string"},"type":"statement","id":"Q1024553$9649E3CE-7E8C-460B-B615-334B43F53D9C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dcfc1bc00c58245854e787073d98b7cbed7ce1ba","datavalue":{"value":"cut elimination","type":"string"},"datatype":"string"},"type":"statement","id":"Q1024553$EC92FEE4-4CE0-41F6-BEB9-6090FAD2DFD2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4368917dfeb6b4bbc805516f2452ab2d8a725b30","datavalue":{"value":"infinitary sequent system","type":"string"},"datatype":"string"},"type":"statement","id":"Q1024553$3BD02B45-3BD1-42B2-A484-3ECAE06DFACA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7703d39a27a27281175ecfee2e3e3ef8e18d9ab1","datavalue":{"value":"nested sequents","type":"string"},"datatype":"string"},"type":"statement","id":"Q1024553$8B98D502-5ECB-4E9A-A824-017525AEE52D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3edc12f7f388e61a194d25476609bec482ce1e12","datavalue":{"value":"proof-depth","type":"string"},"datatype":"string"},"type":"statement","id":"Q1024553$7A2D1236-581A-4F67-BEDF-1EA0842B665B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cd0bf1e62636d9eeae83746cb246445c3e3fd82c","datavalue":{"value":"Veblen function","type":"string"},"datatype":"string"},"type":"statement","id":"Q1024553$304F9B05-1E5A-42B0-85D7-8B68703B0D2D","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":"Q1024553$69070382-7292-4D72-8BB3-BC5B6084A669","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"57d0dc75206f21e193cb828117dc9cbf9fbe9c6b","datavalue":{"value":"https://doi.org/10.1016/j.apal.2009.01.014","type":"string"},"datatype":"url"},"type":"statement","id":"Q1024553$AC5616D1-5419-4478-8312-ED774B9DF84C","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"9e2dea8225cd106f6286576c0e085e0f4f774b7c","datavalue":{"value":"W4213095921","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1024553$1558A7E9-BBF3-4249-816B-667A5D970E6B","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"194d0bf0a6cc5352e93ae868670d4f1ac2906a84","datavalue":{"value":{"entity-type":"item","numeric-id":3498455,"id":"Q3498455"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1024553$B7CB6917-FF3C-46DA-9CA3-2D5A8255E054","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0802b92179426485912c2faef566750722ed4017","datavalue":{"value":{"entity-type":"item","numeric-id":1772772,"id":"Q1772772"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1024553$8659349B-1E70-4F0A-BE08-678DC11E9655","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6015f5a7506db6339797c5e813961394d9eedd0f","datavalue":{"value":{"entity-type":"item","numeric-id":5434494,"id":"Q5434494"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1024553$A5DEA6DD-1B0C-42B1-96EA-1442205BD946","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"74f082372987ccabc92cbd0d14c450ff1b25ffc2","datavalue":{"value":{"entity-type":"item","numeric-id":2500478,"id":"Q2500478"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1024553$9BA147EC-427E-4493-862E-28112B891582","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"65d956577b3303ebd7039744b667c611553174c8","datavalue":{"value":{"entity-type":"item","numeric-id":4982123,"id":"Q4982123"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1024553$7BDECD6E-D0AB-4646-A2DA-B4CCA7CFE8BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"59c29138920afdd872cf6e3791feb17594655142","datavalue":{"value":{"entity-type":"item","numeric-id":3509048,"id":"Q3509048"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1024553$FE2FC551-6F8F-43B0-B91C-9D2EF52001D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2990e15db3ec1299bacd39e760b2d345098c103a","datavalue":{"value":{"entity-type":"item","numeric-id":4845472,"id":"Q4845472"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1024553$9BFD47F3-6221-47EE-BCEA-774A362E1102","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d2ff84a380859792f98a71b73007569735b0f24f","datavalue":{"value":{"entity-type":"item","numeric-id":5277766,"id":"Q5277766"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1024553$9F80BE4C-1A71-4DA5-9C68-12BAA9F76B49","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"07b4a5481d2ba20db96403c8a94b2eeed3801b42","datavalue":{"value":{"entity-type":"item","numeric-id":3477999,"id":"Q3477999"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1024553$3EADC569-1570-4E9B-9292-05B676F00917","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fc207fadc6ba9564432e7709593a9b3cf923d465","datavalue":{"value":{"entity-type":"item","numeric-id":2475436,"id":"Q2475436"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1024553$8A404E97-11A1-4823-A93B-E87E7203DEA1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"840cdf0fd2fc7639009b50125648d2c88152a633","datavalue":{"value":{"entity-type":"item","numeric-id":1317905,"id":"Q1317905"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1024553$B789E4F1-7666-4F46-984C-C3CF2CF83CD1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a52ffcc834194620943ec4a87fc97578b45281e4","datavalue":{"value":{"entity-type":"item","numeric-id":2506830,"id":"Q2506830"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1024553$ABA86944-F0D9-447D-B997-B7086C5E8EEB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"174e3f2701a2bacd196e2d244539c0776079d382","datavalue":{"value":{"entity-type":"item","numeric-id":4858037,"id":"Q4858037"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1024553$FAD382EA-C6A5-4620-A4C5-80A9B896AD42","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5c394edfe97f2771d3f458e785c6ac06b6755082","datavalue":{"value":{"entity-type":"item","numeric-id":3358711,"id":"Q3358711"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1024553$E81086C6-863C-4E15-B238-B4FD2D4A42BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3798ecd2352848fc7f05ce377ca3bb7ca030a458","datavalue":{"value":{"entity-type":"item","numeric-id":1801306,"id":"Q1801306"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1024553$B8D30884-40A5-4F07-B62B-F8E909DF938F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cec940eee0477184e354b8959d22d2df44a783c7","datavalue":{"value":{"entity-type":"item","numeric-id":4215633,"id":"Q4215633"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1024553$D29E504C-70D8-4C82-9393-58FCC989416C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"203318c557c82294d1a13a7b0ee8923a35f083bc","datavalue":{"value":{"entity-type":"item","numeric-id":2648344,"id":"Q2648344"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1024553$7C85D8B9-6903-4789-99CD-F14B3EA3D15C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b7c3e6815cd921fc7767de9db6783bde242a686c","datavalue":{"value":{"entity-type":"item","numeric-id":4143279,"id":"Q4143279"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1024553$1F11D0B2-022B-47A6-ACB9-EBEA88E8762C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7cd156e93f1e8a800af5e3f23078f66edcdefe75","datavalue":{"value":{"entity-type":"item","numeric-id":5483015,"id":"Q5483015"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1024553$74E6A09A-2C2B-4B61-8CED-0E253AE18110","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"df112f62a43a9d44047fd2e019422f51de9dc089","datavalue":{"value":{"entity-type":"item","numeric-id":4465172,"id":"Q4465172"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1024553$F2EF6DF9-5718-4312-A9ED-C8C62EF5B61C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"571c77287950a1b1254eff4765ace8b0315994a4","datavalue":{"value":"10.1016/J.APAL.2009.01.014","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1024553$E05E5A99-B730-48DD-B67A-647FF6819D0D","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"361718c2db0e951115b7ee4ebf37bb3124a74e6d","datavalue":{"value":{"entity-type":"item","numeric-id":4982123,"id":"Q4982123"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1941f9628283c51315ec08be5244fcc3041bf4a1","datavalue":{"value":{"amount":"+0.9683245420455932","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":"Q1024553$C58AF794-6F63-48E5-B26B-F651A2B30E81","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0c00f23ba6f6420028143d5ce2f8dfceb40ce498","datavalue":{"value":{"entity-type":"item","numeric-id":2475436,"id":"Q2475436"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a8864b444ba4fd253177b1ca449fd3f98ca69333","datavalue":{"value":{"amount":"+0.8434219360351562","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":"Q1024553$7765B323-4207-47D4-AA5D-F0D4ECCBC03C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0c26b0bafd973c29839586c72c8bf08f8df0a161","datavalue":{"value":{"entity-type":"item","numeric-id":834716,"id":"Q834716"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a72fee218212d4fff09c1a73d9658a22d5022f8e","datavalue":{"value":{"amount":"+0.8403990864753723","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":"Q1024553$1666DF2B-2AF3-4129-8003-080346ED84C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"641fd0aba4498094ed05f03caeedeb83cfe0551d","datavalue":{"value":{"entity-type":"item","numeric-id":2973444,"id":"Q2973444"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f00c7ed3a13ef49e877a6ba1f41dac3a45cbcd57","datavalue":{"value":{"amount":"+0.8379678130149841","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":"Q1024553$E485A046-806D-486B-9B34-41AF92029E4C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0136ba771022afe1a1a65d2472f604d60be11eb2","datavalue":{"value":{"entity-type":"item","numeric-id":3299587,"id":"Q3299587"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a6eac7552847a8ee8ebcca63f667ade566c70e4b","datavalue":{"value":{"amount":"+0.835847795009613","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":"Q1024553$032E2935-81CA-4E9D-A0A6-8A12C6B8F8C7","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Syntactic cut-elimination for common knowledge","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Syntactic_cut-elimination_for_common_knowledge"}}}}}