Non-principal ultrafilters, program extraction and higher-order reverse mathematics

Journal of Mathematical Logic 12 (1):1250002- (2012)
  Copy   BIBTEX


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 ℕ exists and let [Formula: see text] be the higher-order extension of ACA0. 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 ∀ f ∃ g A qf in [Formula: see text] a realizing term in Gödel's system T can be extracted. This means that one can extract a term t ∈ T, such that ∀ f A qf).



    Upload a copy of this work     Papers currently archived: 76,363

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles


Added to PP

25 (#465,850)

6 months
1 (#451,971)

Historical graph of downloads
How can I increase my downloads?