Filters on computable posets (Q2372682)

This paper studies filters in posets from the viewpoint of computable mathematics. A filter in a poset \((P, {\preceq})\) is an upward closed set \(F \subseteq P\) such that \(\forall p,q \in F\, \exists r \in F (r \preceq p \land r \preceq q)\). A filter which is not properly included in another filter is \textsl{maximal}. The filter \(F\) is unbounded if \(\forall p \notin F\, \exists q \in F\, p \npreceq q\). Obviously every maximal filter is unbounded. It turns out that every computable poset has a \(\Delta^0_2\) maximal filter. On the other hand the authors construct a computable poset with no \(\Sigma^0_1\) or \(\Pi^0_1\) maximal filters, and a computable poset \((P, {\preceq})\) such that if \(F \subseteq P\) is a maximal filter then \(F\) computes the halting problem. It is also shown that every computable poset has a \(\Sigma^0_1\) unbounded filter, and that there exist computable filters without \(\Pi^0_1\) unbounded filters and such that every unbounded filter computes the halting problem. From the reverse mathematics viewpoint (\textit{S. G. Simpson}'s book [Subsystems of second order arithmetic. Berlin: Springer (1999; Zbl 0909.03048)] is the main reference), these results imply that each of the statements ``every poset has a maximal filter'' and ``every poset has an unbounded filter'' is equivalent to \textbf{ACA}\(_0\) over the base theory \textbf{RCA}\(_0\). The paper includes a few more results of the same kind.