An interesting topic in Reverse Mathematics is uniformisation theorems (see VI.2 and VII.6 in Simpson's SOSOA). Now, these theorems all express the following: for a suitable formula $\varphi$, there is a formula $\psi$ (of the same complexity) such that $(\exists X\subset \mathbb{N})\varphi(X) \leftrightarrow (\exists Y\subset \mathbb{N})\psi(Y)$ and where there is at most one $Z\subset \mathbb{N}$ such that $\psi(Z)$.
Plainly put, we can (equivalently) replace an existential quantifier by an existential quantifier with an "at most condition". However, the uniformisation theorems for $\Sigma_3^1$-formulas and beyond (see V.II.6.15 in SOSOA) all have certain extra set-theoretic assumptions. In this light, my question is as follows:
Are there ‘weaker’ uniformisation theorems with the following properties:
these theorems state that existential quantifiers can be equivalently replaced by existential quantifiers that come with an “at most finitely/countably many” condition.
these theorems are provable in weaker systems and/or without set-theoretic assumptions.
