{"entities":{"Q1023047":{"pageid":1024895,"ns":120,"title":"Item:Q1023047","lastrevid":66639666,"modified":"2026-04-12T11:28:44Z","type":"item","id":"Q1023047","labels":{"en":{"language":"en","value":"Substitution Frege and extended Frege proof systems in non-classical logics"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5563891"}},"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":"Q1023047$A8083DFC-B75C-44AB-AE3A-1772ABD28893","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"da17aa5c91d88e8a703621231d704a1c0adfa21a","datavalue":{"value":{"text":"Substitution Frege and extended Frege proof systems in non-classical logics","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1023047$D1B05A38-639B-46FD-A3D0-3FC6C11530CF","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"98892781bb064406268534501f10a6dd407bfbe8","datavalue":{"value":"1173.03044","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1023047$CB268EA6-5EEB-469C-A71E-21D62C73CD9A","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e1376d5316fb71db1c6e9bf664dff79c67388b0d","datavalue":{"value":{"entity-type":"item","numeric-id":331053,"id":"Q331053"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1023047$083E518C-DE9E-47B4-8EB0-FD02A2992EE8","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":"Q1023047$E5432805-5EF8-4EF6-9813-3C86DBBD1CFC","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"787079cd334b8c7e529712503a5fe043609e5231","datavalue":{"value":{"time":"+2009-06-10T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1023047$2C06FC25-B69F-4B3A-8FFA-35B93068886D","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"54f72d3b10cc34b0eb2c86bb7fc837221071b9bd","datavalue":{"value":"Substitution Frege (SF) proof systems have the substitution rule \\(\\phi\\vdash \\phi[p_1/\\phi_1,\\ldots,p_n/\\phi_n]\\) in addition to axiom schemata and the rule of modus ponens. Extended Frege (EF) systems have extension axioms \\(q\\Leftrightarrow \\psi\\) for a fresh propositional letter \\(q\\) instead of the substitution rule. It was known that SF and EF are polynomially equivalent for the classical propositional logic. The author proves the same result for all extensions of KB, all tabular logics, all logics of finite depth and width, in most cases by a polynomial intertranslation with the classical logic. For all modal and superintuitionistic logics of infinite branching a polynomial speed-up of SF over EF is established, extending recent result by P. Hrube\u0161.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1023047$53D0D8E7-0444-44B2-B2A3-1CF8367A36CF","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"ece9b879f80d96e2a1d45b28bdcc8cfa6b01861e","datavalue":{"value":"03F20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1023047$CE5A6BE5-C00D-4072-AF22-5B38B25004AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"74a6cec96241e450625296e63e8dd539239d7104","datavalue":{"value":"03B45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1023047$A260B449-1BBB-4D8F-B349-3FA86765D49C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"87f66489f0c14f30094b654591a05fdd61321103","datavalue":{"value":"03B55","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1023047$85A16BE9-AC79-4714-9CEA-CBA1AE4CCE18","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"c2f31cfd2101b4dec5536213729c049590e69d30","datavalue":{"value":"5563891","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1023047$8E7A1BCA-7223-41D2-A02C-0A034AF96947","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"beacc345177607df4ab1f59f0170626c9d1a1d90","datavalue":{"value":"propositional proof complexity","type":"string"},"datatype":"string"},"type":"statement","id":"Q1023047$36FF83EF-A377-480C-A597-2B087489DD52","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8b8cb70894e2a9655efdcbcc7408847d5fa4f57c","datavalue":{"value":"Frege system","type":"string"},"datatype":"string"},"type":"statement","id":"Q1023047$5FB5A41F-40D9-4F0D-AFB9-F14867CF92EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f1dda010537b7b36bd45151721146f720815706e","datavalue":{"value":"modal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1023047$9529521A-77F5-4792-9F1D-D54D945B106A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e20caaf0551fe84fb69eae2f4da361eb77759b92","datavalue":{"value":"intermediate logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1023047$5BFD834F-2A98-47E7-9BCC-E53EE5414306","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"8f432bccb81d11b6d0c5be5373ba82abf19c1967","datavalue":{"value":{"entity-type":"item","numeric-id":454365,"id":"Q454365"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1023047$E18FAE76-200C-478A-A7B4-130AFC97B401","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":"Q1023047$3502DF6F-54DE-4E13-89F7-FE4E72D3638C","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"02adc125088bde691f5e1abb6357df9d3f4b4998","datavalue":{"value":"https://doi.org/10.1016/j.apal.2008.10.005","type":"string"},"datatype":"url"},"type":"statement","id":"Q1023047$ADA91FE0-DB5A-406C-B45F-8ED4AEAE9474","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"d195296993a257269d6dce42e56d6b57871f1048","datavalue":{"value":"W2155797483","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1023047$7F00377D-3759-4F16-8649-13A665A3652F","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"f2ca04c59b1468ff9eb03a30febcf55d98359908","datavalue":{"value":{"entity-type":"item","numeric-id":1094870,"id":"Q1094870"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1023047$2449E2C6-6B31-4002-8482-D006EEBAB8AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4c57f109ba15c6a048a9a998f89156bed64daa4f","datavalue":{"value":{"entity-type":"item","numeric-id":1872729,"id":"Q1872729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1023047$502A91F7-AC77-410B-8B09-7798EBEB41F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"adc87194f53a9552766b22cbe3fffae4e25dcae6","datavalue":{"value":{"entity-type":"item","numeric-id":2744124,"id":"Q2744124"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1023047$958B5717-6BA7-404F-AA75-A0A9A584883E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4f31cbeafb74eb2331031a6d2305fa02411af3e7","datavalue":{"value":{"entity-type":"item","numeric-id":3775553,"id":"Q3775553"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1023047$5E1FC515-2595-4C4F-BEC8-66BEC6BB867E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"41cfc6d1ca649e77a169b6cd08a9283c8c165615","datavalue":{"value":{"entity-type":"item","numeric-id":1304542,"id":"Q1304542"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1023047$B6473668-DC04-46F7-8862-D1B6CF028879","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6fc582242659cee49d409675b8250ad17fb5d767","datavalue":{"value":{"entity-type":"item","numeric-id":5940143,"id":"Q5940143"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1023047$26117500-DA47-413F-AD3A-A54EE1CD257F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1f72c6e6f4ce6722d395e819cddc203e8d1adeec","datavalue":{"value":{"entity-type":"item","numeric-id":3128959,"id":"Q3128959"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1023047$63051447-5635-4958-94EF-A2C17980F73B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0bea75da9fa67a5f77faa9362cd4aa6c737c792a","datavalue":{"value":{"entity-type":"item","numeric-id":4194955,"id":"Q4194955"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1023047$FA35C877-45A5-4A09-A4C0-A46EB719075B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2ac45ad0e557b1b65daa9ad0ae84ca22e9b11568","datavalue":{"value":{"entity-type":"item","numeric-id":5277730,"id":"Q5277730"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1023047$5A1023C5-D4E5-4EBF-90C7-946945246C14","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aadb89586b12baabd090fee59e578386a236b4eb","datavalue":{"value":{"entity-type":"item","numeric-id":5422311,"id":"Q5422311"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1023047$FE6BF64C-C79C-4B06-98B5-41491A15D587","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aff4ee6a73fbacbcf6d7da620a82d0b3fbe596a6","datavalue":{"value":{"entity-type":"item","numeric-id":876385,"id":"Q876385"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1023047$C983A482-28B1-45B9-9209-AA63CCE93892","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7ccdc2885bcd85970cf2540be17a7b4af1868eaa","datavalue":{"value":{"entity-type":"item","numeric-id":1887654,"id":"Q1887654"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1023047$BADD2AFA-2E8A-4BF7-8657-FC48DBAD656F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"05fa13f8d08455deabdb8d53876205365d278e87","datavalue":{"value":{"entity-type":"item","numeric-id":5696300,"id":"Q5696300"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1023047$4FAB24EA-90FC-4626-B147-C7F5026DCB04","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8ea72334575ec9f68c192adc857ab078ff1e97f3","datavalue":{"value":{"entity-type":"item","numeric-id":2503409,"id":"Q2503409"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1023047$AED88B59-4E76-4F0D-80B4-898A33DDA4F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6fa34ae3e34f6a863a9f8db67c2bfb8bb6401943","datavalue":{"value":{"entity-type":"item","numeric-id":4856172,"id":"Q4856172"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1023047$164D0511-93D9-4119-8853-4F9153AEBC2B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7f9864cd692e177ef3a771b6df84de7a4d93d51b","datavalue":{"value":{"entity-type":"item","numeric-id":5460922,"id":"Q5460922"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1023047$83768890-9043-4F1A-B801-A140A5400355","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8e7deb7cbb7cd9c19da86f917c77d45ea86fa652","datavalue":{"value":{"entity-type":"item","numeric-id":4068699,"id":"Q4068699"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1023047$073FE78C-7AEE-4461-B78E-6D2488A081BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c84bd6b5a534f67b6b7d4c37a09d43bc1c1517c9","datavalue":{"value":{"entity-type":"item","numeric-id":4894720,"id":"Q4894720"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1023047$1568C8F1-93F1-4738-9E9B-CE3C0E951D19","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"0c469bda4f1ae1a3d7681d5aae28b36e7dc41d99","datavalue":{"value":"10.1016/J.APAL.2008.10.005","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1023047$176B1C8C-A26B-44A1-8A20-29381B038D55","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c8cf845b92fca11d3ef94c086cc58b80d7242580","datavalue":{"value":{"entity-type":"item","numeric-id":2084964,"id":"Q2084964"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d23a449e9d3132c6cf6b72a0b62fd57571b99f7b","datavalue":{"value":{"amount":"+0.840369701385498","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":"Q1023047$198D6CAB-410F-4ACE-A43D-A8FC7167260F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b8c0a75c4f1131ee866cde9f99c88c11d29350aa","datavalue":{"value":{"entity-type":"item","numeric-id":4850552,"id":"Q4850552"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"559f6d841579d4eccbd1404369904228e7b9288c","datavalue":{"value":{"amount":"+0.8322829008102417","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":"Q1023047$0266F560-BADA-49AD-85A2-0CEC77713D2E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a4cc45139fbfe093a2bc18cf33ce7eee42df4dcb","datavalue":{"value":{"entity-type":"item","numeric-id":2503409,"id":"Q2503409"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"256e5d545e3edc626a33f4c6857506af635abd18","datavalue":{"value":{"amount":"+0.7955908179283142","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":"Q1023047$D923A78E-5181-4503-9414-521E9A9F3C31","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f4e3bfa89bbce593c83c8f2ca50e1fbe1bc8b7d1","datavalue":{"value":{"entity-type":"item","numeric-id":2032997,"id":"Q2032997"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2aa7f2481eac69cf580a2c069665ff2b9faf0925","datavalue":{"value":{"amount":"+0.7912024855613708","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":"Q1023047$02D61F3D-EFE2-4B5F-BFDF-F04F96E353BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a20304930accadc7fe78aaead233fbe7aa148b06","datavalue":{"value":{"entity-type":"item","numeric-id":3829548,"id":"Q3829548"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"24e094fcb3ddab749064ae01505e5f89a36a6e50","datavalue":{"value":{"amount":"+0.7796527147293091","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":"Q1023047$6B945150-411F-413A-A455-6B9CC198955C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Substitution Frege and extended Frege proof systems in non-classical logics","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Substitution_Frege_and_extended_Frege_proof_systems_in_non-classical_logics"}}}}}