{"entities":{"Q365682":{"pageid":367449,"ns":120,"title":"Item:Q365682","lastrevid":61278546,"modified":"2026-04-10T22:19:52Z","type":"item","id":"Q365682","labels":{"en":{"language":"en","value":"Program extraction for 2-random reals"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6206986"}},"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":"Q365682$C489DE99-E529-48EA-B767-2C82E12D4DEC","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"4bee6b89ab455e0e58bf8c21ad2acd43eaa8fda2","datavalue":{"value":{"text":"Program extraction for 2-random reals","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q365682$51BEC0E2-5523-40E4-BE50-65CC60CA4E23","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"0dd479e8d6510ed598cf90ce224279c631c7b45f","datavalue":{"value":"1295.03039","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q365682$89AAC4B6-D354-48B7-8BD1-CCAD1A41ADB4","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"71b151c9da44809f650995a7f88ca4d5f5807da4","datavalue":{"value":{"entity-type":"item","numeric-id":365681,"id":"Q365681"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q365682$FB0F1926-60C0-4EB9-B650-473AC0241E6C","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":"Q365682$F45E1760-F1E1-465D-B6D0-6C4BA55BF4B3","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6e8c017497806797f217f1d658e3d224a2498206","datavalue":{"value":{"time":"+2013-09-09T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q365682$0EBBDCF1-BB37-45B0-8107-43B77D417B17","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"75bb50f109cf43f1c8b9dd46028239ed32e0d561","datavalue":{"value":"The main theorem of this paper states that \\(\\text{WKL}^\\omega_0 + \\Pi^0_1\\text{-CP} + \\text{CAC}+ 2\\text{-RAN}\\) is conservative over \\(\\text{RCA}_0^\\omega\\) for sentences of the form \\(\\forall f \\exists x A_{qf}(f,x)\\), and that from any proof of such a sentence one can extract a primitive recursive realizer \\(t[f]\\) for \\(x\\). Here \\(\\text{WKL}^\\omega_0\\) denotes the extension of the usual \\(\\text{WKL}_0\\) subsystem of reverse mathematics to all finite types. \\( \\Pi^0_1\\text{-CP}\\) denotes the \\(\\Pi^0_1\\) collection scheme, sometimes called \\(\\text{B}\\Pi^0_1\\) by other authors. \\(\\text{CAC}\\) is the chain anti-chain principle and \\(2\\text{-RAN}\\) asserts the existence of a \\(2\\)-random real relative to any given set. The subscript \\(qf\\) indicates that \\(A_{qf}\\) is quantifier free. An immediate corollary in second-order arithmetic is that \\(\\text{WKL}_0 + \\Pi^0_1\\text{-CP}+\\text{CAC}+2\\text{-RAN}\\) is conservative over \\(\\text{RCA}_0\\) for sentences of the form \\(\\forall X A(X)\\) where \\(A\\) is \\(\\Pi^0_3\\).  The proof of the main theorem is based on the proof extraction techniques developed in work of \\textit{U. Kohlenbach} and \\textit{A. P. Kreuzer} [J. Symb. Log. 77, No. 3, 853--895 (2012; Zbl 1254.03112)] and \\textit{A. P. Kreuzer} [Notre Dame J. Formal Logic 53, No. 2, 245--265 (2012; Zbl 1253.03090)]. A different proof technique was used by \\textit{C. J. Conidis} and \\textit{T. A. Slaman} [J. Symb. Log. 78, No. 1, 195--206 (2013; Zbl 1305.03055)] to prove that \\(2\\text{-RAN}\\) is \\(\\Pi^1_1\\)-conservative over \\(\\text{RCA}_0 + \\Pi^0_1\\text{-CP}\\). For alternative principles equivalent to \\(2\\text{-RAN}\\), see the work of \\textit{J. Avigad} et al. [Ann. Pure Appl. Logic 163, No. 12, 1854--1864 (2012; Zbl 1259.03021)].","type":"string"},"datatype":"string"},"type":"statement","id":"Q365682$A5D928E6-79DF-4D36-AD02-A1FE2CA1EF54","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"c2c7a0f70c0b7cc2161585e985e86183cb70d3ef","datavalue":{"value":{"entity-type":"item","numeric-id":335001,"id":"Q335001"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q365682$A89553BF-E565-4303-924B-843DBD63F63D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"4cb4544bfd0397cd4a315ee326499c372f013de5","datavalue":{"value":"03F35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q365682$54E7D6DE-F91F-4A86-841F-0C821E9B9186","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"13841f0b96793f178ce9a7dcac9f232220625aee","datavalue":{"value":"03B30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q365682$DA41F77F-EEDA-4473-9DEB-0517D2C8667F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"53a6dd9f6671ef90670f5c57fd3a10f9dadfeea8","datavalue":{"value":"03F10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q365682$03486585-5C34-42FB-85D8-40CF14DF2BF1","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"27e515b61c1867078b8b80d80bf751945c9d69f3","datavalue":{"value":"6206986","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q365682$63425FDD-AD93-49BE-9C3E-372FE02A34D0","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"490337ef18b03023a332407f87820bc9b56d61d8","datavalue":{"value":"weak weak K\u00f6nig's lemma","type":"string"},"datatype":"string"},"type":"statement","id":"Q365682$07B94E44-33F3-4D59-8463-CACEB0A5142D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bd15d6db1725e9b5b1a8ee63653406d21e0f41e2","datavalue":{"value":"2-random reals","type":"string"},"datatype":"string"},"type":"statement","id":"Q365682$5EEAB532-CCAE-4F06-972D-920FD942934D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"36a96860261afab88486624af0939a44f9aa584f","datavalue":{"value":"program extraction","type":"string"},"datatype":"string"},"type":"statement","id":"Q365682$56B7EF8B-8CAC-4824-9D70-5931F975C97E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"39ece27df4663c7fd54c61ee7602b62b0604cc6a","datavalue":{"value":"conservation","type":"string"},"datatype":"string"},"type":"statement","id":"Q365682$C7C69D53-33F2-4277-A85F-0190AC3D5349","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d7c23305d5a301c23057fddc53953635a4398a76","datavalue":{"value":"proof mining","type":"string"},"datatype":"string"},"type":"statement","id":"Q365682$857FD61D-BF5F-4508-A5C3-B4ACA8A1A306","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":"Q365682$0761F62D-9D48-4A7F-997A-65368AF533C0","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"00dc0a6e155a8cbed03329ac195de49b811a9aa3","datavalue":{"value":"https://doi.org/10.1007/s00153-013-0336-9","type":"string"},"datatype":"url"},"type":"statement","id":"Q365682$1D407D3C-1292-4228-9CBE-409EED884C88","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"67de7490c3b79720d4b417cde7e85b81fbf9a17f","datavalue":{"value":"W2021119129","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q365682$FBDFD686-1AF4-478F-9CDD-5CEE4445B99B","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"7dd656d8970ab8b37827d9b7d5347b99d737f4db","datavalue":{"value":{"entity-type":"item","numeric-id":2915896,"id":"Q2915896"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q365682$DBD33389-5957-49F8-B28C-109EE620D835","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d4aab8b4eea31d5d165b714e55365ac470a41376","datavalue":{"value":{"entity-type":"item","numeric-id":435242,"id":"Q435242"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q365682$29C9CA7D-BD93-4413-9D90-0D781000C50B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"30ac8787e7c7893030486590f5fa75efd9f4d57e","datavalue":{"value":{"entity-type":"item","numeric-id":2639061,"id":"Q2639061"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q365682$5B1125E1-3DD9-471E-8B2C-9FCA503B4886","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ea72a0b6f492719735a88c38789be486b04287bd","datavalue":{"value":{"entity-type":"item","numeric-id":714719,"id":"Q714719"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q365682$7A46FB5C-DA18-48DD-A50A-29A48C70B7B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9182e1e08dd41cf99fb976a8a02c7dd5bddd4bc0","datavalue":{"value":{"entity-type":"item","numeric-id":4916553,"id":"Q4916553"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q365682$898BB3C1-0436-4D0A-8CFA-55C30485F6CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"372ac7410c3602549aaffbccc69cf9a80d4b9494","datavalue":{"value":{"entity-type":"item","numeric-id":5711891,"id":"Q5711891"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q365682$89520227-41F1-4920-9659-62442D3A114E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"736c442fad7b5d4f015ebade6085c65d041e687b","datavalue":{"value":{"entity-type":"item","numeric-id":436224,"id":"Q436224"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q365682$4CEB172C-57F3-41B5-9E93-D4D43E63F93F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"384c88ee747368e498e55b1ebc22017816448ffc","datavalue":{"value":{"entity-type":"item","numeric-id":2265415,"id":"Q2265415"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q365682$154602EA-9325-4E2F-95E9-CA7134D0F797","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e1484ffd13476ff4e30167317b1f1955782f6b13","datavalue":{"value":{"entity-type":"item","numeric-id":1267846,"id":"Q1267846"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q365682$4F74737C-BC22-4F46-B816-25227DCA1F9E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e73cbdc4f532ed72bacdc9e85f4929b162897095","datavalue":{"value":{"entity-type":"item","numeric-id":5450521,"id":"Q5450521"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q365682$6DCF4B0D-B569-4C27-AAE3-D86EE4026978","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"45131a38ff53f12b9952d52e2962c28740fef2f7","datavalue":{"value":{"entity-type":"item","numeric-id":3161424,"id":"Q3161424"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q365682$9803A38F-5CB8-499C-B337-73A82A173749","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"848b72b2ad6c63d68bfff44b02eacd96943ab169","datavalue":{"value":"10.1007/S00153-013-0336-9","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q365682$FBEC65DA-2BF0-4E74-831A-09EC8F95DF9E","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f25aff33cf49cd05566c14b845bd43f3a6a8ac19","datavalue":{"value":{"entity-type":"item","numeric-id":4916553,"id":"Q4916553"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c39de1005efd923f4daab9a5999905bee3b378fb","datavalue":{"value":{"amount":"+0.7851613759994507","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":"Q365682$FA263E38-7BA3-44DB-AC42-FE0AA3E9BF99","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0f1aa137ed58605d23c57ae58f6c2b1771bc3fa6","datavalue":{"value":{"entity-type":"item","numeric-id":2915896,"id":"Q2915896"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ed9d89d40790c9bffe1734c594ca4969a282f7ad","datavalue":{"value":{"amount":"+0.7486768364906311","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":"Q365682$3501EDF8-A959-454C-B0A7-22F8D1E06E60","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c128cba860242835997e528fbe02e479bcf58b31","datavalue":{"value":{"entity-type":"item","numeric-id":2892679,"id":"Q2892679"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"240dc792328824f5f9874b80e0d1760c4ab64ef0","datavalue":{"value":{"amount":"+0.7448033094406128","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":"Q365682$90B43FCA-5969-4452-A124-BAEBBE87327B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"92900edabf8dfc7ac827acbfff9f64d0bc7092be","datavalue":{"value":{"entity-type":"item","numeric-id":5107230,"id":"Q5107230"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d085dbdd262ac86436428b90b80ba56c43ddd7f2","datavalue":{"value":{"amount":"+0.7353258728981018","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":"Q365682$E6483FED-223B-4507-9EA2-73061E9BC1BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fb4cad0292f73c50bff1f9a51494a0119ad7eaf1","datavalue":{"value":{"entity-type":"item","numeric-id":2898881,"id":"Q2898881"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cab5b4245df9894628e82518fe0fe63df8a2df12","datavalue":{"value":{"amount":"+0.7207164168357849","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":"Q365682$75FA8D41-966D-4575-AAA8-837C42FFC4D0","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Program extraction for 2-random reals","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Program_extraction_for_2-random_reals"}}}}}