We investigate the strength of the existence of a non-principal
ultrafilters over fragments of higher order arithmetic.

Let (U) be the statement that a non-principal ultrafilter on N exists
and let ACA_0^w be the higher order extension of ACA_0 (arithmetical
comprehension).

We show that ACA_0^w+(U) is \Pi^1_2-conservative over ACA_0^w and thus
that ACA_0^w+(U) is conservative over PA.

Moreover, we provide a program extraction method and show that from a
proof of a strictly Pi^1_2 statement \forall f \exists g A_qf(f,g) in
ACA_0^w+(U)$ a realizing term in Gödel's system T can be extracted. This
means that one can extract a term t, such that \forall f A_qf(f,t(f)).