{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,12]],"date-time":"2025-09-12T18:00:24Z","timestamp":1757700024219},"reference-count":21,"publisher":"World Scientific Pub Co Pte Lt","issue":"01","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Math. Log."],"published-print":{"date-parts":[[2012,6]]},"abstract":"<jats:p> We investigate the strength of the existence of a non-principal ultrafilter over fragments of higher-order arithmetic. Let [Formula: see text] be the statement that a non-principal ultrafilter on \u2115 exists and let [Formula: see text] be the higher-order extension of ACA<jats:sub>0<\/jats:sub>. We show that [Formula: see text] is [Formula: see text]-conservative over [Formula: see text] and thus that [Formula: see text] is conservative over PA. Moreover, we provide a program extraction method and show that from a proof of a strictly [Formula: see text] statement \u2200 f \u2203 g A <jats:sub>qf<\/jats:sub>(f, g) in [Formula: see text] a realizing term in G\u00f6del's system T can be extracted. This means that one can extract a term t \u2208 T, such that \u2200 f A <jats:sub>qf<\/jats:sub>(f, t(f)). <\/jats:p>","DOI":"10.1142\/s021906131250002x","type":"journal-article","created":{"date-parts":[[2012,5,10]],"date-time":"2012-05-10T08:15:00Z","timestamp":1336637700000},"page":"1250002","source":"Crossref","is-referenced-by-count":6,"title":["NON-PRINCIPAL ULTRAFILTERS, PROGRAM EXTRACTION AND HIGHER-ORDER REVERSE MATHEMATICS"],"prefix":"10.1142","volume":"12","author":[{"given":"ALEXANDER P.","family":"KREUZER","sequence":"first","affiliation":[{"name":"Fachbereich Mathematik, Technische Universit\u00e4t Darmstadt, Schlossgartenstrasse 7, 64289 Darmstadt, Germany"}]}],"member":"219","published-online":{"date-parts":[[2012,7,8]]},"reference":[{"key":"rf1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-3444-9"},{"key":"rf2","doi-asserted-by":"publisher","DOI":"10.1007\/s001530050095"},{"key":"rf3","unstructured":"J.\u00a0Avigad, Reverse Mathematics 2001, Lecture Notes in Logic\u00a021 (Association Symbol Logic, La Jolla, CA, 2005)\u00a0pp. 19\u201346."},{"key":"rf4","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(98)80020-7"},{"key":"rf5","doi-asserted-by":"crossref","unstructured":"A.\u00a0Enayat, Logic in Tehran, Lecture Notes in Logic\u00a026 (Association Symbolic Logic, La Jolla, CA, 2006)\u00a0pp. 87\u2013113.","DOI":"10.1201\/9781439865873"},{"key":"rf6","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71126-1"},{"key":"rf7","doi-asserted-by":"publisher","DOI":"10.1016\/j.jmaa.2005.04.039"},{"key":"rf8","doi-asserted-by":"publisher","DOI":"10.1111\/j.1746-8361.1958.tb01464.x"},{"key":"rf9","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1080938825"},{"key":"rf10","doi-asserted-by":"publisher","DOI":"10.2178\/bsl\/1140640945"},{"key":"rf11","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-017-1748-9_6"},{"key":"rf12","first-page":"1","volume":"91","author":"Kleene S. C.","journal-title":"Trans. Amer. Math. Soc."},{"key":"rf13","doi-asserted-by":"publisher","DOI":"10.1007\/s001530050104"},{"key":"rf14","doi-asserted-by":"publisher","DOI":"10.2307\/2586791"},{"key":"rf15","unstructured":"U.\u00a0Kohlenbach, Reverse Mathematics 2001, LectureNotes in Logic\u00a021 (Association for Symbolic Logic, La Jolla, CA, 2005)\u00a0pp. 281\u2013295."},{"key":"rf16","series-title":"Springer Monographs in Mathematics","volume-title":"Applied Proof Theory: Proof Interpretations and Their Use in Mathematics","author":"Kohlenbach U.","year":"2008"},{"key":"rf18","doi-asserted-by":"publisher","DOI":"10.1002\/(SICI)1521-3870(200001)46:1<17::AID-MALQ17>3.0.CO;2-8"},{"key":"rf19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-59971-2"},{"key":"rf20","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1978-0491103-7"},{"key":"rf22","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1294171005"},{"key":"rf23","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0066739"}],"container-title":["Journal of Mathematical Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S021906131250002X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,6]],"date-time":"2019-08-06T09:19:58Z","timestamp":1565083198000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/abs\/10.1142\/S021906131250002X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,6]]},"references-count":21,"journal-issue":{"issue":"01","published-online":{"date-parts":[[2012,7,8]]},"published-print":{"date-parts":[[2012,6]]}},"alternative-id":["10.1142\/S021906131250002X"],"URL":"https:\/\/doi.org\/10.1142\/s021906131250002x","relation":{},"ISSN":["0219-0613","1793-6691"],"issn-type":[{"value":"0219-0613","type":"print"},{"value":"1793-6691","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,6]]}}}