In (second-order) Reverse Mathematics, a (code for an) open set $U\subset \mathbb{R}$ is given by two sequences of rationals $(a_n)_{n \in \mathbb{N}}, (b_n)_{n \in \mathbb{N}}$. The idea is that $U$ is represented by the union $\cup_n (a_n, b_n)$. A closed set is the complement of an open set.
Suppose I have a (code for a) closed set $C\subset [0,1]$ which is finite as follows:
$$
\text{there is $N\in \mathbb{N}$ such that for any pairwise distinct $x_0, \dots, x_N \in [0,1]$, there is $i\leq N$ with $x_i\not \in C$ }
$$
Clearly, such finite $C$ has measure zero (in the sense of second-order Reverse Mathematics; see X.1 in Simpson's excellent SOSOA).
My question is in what system we can actually prove that such finite $C$ has measure zero? It would be strange if ATR$_0$ would be needed, for instance. Any related results from (Turing) computability theory are welcome too.
Best Answer
Here's a proof that $\mathsf{ACA}_0$ suffices for the analogous statement over $2^\mathbb{N}$ instead of $\mathbb{R}$, where codes for closed sets are viewed as subtrees of $2^{<\mathbb{N}}$; it's a bit tedious, but not difficult, to port this over to $\mathbb{R}$ (the key point being that there is a very-nicely-definable 2-to-1 continuous surjection $2^\mathbb{N}\rightarrow[0,1]$):
Suppose $T$ is a subtree of $2^{<\mathbb{N}}$, coding a closed set $C$ with the desired property. By arithmetic comprehension we can assume $T$ has no dead ends. Now say that a good sequence is a finite sequence $\sigma=(x_i)_{i<n}$ such that each $x_i$ is a node on $T$ and if $i<j<n$ then $x_i$ and $x_j$ are incompatible. By the condition on $C$ and the lack of dead ends in $T$, we can uniformly extend each node in $T$ to an element of $C$ ("leftmost extension"), and so we get the analogue of your condition for nodes on $T$ rather than paths: there is some $N$ such that there is no good sequence of length $\ge N$.
Now consider the set of lengths of good sequences. This is arithmetically definable, so by arithmetic induction and the role of $N$ above it has some largest element. If $\sigma$ is a maximal-length good sequence, then the set of leftmost paths extending elements of $\sigma$ is finite and is all of $C$.
On the other hand, $\mathsf{RCA}_0+\mathsf{I}\Sigma^1_1$ also suffices (that is, this finiteness principle has no inherent "effective content"): without even bother to switch to Cantor space, just look at the set of $n$ such that there exists a sequence of distinct elements of $C$ of length $n$. This is a $\Sigma^1_1$ set which is bounded, so it has a greatest element and this gives rise to the finiteness of $C$ as desired.
On the other other hand, it is not obvious to me that $\mathsf{RCA}_0+$ arithmetic induction suffices; arithmetic comprehension was crucially used above in pruning $T$.