CONSERVATIVITY OF ULTRAFILTERS OVER SUBSYSTEMS OF SECOND ORDER ARITHMETIC

We extend the usual language of second order arithmetic to one in which we can discuss an ultrafilter over of the sets of a given model. The semantics are based on fixing a subclass of the sets in a structure for the basic language that corresponds to the intended ultrafilter. In this language we state axioms that express the notion that the subclass is an ultrafilter and additional ones that say it is idempotent or Ramsey. The axioms for idempotent ultrafilters prove, for example, Hindman's theorem and its generalizations such as the Galvin-Glazer theorem and iterated versions of these theorems (IHT and IGG). We prove that adding these axioms to IHT produce conservative extensions of ACA(0)+IHT, ACA(0)(+), ATR(0), pi(1)(2)-CAO, and pi(1)(2)-CAo for all sentences of second order arithmetic and for full Z(2) for the class of sentences pi(1)(4). We also generalize and strengthen a metamathematical result of Wang (1984) to show, for example, that any pi(1)(2) theorem for all X there exists Y Theta(X, Y) provable in ACA(0) or ACA(0)(+) there are e,k is an element of N such that ACA(0) or ACA(0)(+) proves that root x(Theta(x,Phi(e) (J((k)) (X))) where Phi(e) is the eth Turing reduction and J((k)) is the kth iterate of the Turing or Arithmetic jump, respectively. (A similar result is derived for pi(1)(3) theorems of pi(1)(1)-CA(0) and the hyperjump.).