{"entities":{"Q690929":{"pageid":692778,"ns":120,"title":"Item:Q690929","lastrevid":63526494,"modified":"2026-04-11T13:46:29Z","type":"item","id":"Q690929","labels":{"en":{"language":"en","value":"Kripke semantics and proof systems for combining intuitionistic logic and classical logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6111172"}},"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":"Q690929$1F4928C6-5497-44F2-91F3-C83D2448A5FE","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"933a7886215e53e3f0ce225c52b1d94dbaff463f","datavalue":{"value":{"text":"Kripke semantics and proof systems for combining intuitionistic logic and classical logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q690929$38EB5DAB-8649-443B-8EE5-54B5FF46953B","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"afcfddb5869e7629f49238995b621ba3275dfc85","datavalue":{"value":"1276.03025","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q690929$C0941BB6-307F-4429-960E-0289AE6666C5","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"c9ce3e80bb1a16307d22ed97af34d804e7fedd0c","datavalue":{"value":{"entity-type":"item","numeric-id":639670,"id":"Q639670"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q690929$A74D87C5-58F6-4C84-8796-0707CA994D06","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"2479aee847d640d3090b268957bfaa9b03ce27ad","datavalue":{"value":{"entity-type":"item","numeric-id":1102281,"id":"Q1102281"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q690929$B1421AE7-7A18-4811-A6C5-7860A1D6D135","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":"Q690929$6D422C07-7DBB-4E24-ABC7-43514C7CA042","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"dd1dd78b610951b080ce7917880823f8267fcfa0","datavalue":{"value":{"time":"+2012-11-29T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q690929$9A9CA8C4-AEF3-4368-AC06-092626176046","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"e12850b030387274eb9f1bc418dbc76efbc820c7","datavalue":{"value":"The basic question discussed here is whether the critical intuitionistic connectives of implication and universal quantification can retain their strength when combined with classical connectives. In order to combine intuitionistic and classical logic the authors introduce a first-order predicate logic called polarized intuitionistic logic (PIL) based on a distinction between two dual polarities defined model-theoretically by means of the Kripke-type semantics for this logic. The proof-theoretical treatment of PIL includes two proof systems: the first one extending Gentzen's sequent calculus for intuitionistic logic, and the second one based on a semantic tableau extending Dragalin's multiple-conclusion sequent calculus for intuitionistic logic. The corresponding soundness and completeness results are obtained having as consequence the admissibility of the cut rule. Various double-negation translations, dual-intuitionistic logic, linear logic, PIL etc. are discussed in the final part of the paper.","type":"string"},"datatype":"string"},"type":"statement","id":"Q690929$8148378B-E270-45C3-86A5-EC0EF8E4E398","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"1281dd6b9c4f62144bc68cb09edbb6fe30760a8f","datavalue":{"value":"03B62","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q690929$5E5F8939-F409-4E1C-9CEB-76E579BCAFD6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c06e0874e30722381d620ef69fb36c407a01cb04","datavalue":{"value":"03B10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q690929$F299A08E-42B6-497E-8559-F41725E5DFA4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"2337f934f367559a8ee0c48540aa4d52d0fa385a","datavalue":{"value":"03B20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q690929$B298CFFC-59A9-4656-90B4-8D41B2FE9199","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f73d157ce9374047ebf746e6996382fc4dfda34d","datavalue":{"value":"03F52","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q690929$4624C4FB-68B6-4B47-8A29-E3AA17D95070","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"f8706d06720db526543eca086c00f923a062570f","datavalue":{"value":"6111172","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q690929$7EB2B162-B0CB-4078-BB93-6DFAAC817B7E","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9ffd3928aa1fd818bc1a8806528172e266ac8bcc","datavalue":{"value":"classical logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q690929$36A9862C-DB33-4961-ACE7-75B44471BA62","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d450f4b3083fe34d24db452ee74b92106c27a96e","datavalue":{"value":"intuitionistic logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q690929$74E5B4C8-962F-43BA-8FFF-4B7968306A57","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0bd13a4bc42b56535792b0eb0ab04c551439e3d3","datavalue":{"value":"hybrid Kripke models","type":"string"},"datatype":"string"},"type":"statement","id":"Q690929$F71ABE46-B3C0-417F-A9F4-E3293AC3A33B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fe51228e17b836f3520db7bc0de40e5086eebee3","datavalue":{"value":"soundness","type":"string"},"datatype":"string"},"type":"statement","id":"Q690929$EFFADD53-D869-4AEF-9A64-A9ACC5FBF24B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f6816fdf79dd11ac09d9af4886c02baab03d2cf9","datavalue":{"value":"completeness","type":"string"},"datatype":"string"},"type":"statement","id":"Q690929$81639770-F65B-433E-9E26-EB684E0C1ED3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"34cead95aa95ce302403dfa3e12afb1f68893c3e","datavalue":{"value":"polarized logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q690929$9A4840B7-B3D0-41A2-A0BE-C1407B1D5CE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2c7d4aa0d3cf1745112ae7d594a2a5578f4e767f","datavalue":{"value":"sequent calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q690929$6DF82578-F54D-4C2B-8C41-F66814D0B4C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5be9b1656f4cb1890f743f99de7eba7a563dc33c","datavalue":{"value":"combining logics","type":"string"},"datatype":"string"},"type":"statement","id":"Q690929$F1ECDA97-4564-48E7-88D4-D0A50E426153","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"2b87c2901b1d9462aa6fffa26502c8ee861836b0","datavalue":{"value":{"entity-type":"item","numeric-id":1062052,"id":"Q1062052"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q690929$2CEA8594-97B1-406F-BCC2-35817A44B2EB","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":"Q690929$D82AA0AB-6C0F-4013-BC44-A7166A63EDCE","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"df254f78d1ce295768e0badf3c2b140a9f0bcca9","datavalue":{"value":"https://doi.org/10.1016/j.apal.2012.09.005","type":"string"},"datatype":"url"},"type":"statement","id":"Q690929$0B004B91-5BB9-4442-A4A3-2EEB528E274E","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"8f901ce174108e9fb77edc1823d1135dce8d8239","datavalue":{"value":"W2009938424","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q690929$9EDB5EA3-A42B-4D83-89E1-BB2E939D6A9D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"e9c4f26772472e294a4623048f7f7ec2440ae79c","datavalue":{"value":"10.1016/J.APAL.2012.09.005","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q690929$89B71C18-2B46-42A4-8C5D-64711436BE43","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8fccb268e4fe7dedf7c0a4de16c652c5b4b6681f","datavalue":{"value":{"entity-type":"item","numeric-id":2021569,"id":"Q2021569"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5dc18ea0e2c07873e9fb9ce6e6702c3a2b257146","datavalue":{"value":{"amount":"+0.91987395","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q690929$3446520E-AE40-4148-A61D-FB56AAA34CEA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"29433b34c53c4b5ea9158a769a116b86a672a7c7","datavalue":{"value":{"entity-type":"item","numeric-id":4635871,"id":"Q4635871"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bb238057e4f79edced634b2a8978c19c44646d0e","datavalue":{"value":{"amount":"+0.918066","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q690929$29F8CC90-644B-4F45-B969-60722525BFA0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4d5700e2f175503e455a8e2ab59771b45018fa71","datavalue":{"value":{"entity-type":"item","numeric-id":4805536,"id":"Q4805536"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"382019ee6e0834209daa31df5949be1aa6411707","datavalue":{"value":{"amount":"+0.9028617","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q690929$5A2AFFFD-45D4-416A-BAC1-17AB3BA14BE9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"01bed03b98e104006f14bf10f3656df34d2016be","datavalue":{"value":{"entity-type":"item","numeric-id":3153244,"id":"Q3153244"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"382019ee6e0834209daa31df5949be1aa6411707","datavalue":{"value":{"amount":"+0.9028617","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q690929$89CF9C92-1D17-46F3-AD34-96C506741EFA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"36ecc4cf8da646662c9091b4b2a1e2ea8db47696","datavalue":{"value":{"entity-type":"item","numeric-id":3016126,"id":"Q3016126"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9619b1aa63e52dc652a797e03d7a5f4ada1b5b05","datavalue":{"value":{"amount":"+0.90013444","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q690929$AC1D58BA-4168-4411-830E-6A32B297566C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9b958373e2438e27311212a3abfee89b629d882e","datavalue":{"value":{"entity-type":"item","numeric-id":1882403,"id":"Q1882403"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1642b9475c015b2052477ee622c4bf07c873e6f2","datavalue":{"value":{"amount":"+0.8988073","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q690929$4641FE94-7B81-438E-8BC8-6EE6DFEFA200","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ba69c8f00c6454f7ba9238a2baf0998162e92342","datavalue":{"value":{"entity-type":"item","numeric-id":2231694,"id":"Q2231694"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1929434662fa589f16119df01784d012752ef7b5","datavalue":{"value":{"amount":"+0.89650905","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q690929$4730C1E7-9E96-47AB-9CD7-B88552160368","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"564c547bd56ee78666c46b25fbf6a1777021d430","datavalue":{"value":{"entity-type":"item","numeric-id":636316,"id":"Q636316"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"53b639db313702dd9c02f58d2a17bdf570f67344","datavalue":{"value":{"amount":"+0.89561874","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q690929$3FB06D07-E7CF-4913-ACE6-657AF02F74F4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e4e8498becd050c80f2ebd77c586d4f37d5274b4","datavalue":{"value":{"entity-type":"item","numeric-id":851196,"id":"Q851196"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1780483d17bcaaed3544bf21cb0154e123227b02","datavalue":{"value":{"amount":"+0.89537615","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q690929$E112A013-B2A7-4D11-A7CC-EC018682B2E6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2992da8d0fed1ab473691d85f466f4e7363920ea","datavalue":{"value":{"entity-type":"item","numeric-id":3309811,"id":"Q3309811"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a4abf50f0fbf8d2d0bb28799ca2ece76c7435d6b","datavalue":{"value":{"amount":"+0.893347","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q690929$28B6ED11-710F-423B-8DBC-2F8F414A93D5","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Kripke semantics and proof systems for combining intuitionistic logic and classical logic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Kripke_semantics_and_proof_systems_for_combining_intuitionistic_logic_and_classical_logic"}}}}}