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 (\*).



The difference between Baire 2 and 'effectively Baire 2'
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.


