On idempotent ultrafilters in higher-order reverse mathematics

TL;DR

This paper investigates the logical strength of the existence of idempotent ultrafilters within higher-order reverse mathematics, establishing implications and conservativity results related to Hindman's theorem.

Contribution

It demonstrates that the existence of idempotent ultrafilters implies the iterated Hindman's theorem in higher-order reverse mathematics and shows their logical equivalence over certain systems.

Findings

(Uidem) implies IHT over ACA_0^w

ACA_0^w + (Uidem) is Pi^1_2-conservative over ACA_0^w + IHT

The results clarify the logical strength of ultrafilter existence in higher-order systems

Abstract

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_0^w, the higher-order extension of ACA_0, the statement (Uidem) implies the iterated Hindman's theorem (IHT), and we show that ACA_0^w + (Uidem) is Pi^1_2-conservative over ACA_0^w + IHT and thus over ACA_0^+.