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$:

- $C_0=\mathbb{R},$
- $C_{\alpha+1}=C_{\alpha} \setminus \bigcup \{U_k: \forall x, y \in C_{\alpha} \cap U_k (|f(x)-f(y)|\le 1)\},$
- 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.

iseffectively Baire class 3 so there's no contradiction there. However, using the effective perfect set theorem you can get a contradiction if you have a countable union of countable sets whose cardinality is neither countable nor continuum. $\endgroup$1more comment