Ultrafilters in reverse mathematics (Q2878778)

The author extends the usual axiom systems of reverse mathematics by appending a predicate symbol \(\mathfrak U\) on sets, where the intended meaning of \(\mathfrak U (X)\) is that \(X\) is in the nonprincipal ultrafilter \(\mathfrak U\). The string \(\exists \mathfrak U\) denotes a list of axioms asserting that the sets satisfying \(\mathfrak U\) form a nonprincipal ultrafilter. The main result of paper shows that if \(T\) is one of the theories ACA\(_0\), ATR\(_0\), or \(\Pi^1_1\)-CA\(_0\), then the theory \(T + \exists \mathfrak U\) is a conservative extension of the theory \(T\). Since RCA\(_0 + \exists \mathfrak U\) implies ACA\(_0\), ACA\(_0\) is the appropriate base theory for this discussion. A property \(\mathfrak P\) of sets is \textit{divisible} if \(\mathbb N \in \mathfrak P\), \(\emptyset \notin \mathfrak P\), \((S\in \mathfrak P \land T \supseteq S)\to T \in \mathfrak P\), and \(S_0 \cup S_1 \in \mathfrak P \to (S_0 \in \mathfrak P \lor S_1 \in \mathfrak P)\). If \(T\) is one of the theories in the list above, \(\mathfrak P\) is an arithmetic property of sets, and \(T\) proves that \(\mathfrak P\) is divisible, then the theory \(T + \exists \mathfrak U + \mathfrak U \subset \mathfrak P\) (that is, \(T\) plus the assertion that there is a nonprincipal ultrafilter in which every element has property \(\mathfrak P\)) is a conservative extension of \(T\). The article concludes with a list of related conjectures and open questions.