Non-principal ultrafilters, program extraction and higher order reverse mathematics
arXiv:1109.4277 · doi:10.1142/S021906131250002X
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 exists and let ACA_0^ω be the higher order extension of ACA_0. 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 \forall f \exists g A(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, such that A(f,t(f)).