On idempotent ultrafilters in higher-order reverse mathematics

الأصل · EN

We analyze the strength of the existence of idempotent ultrafilters in higher-order reverse mathematics. Let (Uidem) be the statement that an idempotent ultrafilter on the natural numbers exists. We show that over ACA₀ʷ, the higher-order extension of ACA₀, the statement (Uidem) implies the iterated Hindman's theorem (IHT), and we show that ACA₀ʷ + (Uidem) is Pi¹₂-conservative over ACA₀ʷ + IHT and thus over ACA₀+.