NON-PRINCIPAL ULTRAFILTERS, PROGRAM EXTRACTION AND HIGHER ORDER REVERSE MATHEMATICS
Alexander Kreuzer · 2013
Abstract. We investigate the strength of the existence of a non-principal ultrafilter over fragments of higher order arithmetic. Let (U) be the statement that a non-principal ultrafilter on N exists and let ACAω 0 be the higher order extension of ACA0. We show that ACAω 0 + (U) is Π1 2-conservative over ACAω 0 and thus that ACAω 0 + (U) is conservative over PA. Moreover, we provide a program extraction method and show that from a proof of a strictly Π1 2 statement ∀f ∃g Aqf(f, g) in ACAω 0 + (U) 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 Aqf(f, t(f)). In this paper we will investigate the strength of the existence of a non-principal ultrafilter over fragments of higher order arithmetic. We will classify the consequences of this statement in the spirit of reverse mathematics. Furthermore, we will provide a program extraction method. Let (U) be the statement that a non-principal ultrafilter on N exists. Let RCA ω 0, ACA ω 0 be the extensions of RCA0 resp. ACA0 to higher order arithmetic as introduced