{"entities":{"Q1304542":{"pageid":1315292,"ns":120,"title":"Item:Q1304542","lastrevid":68414373,"modified":"2026-04-12T23:33:11Z","type":"item","id":"Q1304542","labels":{"en":{"language":"en","value":"The complexity of the disjunction and existential properties in intuitionistic logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1339981"}},"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":"Q1304542$978B9BA0-772C-4C3C-8EE4-CB0BB8CF917C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"ff5dccdcc10bbf3dfa5c666937c4a9bf656132c0","datavalue":{"value":{"text":"The complexity of the disjunction and existential properties in intuitionistic logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1304542$BAC2929D-C0AB-4A32-868A-F2E79E3DE5AA","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"7710e82a43d69c91da5995b82ec2e45f965f5fbb","datavalue":{"value":"0939.03064","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1304542$B7DDE7AA-7987-4BD2-9DA8-2908ABAB8AB5","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"6418d3b1c75f43fffa9fd5dd14231592200cccb8","datavalue":{"value":"10.1016/S0168-0072(99)00002-0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1304542$F7A74318-14CD-4661-A95D-90C0AA79D724","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":"Q1304542$C50DA203-3140-4A36-A55B-364AEE71EE51","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"739bb59f926e46bf270e3affee77bc2ef6969661","datavalue":{"value":{"entity-type":"item","numeric-id":454365,"id":"Q454365"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1304542$BACB9E62-A458-4233-AED7-5FFA4C8858D8","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":"Q1304542$5603A083-5C27-4D8A-8ADE-40443E04FDED","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"8b5bfa12347d4716af416e8493dcfe0d9b94cba5","datavalue":{"value":{"time":"+2000-02-15T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1304542$B4D306ED-6170-498A-9AFF-E8900DB6A00E","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"43c77ee9ca94f09a3cba8b08c287c9a3bab108b5","datavalue":{"value":"As immediate consequences of Gentzen's Hauptsatz, one has disjunction and existential properties of intuitionistic logic. (They are: if \\(\\lvdash A\\vee B\\) then \\(\\lvdash A\\) or \\(\\lvdash B\\), and if \\(\\lvdash\\exists x C(x)\\) then \\(\\lvdash C(t)\\) for some term \\(t\\), respectively.) However, to find which disjunct or which term is beyond recursive means. [The authors remind us to think of the halting problem.]   In this paper, the authors take up a somewhat different aspect: namely, given a proof of \\(A\\vee B\\), or \\(\\exists x C(x)\\), how efficiently\\dots? The answer depends on the logic used. In propositional logic, polynomial time is enough to construct a proof of a disjunct. In predicate logic without function symbols, both properties can be shown in exponential times. But, with function symbols, super-exponential bounds are necessary. Optimality is shown by considering a fragment of arithmetic with a binary predicate for \\(y= 2^x\\) for the existential property, and for the disjunction property a Turing machine whose future states are hard to predict. This last construction is ingeneous, the reviewer thinks.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1304542$EA3BA645-4931-4311-BFE6-0B3A15707728","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"ece9b879f80d96e2a1d45b28bdcc8cfa6b01861e","datavalue":{"value":"03F20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1304542$CC854796-91A7-4DC9-BB76-3E8B23FF1AE7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"3068729a394ad5bf58a1a3e5b5d24254d962e1a7","datavalue":{"value":"03F55","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1304542$D84EF594-3036-4B55-B7BE-E72CC501F8C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"8195a9e26c453276e1d31339bf2413392412013d","datavalue":{"value":"68Q17","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1304542$E090694F-274A-4689-992D-D07CC00EFAFC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b4346faa01bb5fb0576370374d6456afd58d5666","datavalue":{"value":"68Q15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1304542$C6B4A356-CC25-497C-8807-8DD8F5C8166F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"3fcf821cd7103fb483115822e0ea19ccd437f2b6","datavalue":{"value":"1339981","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1304542$6AE2D591-8523-4CB5-AA07-331E4D97B759","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c5f8382ba04f9f05f645b4d0e4b9ea28f0619583","datavalue":{"value":"complexity","type":"string"},"datatype":"string"},"type":"statement","id":"Q1304542$829F8F00-F9DC-4FD0-815A-05E2B584180C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3020c5a082e5813cedace6da7c6bdd6690dd9fb5","datavalue":{"value":"disjunction property","type":"string"},"datatype":"string"},"type":"statement","id":"Q1304542$7689DFD1-3636-46C6-A184-AF36AE458A4B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0d05c13a4abe321ac5c8d87ce4d27164606d0684","datavalue":{"value":"existential property","type":"string"},"datatype":"string"},"type":"statement","id":"Q1304542$89A17832-542E-4536-A930-65EF71673AF8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d450f4b3083fe34d24db452ee74b92106c27a96e","datavalue":{"value":"intuitionistic logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1304542$4701CF2B-F9DC-441D-BAAB-770027BAAF2A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8ab4a6e9e68179258a958a02b9c82d30712b8ab8","datavalue":{"value":"fragment of arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1304542$AE72D8D1-24A8-4EF9-B170-53B22502E625","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":"Q1304542$C5D7BCD3-DE37-499C-AA41-8D38FFBF99B6","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"ff1c9576a9af1e44009a9ef9a0f7f22e091829d5","datavalue":{"value":{"entity-type":"item","numeric-id":5610986,"id":"Q5610986"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1304542$BD1E86A0-9F42-41B4-A6A5-2F0C2D2A2D54","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"21f66774e18bf6d9e857072576d53e1307dde765","datavalue":{"value":{"entity-type":"item","numeric-id":4149442,"id":"Q4149442"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1304542$731B679D-9CAE-40D9-9D75-992B85803210","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"86e2b29d9b4dadfb2f5b72715f7422f8e108a4ff","datavalue":{"value":{"entity-type":"item","numeric-id":1167721,"id":"Q1167721"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1304542$4B1FD0B9-40C7-4EC3-8DE7-19B871899169","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b8d95625ec9e5b7c46cee42d87256157d982706a","datavalue":{"value":{"entity-type":"item","numeric-id":5559220,"id":"Q5559220"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1304542$7AE0B19A-5604-4E7A-897C-3AE6745B8EC6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7e499c86ee0646fff12cf3f079c9131faaea7b20","datavalue":{"value":{"entity-type":"item","numeric-id":4215637,"id":"Q4215637"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1304542$F8DDFFC0-8532-42F7-A674-FD4AADCC099C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cea085d8c059c5f81ccc8c6d0a2a9f9fb30e1313","datavalue":{"value":{"entity-type":"item","numeric-id":1259589,"id":"Q1259589"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1304542$919CD09A-06AC-4421-8CAE-0015A12E21DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1813c495b4019dbc5a0338bf865711982b775489","datavalue":{"value":{"entity-type":"item","numeric-id":4198750,"id":"Q4198750"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1304542$C15C8F98-31F3-4342-8070-25360F5CE266","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"c2ff513ebd4ff751a5db663f3f9feefb68e3a757","datavalue":{"value":"https://doi.org/10.1016/s0168-0072(99)00002-0","type":"string"},"datatype":"url"},"type":"statement","id":"Q1304542$45B52578-C48B-4161-99C4-0B3F2ECAC2DD","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"df0dfb7db5f79f707413cd142d91479ba894f5c3","datavalue":{"value":"W1972606747","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1304542$833637BF-C0F8-4867-A2C7-9CE6A5DE80C8","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8e289159aac412911418892251df2ccdf1333e75","datavalue":{"value":{"entity-type":"item","numeric-id":5940143,"id":"Q5940143"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"19cb451b60bafb2248204b4b8ed1c3eb7d6e299d","datavalue":{"value":{"amount":"+0.8382193446159363","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":"Q1304542$01F46611-7E7C-434E-AD51-9A3FAB2CE08C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a2bb7ab013ca3e4e259966b816e7f387d6ee572d","datavalue":{"value":{"entity-type":"item","numeric-id":3824410,"id":"Q3824410"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"12a295846e51a1b31a412de3191406d9c03b30f8","datavalue":{"value":{"amount":"+0.8008853197097778","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":"Q1304542$7CF75651-3402-4896-9EAD-D1CAA30FA754","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"828704dbb3aad678a8d8e1ea9a8dc1214123cbe7","datavalue":{"value":{"entity-type":"item","numeric-id":5277730,"id":"Q5277730"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"849f696c9ebcd0d4229e36b115f1de3458fcf1a3","datavalue":{"value":{"amount":"+0.798681378364563","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":"Q1304542$FE5EF7C1-1F79-4DEB-B0BB-80FE42FB08B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1db62ab5a1e10fd5a379457aca6928451601e3c5","datavalue":{"value":{"entity-type":"item","numeric-id":4428299,"id":"Q4428299"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9cd6d07cda60b4f85606d8c8338f17f7922c30c4","datavalue":{"value":{"amount":"+0.7949246168136597","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":"Q1304542$E50D53F0-A4B1-44F5-946D-0E8D589F1FCF","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"The complexity of the disjunction and existential properties in intuitionistic logic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/The_complexity_of_the_disjunction_and_existential_properties_in_intuitionistic_logic"}}}}}