{"entities":{"Q1057847":{"pageid":1059695,"ns":120,"title":"Item:Q1057847","lastrevid":66156426,"modified":"2026-04-12T07:55:20Z","type":"item","id":"Q1057847","labels":{"en":{"language":"en","value":"Don't eliminate cut"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 3898843"}},"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":"Q1057847$583A324D-58EC-400B-A768-A60B242F62CA","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"3cf7151d0738517692c0a1caa6cb41b8702e91e8","datavalue":{"value":{"text":"Don't eliminate cut","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1057847$3CB92C85-68FB-436D-BEF2-4F871EA2BF14","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"dd97324d6ac07782f01d6dae2bbafc8d38a1c20d","datavalue":{"value":"0564.03005","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1057847$B3305071-5CB9-4360-92BD-35C32731C970","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"b33c51c26e8c26ed0617f8c8cc85e885760bd179","datavalue":{"value":"10.1007/BF00247711","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1057847$FBFD6C69-5E3A-44B7-A810-E956C6C4AEF4","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"dae5d6cf705e82161555573be309f7a5a5d53fa9","datavalue":{"value":{"entity-type":"item","numeric-id":685072,"id":"Q685072"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1057847$A2440DAC-F43C-41C3-BA5C-B61E1E2F4886","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"e692f569038e7bcb7d3e72ba14d8d8e224046270","datavalue":{"value":{"entity-type":"item","numeric-id":169434,"id":"Q169434"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1057847$A1C06179-1370-48A9-A01B-130033188238","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2ee0f220147ae8bc749a64db56839865dbc4f127","datavalue":{"value":{"time":"+1984-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1057847$5F1F3A41-0BEA-44D0-A272-391B790D63F2","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"ebf2ec8ef715049c369ae9817fc72a2fac46b59b","datavalue":{"value":"Semantic tableau methods are sometimes used in logic courses because they produce derivations of various formulas of first order logic in a straightforward way. The feasibility of these tableau methods depends, however, on the formulas to which they are applied. This paper provides a simple formula H whose derivation by the tableau methods of Smullyan and Jeffrey would have more than \\(2^{128}\\) characters, hence ''more symbols than there are nanoseconds between Big Bangs''. On the other hand, there is a derivation of H in, essentially, Gentzen's system of natural deduction, containing less than 3280 characters.    The tableau methods in question are closely related to cut-free systems. What is really given here is a formula without a feasible cut-free derivation. The emphasis on natural deduction in the paper is a bit misleading. As the author mentions, the crucial point is that modus ponens provides for increased efficiency by allowing an appeal to previously established conclusions. The example shows in a vivid way just how great the gain in efficiency can be.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1057847$20FF272F-944A-40F2-99C8-A5FF505520E5","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"c06e0874e30722381d620ef69fb36c407a01cb04","datavalue":{"value":"03B10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1057847$ED70B101-5C66-41A9-9BCE-3CDAE884C481","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1057847$6B2E08A0-F780-4C36-BAF5-8F337DA7602E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"0277b898648c6ce6659f2a08052cd4cf75406c8b","datavalue":{"value":"3898843","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1057847$0B8ADDB9-051F-40EE-8694-19F86ADEFC5D","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"08adad6cd898e7c7d897e7197186a448e1e0c067","datavalue":{"value":"semantic tableaux","type":"string"},"datatype":"string"},"type":"statement","id":"Q1057847$57B2F484-56B9-4D7B-9EE0-7EBE65DB5A5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1ef97c440d93dc04ecec106dcb608da8f95f7ea6","datavalue":{"value":"method of trees","type":"string"},"datatype":"string"},"type":"statement","id":"Q1057847$9CC92025-31E7-4619-83EA-777B6F5D7892","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dcfc1bc00c58245854e787073d98b7cbed7ce1ba","datavalue":{"value":"cut elimination","type":"string"},"datatype":"string"},"type":"statement","id":"Q1057847$5CFB01E4-9C35-414B-A8D9-1258BD7857D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7e69dc5c4ff087096957a773306fa5e069636620","datavalue":{"value":"feasibility of proof procedures","type":"string"},"datatype":"string"},"type":"statement","id":"Q1057847$600209AE-F059-4D93-918C-B4A7A66761FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d3ac5f87c2452a4bb9221668c72755935919ba5b","datavalue":{"value":"tableau methods","type":"string"},"datatype":"string"},"type":"statement","id":"Q1057847$12FA11AA-4DC4-433A-B653-6439A41E59BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c39a3dcb919cfb7892b24ca37da2f18a4bcfe1c8","datavalue":{"value":"first order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1057847$9D34DE50-0DC7-4017-8AD1-DE9BCB94A2DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a7245057d33d9a959e820bafe53b372c083536e6","datavalue":{"value":"natural deduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q1057847$99E5ECF7-7794-41D0-8786-DD47E56422DB","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"e5e2a5720a49af3f774a10463c80dd488df8d858","datavalue":{"value":{"entity-type":"item","numeric-id":1161721,"id":"Q1161721"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1057847$CA52103E-48EF-4E48-BBB5-13D3771A23B0","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":"Q1057847$47D949FC-261B-4CA5-9CAE-F7E25D442F5F","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c7c43b7b18edc7d157fb7e5ac48ae2b05eb97b16","datavalue":{"value":{"entity-type":"item","numeric-id":4523479,"id":"Q4523479"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e1b0f5131f6edf38fbc720148e9ca9874075db37","datavalue":{"value":{"amount":"+0.99999994","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":"Q1057847$2B2CE03F-1136-4D26-976C-45F8E2C1DD25","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2596cee26fb2591617236d3064cebdaeb13b9a0f","datavalue":{"value":{"entity-type":"item","numeric-id":4842272,"id":"Q4842272"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3194a49a94c0616b3b6ad724ce2158f25d262621","datavalue":{"value":{"amount":"+0.8143414","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":"Q1057847$F52E0DA3-B15D-4E8A-932F-23776454335D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4b7c426f10a188313032acdbe9224fcaf7d72a3e","datavalue":{"value":{"entity-type":"item","numeric-id":3019775,"id":"Q3019775"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cbb50464daad68926a5e468c0c585c642c974b01","datavalue":{"value":{"amount":"+0.8024379","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":"Q1057847$AEB5395E-2218-48D1-A5D4-B5DC0C5D62A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5fe186cac75804def3c2fa703a831734e4da013d","datavalue":{"value":{"entity-type":"item","numeric-id":5361251,"id":"Q5361251"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"16c853f48e8e09e96be0026c6acd5374b82a8c6f","datavalue":{"value":{"amount":"+0.8016384","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":"Q1057847$6E826D62-905B-4D14-9996-B08FB3EE197D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"03da4b6b3513810b613f5f467d21802b524db7f7","datavalue":{"value":{"entity-type":"item","numeric-id":1817695,"id":"Q1817695"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0a7b64216b855f611b799e2c6379df3fad56ef4c","datavalue":{"value":{"amount":"+0.7758518","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":"Q1057847$2378D759-664A-46B4-B047-0C775B1B8588","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0fe0d74cab51b01aceeb955993bcda7e38c51e55","datavalue":{"value":{"entity-type":"item","numeric-id":3188285,"id":"Q3188285"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4284e0e051cc42dacd2be4f33d57de66f1094094","datavalue":{"value":{"amount":"+0.7736386","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":"Q1057847$02357151-4BEE-4542-B955-4838A320AC43","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"acb8ea6bb99c8f81b2ce256b0179befeaafd7c1c","datavalue":{"value":{"entity-type":"item","numeric-id":3367500,"id":"Q3367500"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e18bc661ccc97c62788e347101846bd3f190d7b4","datavalue":{"value":{"amount":"+0.77306056","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":"Q1057847$E7255008-7868-49E1-887D-D7343A222B05","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a2402b34c779a73eb9f6c4530e64b5a77c98788a","datavalue":{"value":{"entity-type":"item","numeric-id":609451,"id":"Q609451"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9a73c74a45e85963570973d054eae3f524afe8c3","datavalue":{"value":{"amount":"+0.7659159","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":"Q1057847$5994F108-1C06-49CA-95D1-F34FD3BE91EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"54139f930430c44bfddd66e87c6f88b9f5f6beaa","datavalue":{"value":{"entity-type":"item","numeric-id":4637625,"id":"Q4637625"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"eedbbbc3d073cf13e45b373c9158ca9d8fc661c1","datavalue":{"value":{"amount":"+0.75353324","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":"Q1057847$FEC05585-3E9E-49A4-8491-6E9BAB9FD24F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"651956c00c3a3fde0e9170d9c631adf2f69dd473","datavalue":{"value":{"entity-type":"item","numeric-id":851192,"id":"Q851192"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c91282114f5d1ed9614ca566113c4bd8638ffa4f","datavalue":{"value":{"amount":"+0.7492453","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":"Q1057847$907F329A-DA01-40C2-B09E-F14DD29E6DC0","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Don't eliminate cut","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Don%27t_eliminate_cut"}}}}}