{"entities":{"Q1267846":{"pageid":1278596,"ns":120,"title":"Item:Q1267846","lastrevid":70036398,"modified":"2026-04-13T12:00:29Z","type":"item","id":"Q1267846","labels":{"en":{"language":"en","value":"Elimination of Skolem functions for monotone formulas in analysis"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1210623"}},"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":"Q1267846$0CC870A7-548A-4B6F-82CA-42451064BFCE","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"3ed6da3453513b553746f415cb370ff7fef6a957","datavalue":{"value":{"text":"Elimination of Skolem functions for monotone formulas in analysis","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1267846$C371C6A5-FD35-4122-9F2F-A1955C9E9097","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"11469b8a16389257d93a5786c2a8e8bef3ffff49","datavalue":{"value":"0916.03040","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1267846$D01E96DA-C2A2-430F-B4A0-F751FA8515F1","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"3757c450e8ea3891f056e58fdb032b2670ff909f","datavalue":{"value":{"entity-type":"item","numeric-id":175049,"id":"Q175049"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1267846$2F0601B8-D703-4663-9C70-7DAFA753F355","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":"Q1267846$C15A82D1-B443-4005-92BA-58A42A25CE68","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"eec3153ba3dc7a85e2777def2dfd25825f99d8e8","datavalue":{"value":{"time":"+1998-11-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":"Q1267846$E8D8A5C0-20D7-421B-94F1-05540D5E4E7F","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"6f12029793d45994aca6459696d47318dccabb49","datavalue":{"value":"This is the second of a series of papers whose over-all purpose is to give estimations to the complexities of (formal) proofs of analysis. In this paper, the author develops a technical device -- elimination of Skolem functions -- to be used in subsequent work. Actually, he deals with the Herbrand normal form \\(B^H\\) of \\(B\\), and shows, roughly, that when \\(B\\) is monotone and \\(B^H\\) is provable from AC-qf in \\(G_nA^\\omega\\), then \\(B\\) is provable without AC-qf and also one can extract a tuple \\(\\psi\\) that satisfies the functional interpretation of \\(B\\). (For an explanation of \\(G_nA^\\omega\\) etc., refer to the first paper [\\textit{U. Kohlenbach}, ibid. 36, No. 1, 31-71 (1996; Zbl 0882.03050)].) There are many other results, including \\(G_2A^\\omega\\lvdash \\Pi^0_1\\text{-AC}\\to \\Pi^0_1\\)-[collection principle], and the like.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1267846$8FBA1527-CF91-4AE6-B90F-8DED4445AD53","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"4cb4544bfd0397cd4a315ee326499c372f013de5","datavalue":{"value":"03F35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1267846$BB8CD546-2C35-4406-92BC-88B199CE1850","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"53a6dd9f6671ef90670f5c57fd3a10f9dadfeea8","datavalue":{"value":"03F10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1267846$2169CE92-E260-4E68-BF54-EA9284AE6A06","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d971f250f4b60bd91da7e9350568180af141e6af","datavalue":{"value":"03F03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1267846$120EDF6D-AD55-4F88-8CE4-61F0F7597619","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"4dd17e948ef0e266d136e969bf8283741afbd898","datavalue":{"value":"03F25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1267846$BFBEDE42-17C4-4113-9F69-68F757D43684","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a7b2ff200a70acfa8a0fed3c496cfda0c139d3b1","datavalue":{"value":"1210623","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1267846$2FEB21A2-6921-4F4E-BBC8-60A4CDCE26CE","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"831c75974c29c6cb25f2a763e4b44981013e19e6","datavalue":{"value":"elimination of Skolem functions","type":"string"},"datatype":"string"},"type":"statement","id":"Q1267846$03B4FACD-8C9E-42F9-8E4E-E5163D121129","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8661572aaccc8ef90a52fd7944cc932d8244f9c1","datavalue":{"value":"Herbrand normal form","type":"string"},"datatype":"string"},"type":"statement","id":"Q1267846$65AEC32A-40D7-4F09-B452-10256D5EDF84","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"492942e689dba58f90096ed1c12c52b0f868caa6","datavalue":{"value":"functional interpretation","type":"string"},"datatype":"string"},"type":"statement","id":"Q1267846$A11F3E41-BEAE-4D72-992E-2312F1F72C23","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":"Q1267846$D6E51E29-2A9B-4E45-A7F0-D3126AD264A9","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"96f30118afc8cb473575d4e95a69052d66ef5ab0","datavalue":{"value":"https://doi.org/10.1007/s001530050104","type":"string"},"datatype":"url"},"type":"statement","id":"Q1267846$9F798635-1AF2-4108-B7F3-D66CED281C8E","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"5c53c4395d50a62f3f69a7da665cec56a413c7e6","datavalue":{"value":"W2001283416","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1267846$BE0CAB14-F040-41A9-9BF7-3EA616A38777","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f95b4535352f6d91607d33d5c23a50b5e723c228","datavalue":{"value":"10.1007/S001530050104","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1267846$044C77E4-D644-48C0-A00A-B9CBA1C2BAAA","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a6f13673604c697f60328849c656c56bea8944c7","datavalue":{"value":{"entity-type":"item","numeric-id":557798,"id":"Q557798"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2d6d3fc7994b90f8fc5c06e4dc25920944db3294","datavalue":{"value":{"amount":"+0.7836142182350159","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":"Q1267846$75CD6BBA-BB03-49B0-836D-FDF375DB4F8D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"39bbe7b05b504353157065776216c7d10590706b","datavalue":{"value":{"entity-type":"item","numeric-id":5267436,"id":"Q5267436"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0fb739562b273c5b4ff5234f0ecb044e744e8677","datavalue":{"value":{"amount":"+0.7597521543502808","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":"Q1267846$873C368D-1CA3-4295-9380-34FC5B60C921","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"804e47f8b399f9512aae8ae32179e6e6d1a0f29d","datavalue":{"value":{"entity-type":"item","numeric-id":2144618,"id":"Q2144618"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b3c94ed1399c18171eb7a2243b9de0fa809bab59","datavalue":{"value":{"amount":"+0.7569115161895752","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":"Q1267846$A99C1238-D2A5-4B66-8057-8A1BDD25B219","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4c05ff52b80d6dbfd5dc36ac59d953a7f881a330","datavalue":{"value":{"entity-type":"item","numeric-id":4304753,"id":"Q4304753"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4b102dc67acf368c59eeee65efe7aea4f63f7f3c","datavalue":{"value":{"amount":"+0.7495467662811279","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":"Q1267846$A687879F-186D-4F65-A98A-42BC6771E051","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fd6d9196b90aadfbe46f06604044c5d57c9eda7b","datavalue":{"value":{"entity-type":"item","numeric-id":4918424,"id":"Q4918424"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7c6abffe724eddf8d5ed41db99c18f7ded96a74d","datavalue":{"value":{"amount":"+0.7467284202575684","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":"Q1267846$FCBDFFF5-F63A-44C9-AA22-6606F8988E37","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Elimination of Skolem functions for monotone formulas in analysis","badges":[]}}}}}