It is known that the following form of $\Pi^1_1$-uniformization is equivalent to $\Pi^1_1$-Comprehension over $\mathsf{ATR}_0$ (cf. VI.2.6 of Simpson's book) :
(Kondo's uniformization theorem) For each $\Pi^1_1$-formula $\psi(X,Y)$, we can find another $\Pi^1_1$ formula $\hat{\psi}(X,Y)$ such that the following holds:
- $\forall X,Y [\hat{\psi}(X,Y)\to\psi(X,Y)].$
- $\forall X, Y, Z [\hat{\psi}(X,Y)\land \hat{\psi}(X,Z)\to Y=Z]$.
- $\forall X, Y [\psi(X,Y) \to \exists Z \hat{\psi}(X,Z)]$.
Question. Is the following form of $\Pi^1_1$-uniformization equivalent to $\Pi^1_1$-Comprehension over $\mathsf{ATR}_0$, or provable from a weaker subsystem like parameter-free $\Pi^1_1$-comprehension or $\mathsf{ATR_0}$ plus $\Pi^1_1$-Transfinite Induction?
(Uniformization for a unary lightface $\Pi^1_1$ formula) For each $\Pi^1_1$-formula $\psi(X)$ with all free variables displayed, we can find another $\Pi^1_1$ formula $\hat{\psi}(X)$ (also, with all free variables displayed) such that the following holds:
- $\forall X [\hat{\psi}(X)\to\psi(X)].$
- $\forall X, Y [\hat{\psi}(X)\land \hat{\psi}(Y)\to X=Y]$.
- $\forall X [\psi(X) \to \exists Y \hat{\psi}(Y)]$.
The usual proof for the $\Pi^1_1$-uniformization theorem (one using scales for $\Pi^1_1$ sets, also provided in Simpson's book) proves Kondo's uniformization theorem, so the usual proof always requires $\Pi^1_1$-Comprehension. Simpson's proof of $\Pi^1_1$-Comprehension from Kondo's uniformization theorem seems to heavily use the uniformization for binary relations, so I do not see if the $\Pi^1_1$-uniformization for unary formula implies the existence of, for example, the hyperjump of $0$.
