{"entities":{"Q1422103":{"pageid":1432843,"ns":120,"title":"Item:Q1422103","lastrevid":68797578,"modified":"2026-04-13T02:07:16Z","type":"item","id":"Q1422103","labels":{"en":{"language":"en","value":"Reverse mathematics and completeness theorems for intuitionistic logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 2038296"}},"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":"Q1422103$97C47085-D0A1-4576-9CD2-7BD72C95B1D9","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"8fc5af23b7e1bab129bef528c4b5950380381f89","datavalue":{"value":{"text":"Reverse mathematics and completeness theorems for intuitionistic logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1422103$5A607662-1C29-450B-ABCC-824CAA286DCB","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"4b6b318530b6f234e9a0252b7ffb49435cdc5ec9","datavalue":{"value":"1036.03008","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1422103$766AD1C6-B159-4697-9F51-8FCA55EE786B","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"c6bb43a942f467a7751dad22d578372df9f5bcd8","datavalue":{"value":{"entity-type":"item","numeric-id":527336,"id":"Q527336"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1422103$B3C473D3-F3AE-4EF5-9D8C-BBBB713F734C","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"6325d9f59cde8ebbdb24a9f950cab3fcef3decf6","datavalue":{"value":{"entity-type":"item","numeric-id":190248,"id":"Q190248"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1422103$BC1CC13A-3FD4-4C6A-AC9D-15837798E9F9","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"4771f8a4f0386977402ebf0335c556de7718d136","datavalue":{"value":{"time":"+2004-02-04T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1422103$DB5896CC-15D9-4DD1-B93A-D108856365BD","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"76d9363a894a8fe432385ab9490cc188684bd9ed","datavalue":{"value":"This article investigates the mathematical logic of intuitionistic propositional and predicate calculi using the framework of reverse mathematics [\\textit{S. G. Simpson}, Subsystems of second order arithmetic, Berlin: Springer (1999; Zbl 0909.03048)]. Working in RCA\\(_0\\), the author shows that a version of the strong completeness theorem asserting the existence of a particular sort of Kripke model is equivalent to ACA\\(_0\\). The paper includes a proof that the saturation lemma for intuitionistic predicate logic is equivalent to WKL\\(_0\\). These results can also be found in \\S{3.2} of the author's thesis [Model-theoretic studies on subsystems of second order arithmetic, Tohoku Mathematical Publications. 17. Sendai: Tohoku Univ. (2000; Zbl 0964.03059)].","type":"string"},"datatype":"string"},"type":"statement","id":"Q1422103$8DEFDD62-0C40-48FF-B9F0-613604BB76B9","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"2337f934f367559a8ee0c48540aa4d52d0fa385a","datavalue":{"value":"03B20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1422103$4536DDE8-A1BE-4E79-9ABD-BA8D6C9C0D77","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"13841f0b96793f178ce9a7dcac9f232220625aee","datavalue":{"value":"03B30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1422103$95D6A759-45F3-4BC9-8F92-69B67DF3BE5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"4cb4544bfd0397cd4a315ee326499c372f013de5","datavalue":{"value":"03F35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1422103$B2292EDE-36BE-45AA-A4FE-1845883A22B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"3068729a394ad5bf58a1a3e5b5d24254d962e1a7","datavalue":{"value":"03F55","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1422103$9E43C9ED-AE5B-4716-8280-6A96EBCDA7E7","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"b786a44fe61172c6d9ecefd4aca1ab26a6c6a473","datavalue":{"value":"2038296","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1422103$DA36113B-81E8-45E8-88B6-39B64B032AEF","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e325a72f0e26ab98b1e996e2e86ac8d7891b9a92","datavalue":{"value":"reverse mathematics","type":"string"},"datatype":"string"},"type":"statement","id":"Q1422103$F210F7E2-FBA5-4C48-9AA7-39B87C14CE90","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"87748aa4dda05bf8965e742d76826d38a1ea956d","datavalue":{"value":"RCA","type":"string"},"datatype":"string"},"type":"statement","id":"Q1422103$D0F94C14-A481-4546-82F7-A2EC99479DBF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"461d39200e573b893247f72bc707a68f4eb77ea1","datavalue":{"value":"ACA","type":"string"},"datatype":"string"},"type":"statement","id":"Q1422103$67E776E3-4C7C-4F06-9BC3-D628EC06E457","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e928ef71c0e7c501fd4e474de74400a15fc3e89d","datavalue":{"value":"second-order arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1422103$75B0F79B-F402-40AF-AAC6-2D37794E77C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4f2c19f911179bd48de63cc4a5c8166d20f9271d","datavalue":{"value":"completeness theorems","type":"string"},"datatype":"string"},"type":"statement","id":"Q1422103$EBA831D7-7131-4E33-AAA5-1C09808FCB58","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d450f4b3083fe34d24db452ee74b92106c27a96e","datavalue":{"value":"intuitionistic logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1422103$6A2536FB-583F-488A-A1AB-472C0A039A1C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3875c79fa835ac45a1818de05c1bd8b1020c938e","datavalue":{"value":"Kripke model","type":"string"},"datatype":"string"},"type":"statement","id":"Q1422103$87199201-024A-4AD0-9EBC-FC7646769624","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"c2c7a0f70c0b7cc2161585e985e86183cb70d3ef","datavalue":{"value":{"entity-type":"item","numeric-id":335001,"id":"Q335001"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1422103$CD378F12-E5C4-40FD-8451-20CACC9D8E09","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":"Q1422103$25596558-70FB-461F-9859-AE5366DB1F44","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"f0bf415079cc4f0bd0fb6ca04111d7adb3e14c82","datavalue":{"value":"https://doi.org/10.1305/ndjfl/1063372197","type":"string"},"datatype":"url"},"type":"statement","id":"Q1422103$8F55C380-7C86-4520-B221-DD8BEC8D1496","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"f6330e92d57b394f47cf14d112de59f7fee92d21","datavalue":{"value":"W2036685181","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1422103$8BBFED2E-DC76-45BC-9632-B588F594D75D","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"a5dfbc538077da75d332fb528c12551a8b230f68","datavalue":{"value":{"entity-type":"item","numeric-id":1148885,"id":"Q1148885"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1422103$9A298CA6-20B7-456A-88E0-D0D5F5166C5B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dbd45668f5c7df10e41357180dce692a684f32ed","datavalue":{"value":{"entity-type":"item","numeric-id":1295382,"id":"Q1295382"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1422103$60D044E4-8070-4E84-A735-D572EE346FDE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ade6af8b14e3e35f4108a39f58b550626f0e8699","datavalue":{"value":{"entity-type":"item","numeric-id":4220572,"id":"Q4220572"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1422103$D24F0E5D-5D96-4A1C-B229-D1E01B263962","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":"Q1422103$60B897F3-4B30-4869-922B-B29348A707CC","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"554b6bdeff15380f5ae6629f316fb539a52ce0da","datavalue":{"value":"10.1305/NDJFL/1063372197","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1422103$20A6C94A-8CDC-45B5-9FF7-5383C79465EB","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e1cf0092b223699992e363dfeb119325463eb344","datavalue":{"value":{"entity-type":"item","numeric-id":708927,"id":"Q708927"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"022494e7fbfcdeaa01cc5cb94ed99a97701b42e8","datavalue":{"value":{"amount":"+0.801729142665863","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":"Q1422103$912CD3BA-468B-489C-B522-38BACB831A88","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":"f1ca53772b2ec590039e1c5fe53d4aa40d1724f0","datavalue":{"value":{"amount":"+0.7981385588645935","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":"Q1422103$7468CB4F-A407-4FF2-8606-6FCDCF8AF831","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8012afe9c971671213ca3724296aa1e4d5255425","datavalue":{"value":{"entity-type":"item","numeric-id":540402,"id":"Q540402"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d80fda8e8afa3ffbbbd72c8bfbf60a6c15ae3ac8","datavalue":{"value":{"amount":"+0.7894526720046997","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":"Q1422103$1AF8564C-7095-4710-99E9-04611BCE7F16","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"22eed11b0b0c9c9ec9c7b273fbd8edcda3ada453","datavalue":{"value":{"entity-type":"item","numeric-id":4397034,"id":"Q4397034"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"19595fea2bef9698e3bf79eda022a5869627b89b","datavalue":{"value":{"amount":"+0.7797882556915283","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":"Q1422103$B79EB95D-23B9-45B5-99CE-79E1E55C4194","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7bda8203e90c35ad1cc66854ea0db74d933291f4","datavalue":{"value":{"entity-type":"item","numeric-id":5502819,"id":"Q5502819"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ce6da119e2d8c6567544005315b7985bd9318da5","datavalue":{"value":{"amount":"+0.7754177451133728","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":"Q1422103$676A0A69-D32C-4B6C-B699-E86E6533A0AD","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Reverse mathematics and completeness theorems for intuitionistic logic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Reverse_mathematics_and_completeness_theorems_for_intuitionistic_logic"}}}}}