{"entities":{"Q701740":{"pageid":703589,"ns":120,"title":"Item:Q701740","lastrevid":48390370,"modified":"2026-01-04T14:11:47Z","type":"item","id":"Q701740","labels":{"en":{"language":"en","value":"Combinatorics of first order structures and propositional proof systems"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 2123159"}},"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":"Q701740$FCF7284E-8B95-4798-9635-BE89500B2287","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"6af5fc48944901293905998f49c6cc7222099f71","datavalue":{"value":{"text":"Combinatorics of first order structures and propositional proof systems","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q701740$53146B9F-6C41-470D-83BA-18548B635F4A","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"04b7cb3891461c93ac1626c7d607543503a0430a","datavalue":{"value":"1061.03060","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q701740$E0188E11-CED0-40F4-89ED-EDFAAAA5DCD7","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e4b9ae896fbf78b3fa2084fd5300754d74076f66","datavalue":{"value":{"entity-type":"item","numeric-id":226860,"id":"Q226860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q701740$A74B2FF6-BFE8-47BE-8C9C-841BFD52FD5E","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"a0a7cd28a9f85b9c6ad57bd5bb1ae477bfe37846","datavalue":{"value":{"entity-type":"item","numeric-id":114337,"id":"Q114337"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q701740$1A7E5B58-1122-44B5-8533-53CB2F8BF3D3","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"df1e508a21ee9936a7a8f9defc1512d58443c3e3","datavalue":{"value":{"time":"+2004-12-16T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q701740$78B38F11-CFF0-4422-AD3C-0C19FFE950EA","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"4e2df87acd591546ca7f867a4bc74ce00ca72792","datavalue":{"value":"The author continues his work of giving bounds of proof complexity by means of model theory. In this paper, he defines the combinatorics of a first-order structure \\(M\\), \\(\\text{Comb}(M)\\), and the notion of `\\(M\\) covers a propositional proof system \\(P\\)'. Using these, he obtains results that are not amenable to other methods. Namely, the proofs of propositional statements, \\(\\varphi_0,\\varphi_1,\\dots, \\varphi_k,\\dots\\) require superpolynomial (in \\(k\\)) size in each of the systems: resolution \\([R^*(\\log)]\\), Nullstellensatz proof system, and polynomial calculus, where \\(\\varphi_0,\\varphi_1,\\dots\\) are associated with familiar statements in field theory (like `a finite field cannot be ordered'). The general metatheorem, on which these results are based, relates the existence of an infinite counter-model of the given predicate statement to superpolynomial size of proofs of the associated \\(\\langle\\varphi_k\\rangle\\). The author also shows how to construct structures that cover the given proof system, on the basis of bounded arithmetic, and conversely (so to speak) how to construct a proof system starting from structures. Some conditions must be met for the construction to work, of course; and a number of results are obtained. For instance, if \\(P\\) contains a Frege system then any structure constructed covers \\(P\\), and the system polynomially simulates \\(R^*(\\log)\\) if it is obtained from a class \\(C\\) of infinite structures such that \\(\\text{Comb}(C)\\) is r.e.","type":"string"},"datatype":"string"},"type":"statement","id":"Q701740$EC1C94B3-7A95-42C4-97D6-5CB1F3613070","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"ece9b879f80d96e2a1d45b28bdcc8cfa6b01861e","datavalue":{"value":"03F20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q701740$199F0A6B-0879-42FB-85FD-2BC64CCAD454","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"abca938afd309309893053e8ee4f51374fed9de6","datavalue":{"value":"03C07","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q701740$17A83507-861F-4DB8-8668-91B4A5843281","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"8195a9e26c453276e1d31339bf2413392412013d","datavalue":{"value":"68Q17","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q701740$E908974D-62B8-405A-B5AA-7986B5AC13C1","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"822973ef3dd4998bf54b3cb37cd500e92cac2c5b","datavalue":{"value":"2123159","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q701740$4C652577-442E-4CA6-9A2F-129FA161BF26","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4ee539f3c66b5148353f42975573a39b50c5340f","datavalue":{"value":"complexity of proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q701740$6775CA03-57FE-4FC6-A7E9-70E7EF36FE69","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1d50ee99c2295ee97c52f35d687d4efe3cae3b14","datavalue":{"value":"model-theoretic method","type":"string"},"datatype":"string"},"type":"statement","id":"Q701740$943F0183-FAAD-486F-B406-061E1654FDBE","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":"Q701740$6B8C280C-0E18-49D8-B309-9983C703F486","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"a83d90803e4ce4b2c8d721e33bf14c8c95ad1d07","datavalue":{"value":"https://doi.org/10.1007/s00153-003-0186-y","type":"string"},"datatype":"url"},"type":"statement","id":"Q701740$B590A652-CB3C-4449-B230-D91A2266AE2C","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"68907b3d513c3a7ec0f40f315b88d7256c22330d","datavalue":{"value":"W1552145226","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q701740$354A13B9-9269-4CF7-9424-5661C08DE5B3","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"4852ab2f77a1b795eadd739e85bdc08af507293f","datavalue":{"value":"10.1007/S00153-003-0186-Y","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q701740$A22E126A-2158-4206-B895-2E2438E95086","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"00ba1c674b8c2ae1df7fd3017f835f546ef95963","datavalue":{"value":{"entity-type":"item","numeric-id":4625692,"id":"Q4625692"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7fa699531f73bfd0ef6e057ef3266248bee5f44c","datavalue":{"value":{"amount":"+0.750648021697998","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":"Q701740$FAB83DCE-35F1-430B-9E20-1F34511ED91B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"703adb724ab299360fb30806591e423fa43d4d8d","datavalue":{"value":{"entity-type":"item","numeric-id":5111195,"id":"Q5111195"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4e4f0b19a5dab8d24344f9d3e5a82ec3c883ac83","datavalue":{"value":{"amount":"+0.746310293674469","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":"Q701740$0B1AD406-E6DB-4A2E-9A9F-F378F0BE7EAD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2d2414746d0c17a096536954eb7fca1268bd6b97","datavalue":{"value":{"entity-type":"item","numeric-id":5444711,"id":"Q5444711"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7fa49fbf0de9be7acfb72ea15517fe834e687082","datavalue":{"value":{"amount":"+0.7349321246147156","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":"Q701740$7B5E28C5-4F40-4FE0-AF7C-60BB4D48B0EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"580ed2424e9846e9da8bbc3a40e4cf849a4221ab","datavalue":{"value":{"entity-type":"item","numeric-id":4399249,"id":"Q4399249"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"954b9246c714a60ae393e18b6c81ea39ab880ccd","datavalue":{"value":{"amount":"+0.7322335839271545","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":"Q701740$95F3C770-32F1-46B1-95A2-BEADA80B6BAE","rank":"normal"},{"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":"954b9246c714a60ae393e18b6c81ea39ab880ccd","datavalue":{"value":{"amount":"+0.7322335839271545","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":"Q701740$7C567E76-EA0C-4005-A206-41E1B0583057","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:701740","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:701740"}}}}}