# "At most one" versus "at most finitely many"

As shown in Simpson's excellent Subsystems of Second Order Arithmetic, the ‘big five’ system ATR$$_0$$ from second-order reverse mathematics is equivalent to the following principle:

For arithmetical $$\varphi$$ such that $$(\forall n)(\exists \text{ at most one } X)\varphi(X, n)$$, there is $$Z$$ such that $$(\forall m)(m\in Z\leftrightarrow (\exists X)\varphi(X,m))$$.

My question is whether this ‘at most one’ comprehension principle is also equivalent to the following ‘at most finitely many’ principle, where $$w^{1^*}$$ is a finite sequence of sets of length $$\lvert w\rvert$$.

For arithmetical $$\varphi$$ such that $$(\forall n)(\exists w^{1^*})(\forall X)\Bigl[\varphi(X, n)\rightarrow (\exists i< \lvert w\rvert)(X=w(i))\Bigr],\tag{*}\label{star}$$ there is $$Z$$ such that $$(\forall m)(m\in Z\leftrightarrow (\exists X)\varphi(X,m))$$.

Note that the condition \eqref{star} guarantees that there are only finitely many $$X$$ satisfying $$\varphi(X,n)$$, for fixed $$n$$.

• A related phenomenon is the fact in set theory that a set is hereditarily ordinal definable if and only if it is hereditarily ordinal algebraic. (Algebraic means that the object has a property that only finitely many objects have.) See dx.doi.org/10.1215/00294527-3542326 Nov 20, 2022 at 14:08
• Another related phenomenon, which is classical and may have motivated the question, is that finite-to-one, or even countable-to-one, projections of Borel sets are Borel. Nov 20, 2022 at 14:31
• Is $|w|$ fixed here, or not? That is, should I read $(\ast)$ as saying $$(\exists l) (\forall n)(\exists w : [0,l-1] \to \mathbb N) (\forall X)\Bigl[\varphi(X, n)\rightarrow (\exists i< l )(X=w(i))\Bigr]\tag{*1}$$ or should I rather read it as saying $$(\forall n)(\exists l) (\exists w : [0,l-1] \to \mathbb N) (\forall X)\Bigl[\varphi(X, n)\rightarrow (\exists i< l )(X=w(i))\Bigr]\tag{*2}$$? (In either case I assume some coding is used to talk about having a function $w : [0,l-1] \to \mathbb N$.) Nov 23, 2022 at 14:45

The answer is positive, assuming extra induction, and a sketch is as follows.

Let $$\varphi(X,n)$$ be as in (*).

1. Define an analytic code $$A_n$$ as follows $$X\in A_n\leftrightarrow \varphi(X, n)$$.

2. Use induction (say for $$\Sigma_2^1$$-formulas) to show that $$A_n$$ can be enumerated (as a finite sequence).

3. Now use V.4.10 from Subsystems of Second-order Arithmetic to show that $$\cup_{n\in\mathbb{N}}A_n$$ can be enumerated, say by $$(X_m)_{m\in \mathbb{N}}$$.

4. Then for all $$n\in \mathbb{N}$$, we have

$$(\exists X\subset \mathbb{N})\varphi(X, n)\leftrightarrow (\exists m\in \mathbb{N})\varphi(X_m, n),$$ and we are done. Note that step 3. makes use of ATR$$_0$$.