{"entities":{"Q685055":{"pageid":686904,"ns":120,"title":"Item:Q685055","lastrevid":42640647,"modified":"2025-07-07T14:45:19Z","type":"item","id":"Q685055","labels":{"en":{"language":"en","value":"Intuitionistic validity in \\(T\\)-normal Kripke structures"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 416872"}},"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":"Q685055$E5DD9290-0305-4CB0-BCCD-9595F1251818","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"21517ef77b22e4537a80398997bb005ef21330bf","datavalue":{"value":{"text":"Intuitionistic validity in \\(T\\)-normal Kripke structures","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q685055$731117E3-114D-4AA5-9CD6-F857B55D44EA","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ed5f6194d108e074c5f1ac48db4da7199ae4b4b6","datavalue":{"value":"0802.03006","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q685055$53F11F86-665E-4129-8C20-697F3CF23D88","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"8ae74bce38a0940f921376328902794a81d22a2e","datavalue":{"value":"10.1016/0168-0072(93)90091-Q","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q685055$94C489D4-9F66-4AE5-B78E-6FC5B1383D42","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"556b5f897f5d545f04c26b56d4624f5cc4b2661a","datavalue":{"value":{"entity-type":"item","numeric-id":195654,"id":"Q195654"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q685055$92275671-F5A0-4F43-B740-1BF9A88DED52","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":"Q685055$3810CAA8-749A-4F30-BF06-46CACA4DA92C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6918393775fb1c8826438f5277bce44cf6f24c36","datavalue":{"value":{"time":"+1993-09-22T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q685055$A300B79E-4FA6-4491-9263-162B39242731","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"3b043501b5b9dc92f37421632a54765f840c7ff8","datavalue":{"value":"Given any classical first-order theory \\(T\\), the author considers the set \\({\\mathcal H} T\\) of all first-order sentences that are valid in every \\(T\\)- normal Kripke structure. A Kripke structure may be considered as a partially ordered set of classical structures and it is called \\(T\\)-normal iff each of these classical structures is a classical model of \\(T\\). The author's main motivation for studying such structures is his wish to extend model-theoretic techniques from classical logic to intuitionistic logic. He gives a very nice and surprising characterization of \\({\\mathcal H} T\\): it is the set of all sentences that may be proved by intuitionistic logic from formulas of the form \\(\\theta^ \\phi \\to \\phi\\) where \\(\\theta\\) is a semipositive formula (that is, each subformula of the form \\(\\theta_ 1\\to \\theta_ 2\\) has \\(\\theta_ 1\\) atomic; observe that \\(\\neg\\psi\\) abbreviates \\(\\psi\\to \\perp)\\), \\(\\neg\\theta\\) follows by classical logic from \\(T\\), and \\(\\theta^ \\phi\\) is obtained from \\(\\theta\\) by replacing each atomic subformula \\(\\chi\\) of \\(\\theta\\) by \\(\\chi\\vee \\phi\\). In fact, \\(\\theta^ \\phi\\) is H. Friedman's \\(\\phi\\)-translation of \\(\\theta\\) [see \\textit{H. Friedman}, Lect. Notes Math. 669, 21-27 (1978; Zbl 0396.03045)]. As a special case the author considers Peano arithmetic PA. He shows that \\({\\mathcal H}\\text{PA}\\) proves (intuitionistically) \\(\\Sigma_ 1^ 0\\)-induction, and, using a very nice argument, that \\({\\mathcal H}\\text{PA}\\) does not prove \\(\\Pi_ 1^ 0\\)-induction: \\({\\mathcal H}\\text{PA}\\) is a proper subtheory of Heyting arithmetic HA. The author concludes his paper with some questions. I have one more to ask: is it possible to make sense of the notion of a \\(T\\)-normal Kripke structure from an intuitionistic point of view, that is, if one uses an intuitionistic metalanguage?","type":"string"},"datatype":"string"},"type":"statement","id":"Q685055$D11EED7A-D6D6-46AA-B135-9512021210DB","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"2337f934f367559a8ee0c48540aa4d52d0fa385a","datavalue":{"value":"03B20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q685055$2C360BF6-7E43-4AC3-BFD2-758F0DB404B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c15287dbb142f8dc10ab92a91b8457ac3c169cd3","datavalue":{"value":"03F30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q685055$D463D9C1-EB48-41B5-8579-F2786B7F2ABF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"8612eb3fa5372f4e40168b827ed17a01cee8d8f6","datavalue":{"value":"03F50","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q685055$70F24B40-9801-4919-8B95-DF6FED9D1D60","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ed0e9d16aabdfc4de2754948a872b6ceb30bba56","datavalue":{"value":"03C90","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q685055$D1ED5AEF-09C4-414D-8670-61F7E22774EC","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"62dbfe94f8fbf25e33262a0d2e6a30116b62b158","datavalue":{"value":"416872","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q685055$4000F931-5FF3-4C79-8E1E-CED27995C129","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1103c6be7b4d9722b4eccbf2347aba04abe91478","datavalue":{"value":"\\(T\\)-normal Kripke structure","type":"string"},"datatype":"string"},"type":"statement","id":"Q685055$5DA7C386-6659-4714-AFDC-FD542B5214D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d450f4b3083fe34d24db452ee74b92106c27a96e","datavalue":{"value":"intuitionistic logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q685055$21CE6CC6-9B89-465B-88DD-1463752D98A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4179e835513e3ecb4e88002bdf28512e160e0b9f","datavalue":{"value":"Friedman's \\(\\phi\\)- translation","type":"string"},"datatype":"string"},"type":"statement","id":"Q685055$A0E48EF9-46B4-469E-A158-9DA5AFE2C230","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7090cb2b2cefa03cee6b50a67ca057c086ad0f00","datavalue":{"value":"Peano arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q685055$65D45BA6-778F-4F3C-96E7-6D8F42CAA1A7","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"6d31cfcd4872ca33402e7ff9adb26d2a568fa6e6","datavalue":{"value":{"entity-type":"item","numeric-id":185815,"id":"Q185815"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q685055$86EDB094-ABBB-4EDB-8A91-CA5D1FE195CB","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":"Q685055$679ED509-C507-430B-A5C0-9048A634F477","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"4489775ac4fe4693cafe9f4393b82cee4cc4e5dc","datavalue":{"value":{"entity-type":"item","numeric-id":4035302,"id":"Q4035302"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q685055$B2B2859E-D3DC-4BFC-99DB-A6A975D1CC61","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"20078d69304e2df97ca3f40332c8d92086a6b541","datavalue":{"value":{"entity-type":"item","numeric-id":4179016,"id":"Q4179016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q685055$7D239225-A687-4662-8F27-C59FD8FE6A1F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2358a93286be8f533ed707b97f4163c56085c86c","datavalue":{"value":{"entity-type":"item","numeric-id":3481670,"id":"Q3481670"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q685055$EF727139-6917-4556-9A87-AA7445585384","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2002e9228b023d08f49489031907fa50fb1b3491","datavalue":{"value":{"entity-type":"item","numeric-id":1188500,"id":"Q1188500"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q685055$4D4AB368-70E5-472C-A1A2-17248084F5BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3166a1df231f17c0eace0ec4a3cd14533d6a0c5e","datavalue":{"value":{"entity-type":"item","numeric-id":1095140,"id":"Q1095140"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q685055$D6DD8915-4041-490A-A4BC-EAE062725D3C","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"3334660ca22c01e310aade43eb890d2251e3049a","datavalue":{"value":"https://doi.org/10.1016/0168-0072(93)90091-q","type":"string"},"datatype":"url"},"type":"statement","id":"Q685055$ED67005C-BFA4-4B70-9715-67B83B478FFF","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"931cd2b6e2ff736d1121fa62cfcdf343579ad35e","datavalue":{"value":"W2092214433","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q685055$21C3064D-1B87-4234-98B6-8DD2C06216BB","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9ea6babad674bebc1e4d549a3a4a30547d9ced44","datavalue":{"value":{"entity-type":"item","numeric-id":5202656,"id":"Q5202656"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"420d65c164960352846e33fb3f94533fa61c9ebc","datavalue":{"value":{"amount":"+0.87465715","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q685055$306DC723-4C17-4075-8555-DECDD6094411","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"30b12eb0fb3501952deefc2ba7e19d5d80ee1f0c","datavalue":{"value":{"entity-type":"item","numeric-id":1412839,"id":"Q1412839"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"947b6dff9491dd94b9f9c1233da1bb3d9820dc23","datavalue":{"value":{"amount":"+0.87256926","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q685055$A026F389-1EF2-4337-880B-6DCA815D4BB9","rank":"normal"},{"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":"4cd4a8d08fc814e90bdc13a276daf31e2df95da7","datavalue":{"value":{"amount":"+0.8712557","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q685055$A8B6ED81-BD11-4264-96EF-8454E867BD56","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8498276b0ae6a2bdc554445ff25a6b25b5011339","datavalue":{"value":{"entity-type":"item","numeric-id":3027002,"id":"Q3027002"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c68adc64019a0126baa08abeeafa2ca347ab413b","datavalue":{"value":{"amount":"+0.87063026","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q685055$E108E9A7-A501-41A3-BAFE-D121A93DCEE1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0108300adc6ece2b5ea582a3150c11ec47889494","datavalue":{"value":{"entity-type":"item","numeric-id":1295382,"id":"Q1295382"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cbc1284ae7dfa1622f2da44e008795e51f7cc087","datavalue":{"value":{"amount":"+0.87030894","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q685055$1E29BC79-3294-4C8B-A5C7-56318CF97F6A","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":"5243d2c064fcb5d14e97de63d3cbe9258bc5344d","datavalue":{"value":{"amount":"+0.86795634","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q685055$05EB02AB-E1B3-4452-B96B-1F4E05B4F6DC","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":"5243d2c064fcb5d14e97de63d3cbe9258bc5344d","datavalue":{"value":{"amount":"+0.86795634","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q685055$C95A9551-0CAB-4827-B6B8-1A356769C782","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9df0f08a4c5eb2cfc2831660db6d3739103dc08e","datavalue":{"value":{"entity-type":"item","numeric-id":5603863,"id":"Q5603863"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"470228184004e377bfa05eb3926fdc38cdd4a96b","datavalue":{"value":{"amount":"+0.8662077","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q685055$8C29CF0F-B712-464A-94FF-9EEBC2E421C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"89ba66a2ee9ac35b0e9bed1c531eb349a004ea69","datavalue":{"value":{"entity-type":"item","numeric-id":4857856,"id":"Q4857856"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"99dd8bbc34544e2a0c04d09c559eb5a2c52c258c","datavalue":{"value":{"amount":"+0.86373234","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q685055$515E86F1-D1F2-45C1-8B4B-F95354575508","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f0d25d6b8e208eae81925c9214cb67470d4ad69d","datavalue":{"value":{"entity-type":"item","numeric-id":2785696,"id":"Q2785696"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bf0ca06a2d0a234faa101764cf095667ca32edc4","datavalue":{"value":{"amount":"+0.8632949","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q685055$F8E8C07C-0B95-4E74-A6C2-E31AF19D2D71","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:685055","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:685055"}}}}}