{"entities":{"Q1177033":{"pageid":1187782,"ns":120,"title":"Item:Q1177033","lastrevid":70168563,"modified":"2026-04-13T12:54:48Z","type":"item","id":"Q1177033","labels":{"en":{"language":"en","value":"Propositional consistency proofs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 12850"}},"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":"Q1177033$2D9748D2-176D-45A1-96EB-8B53B79BFAF5","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"5949a07788e85f69068222fdb83c7858c44c0bbe","datavalue":{"value":{"text":"Propositional consistency proofs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1177033$314EA77C-A9FF-447F-BF60-24DFEECDC8F4","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"38d2e6fd5678ea681860b10a0d51f75431a8ba53","datavalue":{"value":"0749.03040","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1177033$6E9D71AA-3643-4C9E-B88D-86FC10E348EB","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"a082da124b4db8ecfb40cc13e0a5ef52f182649a","datavalue":{"value":"10.1016/0168-0072(91)90036-L","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1177033$34C9511C-1489-428A-B39D-1412592440FE","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":"Q1177033$A1A9629D-B98A-4DD1-B17E-2E15AB7909C0","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":"Q1177033$5D37E135-BBAA-4302-BB35-79B5A07380A8","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"d3f790682a6be4cc1f3210e15eebe1d6cc5ffbc2","datavalue":{"value":{"time":"+1992-06-25T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1177033$5D3B84A5-E19C-4839-849E-24E78E541F56","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"001a8ea7a078ff2f4a6349e535b09755307c6d2a","datavalue":{"value":"Let \\(\\text{Con}_{\\text{ZF}(n)}\\) be the statement that there is no ZF- proof of a contradiction using at most \\(n\\) symbols. Then, of course, \\(\\forall n \\text{Con}_{\\text{ZF}(n)}\\) is not provable in ZF; but \\(\\text{Con}_{\\text{ZF}(n)}\\) is for each numeral \\(n\\), and, indeed, within a polnomial of \\(n\\) steps. The author presents similar results in propositional calculi. A choice of (propositional) connectives and (a finite number of) axiom schemes, together with modus ponens as the only rule of inference constitute a Frege system. (Of course, completeness is required.) Of any two such systems \\(\\mathcal F\\) and \\(\\mathcal G\\), the autor (i) produces a polnomial \\(p(n)\\) such that \\(\\mathcal F\\) proves \\(\\text{Con}_{\\mathcal G}(n)\\) within \\(p(n)\\) symbols, and (ii) presents a new proof of a result of Reckhow that \\(\\mathcal F\\) and \\(\\mathcal G\\) \\(p\\)-simulate each other (i.e. a proof of \\(\\mathcal F\\) is translatable in \\(\\mathcal G\\) within polynomial growth rate, and vice versa). Let \\(e{\\mathcal F}\\) be the extension of \\(\\mathcal F\\) by addition of the rule that allows the derivation of \\(p\\leftrightarrow\\varphi\\) where \\(p\\) is a new variable which has not been used yet and does not appear in \\(\\varphi\\) or in the last line of the proof. The last result is: (iii) \\(\\mathcal F\\) \\(p\\)-simulates \\(e{\\mathcal F}\\) iff \\(\\mathcal F\\) proves \\(\\text{Con}_{e{\\mathcal F}}(n)\\) with a polynomial bound of \\(n\\). To code meta-mathematical notions into propositional languages, and within polynomial bounds at that, requires much skill and elaborate work: hence the length of the paper. Indeed, for instance, the natural definition of a formula being depth \\(k\\) subformula of another grows faster than any polynomial of \\(k\\), and so the author devises a new definition that is polynomially bounded. With good explanations and examples, he makes the flow of thought clear.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1177033$98FA9FED-84E9-4084-9EBE-F2B42DEF5A39","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"4dd17e948ef0e266d136e969bf8283741afbd898","datavalue":{"value":"03F25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1177033$57EFCA4B-565C-4F64-9E6C-10C078F482F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ece9b879f80d96e2a1d45b28bdcc8cfa6b01861e","datavalue":{"value":"03F20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1177033$45C515B9-926C-4DE8-ADD3-B65FD621201B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"419d6f2b09c39920e34f63114ff159a2f0a01812","datavalue":{"value":"03B05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1177033$643F54C5-11BC-45CF-84E5-C7AC9412BEC3","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"670ec907e764520c35cada0f9fbb31d8001558c8","datavalue":{"value":"12850","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1177033$AB7674BE-B8CA-4DE7-9A2F-277438C3D168","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"78640e80bb829bfe179051d5d25cbc717a03aa07","datavalue":{"value":"mutual consistency proof","type":"string"},"datatype":"string"},"type":"statement","id":"Q1177033$4913446C-2F71-46F6-A5DD-4A8CD86982FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"097d6e89bfa4166ac039f0b7da62203670467618","datavalue":{"value":"propositional calculi","type":"string"},"datatype":"string"},"type":"statement","id":"Q1177033$3673314E-3E5A-44D0-BD9F-8DB2E8EC1FBC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8b8cb70894e2a9655efdcbcc7408847d5fa4f57c","datavalue":{"value":"Frege system","type":"string"},"datatype":"string"},"type":"statement","id":"Q1177033$96322198-5F6A-41E4-A843-7FE0FEF67CDF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4565836cda8f6196b10c191b12032cc546833a0f","datavalue":{"value":"polynomial bounds","type":"string"},"datatype":"string"},"type":"statement","id":"Q1177033$F071186E-0E0A-44D9-B6A5-76B8F487E413","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":"Q1177033$4CA3F35E-35F2-4DA5-9573-B483731988CB","rank":"normal"}],"P223":[{"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":"Q1177033$616CDBA7-1364-4BCA-BD97-F493F7572545","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"34a549ed1d776396be3e4308655e166de224ba89","datavalue":{"value":{"entity-type":"item","numeric-id":4133141,"id":"Q4133141"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177033$93251682-2ECB-4D84-96AD-7BBD8B41217E","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":"Q1177033$2AF35C89-34A4-4BD6-B57B-4B94B05C762A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"25f4a86512e0f02bf82877dbb62313fcd7fe9ed1","datavalue":{"value":{"entity-type":"item","numeric-id":3472096,"id":"Q3472096"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177033$EC9E9C09-6490-4524-BCCD-C5919C0581A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"16379452a4949bf4e97a3cd79c6104d4a7ee9465","datavalue":{"value":{"entity-type":"item","numeric-id":3755452,"id":"Q3755452"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177033$CC0FA607-8728-4B54-9D91-B900C53EA58F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"11c8e8c45bd30e4d2779b4e28bf2c174478c03fb","datavalue":{"value":{"entity-type":"item","numeric-id":3773878,"id":"Q3773878"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177033$ADFA3A0A-632E-4DCD-A879-16401455E023","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7d99375d9af310691fe93cef97a2d130b782c085","datavalue":{"value":{"entity-type":"item","numeric-id":3472096,"id":"Q3472096"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5110a6d0bec990831c23a02fd1698b9b76114088","datavalue":{"value":{"amount":"+0.8036717772483826","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":"Q1177033$A2A7A7C4-09EE-4876-97F9-E5E70CBEF9AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fbe76ff71529b5c527ec5d305058ab677441c61e","datavalue":{"value":{"entity-type":"item","numeric-id":2469433,"id":"Q2469433"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f54c7e1b78b15a801559a13d12b2343d4fd32f83","datavalue":{"value":{"amount":"+0.7922305464744568","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":"Q1177033$FBC482F2-3024-4433-AFAE-D99ACF3B8CC8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c2cccaac9b36deb25402bd0f6ccff787ac830afb","datavalue":{"value":{"entity-type":"item","numeric-id":3775553,"id":"Q3775553"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"02dce4ee147fd34d83e8d2bac4027e15bcecb369","datavalue":{"value":{"amount":"+0.7856056690216064","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":"Q1177033$A6B77C6B-3DC3-4F19-AB4B-3C58436C2B63","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":"9fcc1dc1eda8d5f5b39e624487a88ee22081e11c","datavalue":{"value":{"amount":"+0.780411958694458","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":"Q1177033$7CA5E62F-6DD4-479A-8484-CEA9C5F57A1A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e4ef7516fef19e6ad66dadf2480597f1ae72fc3d","datavalue":{"value":{"entity-type":"item","numeric-id":3081620,"id":"Q3081620"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fe32352e898ad7d70d9a7bd2c2690ea6bb5226c6","datavalue":{"value":{"amount":"+0.7764987349510193","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":"Q1177033$B36AB185-6D97-4C0C-AADB-707386B1E4C4","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Propositional consistency proofs","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Propositional_consistency_proofs"}}}}}