The difference between Baire 2 and 'effectively Baire 2'

Question

In short: Baire 2 functions are often assumed to be given by a double sequence of continuous functions, thought this is not the exact definition. Does one need the Axiom of Choice (or related) to connect these two definitions?

Longer version: we are working over the real numbers. As is well-known, Baire 0 functions are the continuous ones, while Baire $n+1$ functions are the pointwise limits of Baire $n$ functions.

I call a function $f$ from reals to reals effectively Baire 2 in case it is the double limit of a double sequence $(f_{n,m})_{n, m \in \mathbb{N}}$, i.e. for all reals $x$, we have $$ (\forall \epsilon>0)(\exists n'\in \mathbb{N})(\forall n> n')(\exists m'\in \mathbb{N})(\forall m>m')( |f_{m,n}(x)-f(x)|<\epsilon). \qquad (*) $$ As pointed out by Baire himself already, Baire 2 functions can be represented by effectively Baire 2 functions, though Baire did not use the latter terminology.

The notion (*) is essentially the definition of Baire 2 used in reverse mathematics/second-order arithmetic.

My question is then whether one needs the Axiom of Choice (or related) to show that for a general Baire 2 function, there is a double sequence satisfying (*).

Answer 1

It's provable in ZF that every Baire-2 function is effectively Baire-2. It suffices to prove the following:

(ZF) There is an explicit function which maps each Baire-1 function $f: \mathbb{R} \rightarrow \mathbb{R}$ to a sequence of rational polynomials that pointwise converge to it.

The first step is to construct a sequence of reals $\langle r_n \rangle$ such that each $r_n$ codes a rational-valued function $f_n$ such that $|f_n(x)-f(x)| \le \frac{1}{n}$ for all $x \in \mathbb{R}.$ We'll construct $r_1,$ which immediately generalizes to other $n.$

Let $U_k$ enumerate the basic open sets. We use transfinite recursion to define a descending sequence of closed sets $\langle C_{\alpha}: \alpha<\omega_1 \rangle$:

1. $C_0=\mathbb{R},$
2. $C_{\alpha+1}=C_{\alpha} \setminus \bigcup \{U_k: \forall x, y \in C_{\alpha} \cap U_k (|f(x)-f(y)|\le 1)\},$
3. For limit $\alpha,$ $C_{\alpha}=\cap_{\xi<\alpha} C_{\xi}.$

If $C_{\alpha} \neq \emptyset,$ then $f \restriction_{C_{\alpha}}$ is continuous at some $x \in C_{\alpha}$ by Baire's Characterization Theorem. Then $x \not \in C_{\alpha+1},$ so $C_{\alpha+1} \subsetneq C_{\alpha}.$ Define a surjective partial map $g: \omega \rightharpoonup\beta = \{\alpha: C_{\alpha} \neq \emptyset\}$ by sending $k$ to the greatest $\alpha$ such that $U_k \cap C_{\alpha} \neq \emptyset,$ and a well-founded partial ordering $(\omega, \prec)$ by $i \prec j$ if $g(i) < g(j).$ Define $h: \text{dom}(g) \rightarrow \mathbb{Z}$ by $h(k)=\lfloor \sup_{U_k \cap C_{g(k)}} f \rfloor.$

Define $f_1: \mathbb{R} \rightarrow \mathbb{Z}$ as follows: for given $x,$ let $j=\min\{k<\omega: x \in U_k \wedge \forall \alpha (x \in C_{\alpha} \leftrightarrow U_k \cap C_{\alpha} \neq \emptyset)\}.$ Set $f_1(x) = h(j).$

Let $r_1$ be a real which encodes $(\omega, \prec)$ and $h.$ From $(\omega, \prec),$ one can determine the sequence $\langle C_{\alpha}\rangle$ and hence $g.$ Thus, $f_1$ can be determined from $r_1.$ This completes the construction of $r_1$ (and hence all $r_n$).

Let $r$ encode $\langle r_n \rangle$ (and thus $f$). By Shoenfield absoluteness relativized to $r,$ we have in $L[r]$ that $r$ encodes a Baire-1 function $\hat{f}.$ Enumerate the rational polynomials by $\langle q_n \rangle.$ A Stone-Weierstrass argument shows that there is $\langle n_k \rangle$ such that $\langle q_{n_k} \rangle$ converges pointwise to $\hat{f}$ in $L[r].$ Let $\langle n_k \rangle$ be the $L[r]$-least such sequence. Applying Shoenfield absoluteness upwards relative to a real encoding $(r, \langle n_k \rangle),$ we see in $V$ that $\langle q_{n_k} \rangle$ converges pointwise to the Baire-1 function coded by $r,$ namely $f.$ This completes the construction.

Some additional remarks: The above construction can be carried out in $Z_2.$ I don't know enough about subsystems of analysis to say more with confidence. By analyzing how much of $L[r]$ is really needed in the above, you can probably get this down to $\Pi^1_1-CA_0.$

As I showed in the comments, it is not provable in ZF that every Baire-3 function is effectively Baire-3, since if $\mathbb{R}$ is a countable union of countable sets, then every indicator function is Baire-3.