{"entities":{"Q2804339":{"pageid":2815077,"ns":120,"title":"Item:Q2804339","lastrevid":52518617,"modified":"2026-01-22T20:54:49Z","type":"item","id":"Q2804339","labels":{"en":{"language":"en","value":"Binding modalities"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6575049"}},"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":"Q2804339$FF0CAA72-9A3A-4694-AE69-3BF0D035A870","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a23bd8ffea1d3dedcfb6be580c0abd42d346f814","datavalue":{"value":{"text":"Binding modalities","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2804339$BE56963C-77C4-4D77-BC6E-E3A642213B81","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c9d3ff3d0e0cd488b0e8bcf43ba0f03dc3808d77","datavalue":{"value":"1352.03027","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2804339$F4E3E63C-8909-4138-8924-3C8081D7A0CA","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"65d92ec75d628fee5ec7d8ff1596e77d100222be","datavalue":{"value":{"entity-type":"item","numeric-id":2804338,"id":"Q2804338"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2804339$AC8FFA0A-11E7-4223-AFF4-94E6EAABCFE9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"3f5711a22c90a25acfa5e838b5972ab6cd5c8785","datavalue":{"value":{"entity-type":"item","numeric-id":1317985,"id":"Q1317985"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2804339$4BE502BD-9C94-494F-A6EC-6A28DCFF944C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"023d69fc066169597fa101da2e0c4ab7a589a584","datavalue":{"value":{"time":"+2016-04-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":"Q2804339$A3203551-1609-4B0F-B97E-2F5BD3D53C04","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"af4ced2f797e75c31dd69273559e6fab52c76c32","datavalue":{"value":"https://semanticscholar.org/paper/05d59ba283103dfabd3902e815a5cbc27fbcf6a9","type":"string"},"datatype":"url"},"type":"statement","id":"Q2804339$0150B5D6-629F-4E9E-B7CE-55E7AE2F9FB8","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"74a6cec96241e450625296e63e8dd539239d7104","datavalue":{"value":"03B45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2804339$619BDFC3-B065-48D5-B5D9-BBE5CF3DB5C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b638c7935436ccffba7a737e2b57436cbbd2533c","datavalue":{"value":"03F45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2804339$4D1F3C92-A17D-432C-959F-4F4585226FA1","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"4de15166155a1c11b47fa45e5ca3d517d16dbbd0","datavalue":{"value":"6575049","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2804339$AF4037A1-625D-44EA-B7B6-54D4D93AD33C","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f1dda010537b7b36bd45151721146f720815706e","datavalue":{"value":"modal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2804339$70883FE8-2416-44FB-BE35-391A0AD9AF95","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7e2e21a984526b8024b04acd04fd80cbaaf58f4b","datavalue":{"value":"logic of proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q2804339$629314E9-258C-46B3-B73E-0E9BB75EB44F","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":"Q2804339$627B0420-127E-4894-8A2B-603006C3ABF1","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"607b2e1dfde92ddda0074687709452dd9b8d360d","datavalue":{"value":"W4245485865","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2804339$FFA81B5B-EB10-45C3-BBBF-BEF5B82DCB86","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"3bc6fde2e95902419f6d876ff55ba2458820006c","datavalue":{"value":"10.1093/LOGCOM/EXT017","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2804339$10AC7289-A99D-43FB-AE8C-6F8E688BF4A5","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"4e284497c1d95ed03031b32369f55bf404c9e002","datavalue":{"value":{"entity-type":"item","numeric-id":6768690,"id":"Q6768690"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2804339$772C03AA-F761-40A6-ABB3-73E81F32A0BE","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"20199b940525a416f073ea15768c1ee8b52733ba","datavalue":{"value":"The paper studies a modal logic \\(\\mathsf{FOS4}^*\\) with binding modalities. If \\(X\\) denotes a finite set of individual variables and \\(y\\) is an individual variable, then \\(Xy\\) stands for \\(X \\cup \\{y\\}\\) and it is assumed that \\(y \\notin X\\). The logic \\(\\mathsf{FOS4}^*\\) is axiomatized by the following schemas, where \\(A\\) and \\(B\\) are formulas, \\(X\\) is a set of individual variables, and \\(y\\) is an individual variable: NEWLINE\\begin{itemize}NEWLINE\\item[(A0)] classical axiom schemas of first-order logic NEWLINE\\item[(A1)] \\(\\square_{Xy} A \\to \\square_XA\\), \\(y \\notin\\mathrm{FVar}(A)\\) \\item[(A2)] \\(\\square_X A \\to \\square_{Xy} A\\) \\item[(A3)] \\(\\square_X A \\to\\square_X \\forall{x}A\\), \\(x \\notin X\\) NEWLINE\\item[(B1)] \\(\\square_X (A \\to B) \\to (\\square_X A \\to \\square_X B)\\) NEWLINE\\item[(B2)] \\(\\square_X A \\to A\\). NEWLINE\\end{itemize}NEWLINEInference rules: NEWLINE\\begin{itemize}NEWLINE\\item[(R1)] \\(A,A\\to B \\Rightarrow \\;\\vdash \\;B\\quad \\text{modus ponens}\\) NEWLINE\\item[(R2)] \\(A \\Rightarrow \\;\\vdash \\forall{x}A\\quad \\text{generalization}\\) NEWLINE\\item[(R3)] \\(A \\Rightarrow \\;\\vdash \\square_\\emptyset A\\quad \\text{necessitation}\\).NEWLINE\\end{itemize} NEWLINEA sequent calculus for \\(\\mathsf{FOS4}^*\\) is constructed in Section 3, and the cut-elimination theorem is proven. The connections between \\(\\mathsf{FOS4}^*\\) and \\(\\mathsf{FOS4}\\) -- first order \\(\\mathsf{S4}\\) -- are studied in Section 4. In particular, if \\(A^*\\) is a formula obtained from a given \\(\\mathsf{FOS4}\\)-formula \\(A\\) by replacing all occurrences of subformulas of \\(A\\) of the form \\(\\square B\\) by \\(\\square_X B\\), where \\(X = \\mathrm{FVar}(B)\\), we have NEWLINE\\[NEWLINE\\mathsf{FOS4} \\vdash A \\text{ if and only if } \\mathsf{FOS4}^* \\vdash A^*.NEWLINE\\]NEWLINE A complete Kripke semantic for \\(\\mathsf{FOS4}^*\\) is described in Section 5. And Section 6 is dedicated to proof that every formula \\(A\\) derived in \\(\\mathsf{FOS4}^*\\) has a normal realization \\(A^r\\) and \\(\\mathsf{FOLP} \\vdash A^r\\), where \\(\\mathsf{FOLP}\\) is the first order logic of proofs.","type":"string"},"datatype":"string"},"type":"statement","id":"Q2804339$173CE721-9872-49F8-B946-44663F84CF8E","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"42952f847986d97f96b12a6dfd7da21342953d87","datavalue":{"value":{"entity-type":"item","numeric-id":454374,"id":"Q454374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2804339$FA6D1BEF-7C71-430B-AB69-EA7B0F175563","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7187941eeaeafc51dc91ac752c0566a699290b3a","datavalue":{"value":{"entity-type":"item","numeric-id":1115410,"id":"Q1115410"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"44d100cb09a8cbaf4fab817b965cedb13eb560cb","datavalue":{"value":{"amount":"+0.7527863383293152","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":"Q2804339$618AA4D9-3461-4536-B412-D9C2BF3F002E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b108a6b167800fa57292324f80188fa967063337","datavalue":{"value":{"entity-type":"item","numeric-id":4430390,"id":"Q4430390"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4bb41c9e574c5b08fea649c0da1c9cfac19ec7a5","datavalue":{"value":{"amount":"+0.7327050566673279","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":"Q2804339$7FB8E44C-18DB-4B03-A9CD-D618CEABE26A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5ddc51bc6e27a4569a17968485e70f6d1bb0171b","datavalue":{"value":{"entity-type":"item","numeric-id":1870904,"id":"Q1870904"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c83ae25e932e707968668f739660be3fe7d4e82a","datavalue":{"value":{"amount":"+0.7322911024093628","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":"Q2804339$C9C53E55-2ECF-48AB-B7E4-3B830FC4B9E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9ac8fc95e9314122a53059e4d5b70a27d8e08803","datavalue":{"value":{"entity-type":"item","numeric-id":3777990,"id":"Q3777990"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d3647db3f73b9df3376c6f658ec9dff8e8a2997e","datavalue":{"value":{"amount":"+0.7093101143836975","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":"Q2804339$BBD85A01-5B28-4E10-99DF-AF8AC81620B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"69d87b5e218d98e96fbe330a89f8363e0ddcc405","datavalue":{"value":{"entity-type":"item","numeric-id":5351988,"id":"Q5351988"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9e0426bda197284f1bd26a4ed79468f3759a69aa","datavalue":{"value":{"amount":"+0.6996271014213562","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":"Q2804339$88568738-7006-4A41-AA0F-5EECAA2A64AD","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2804339","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2804339"}}}}}