It is well known that every Borel set has the property of Baire. That is, for every Borel set $B$, there is an open set $U$ and a sequence of dense open sets $D\_n$ such that for every $x\in \cap\_n D\_n$, $x\in B \iff x \in U$.


Also well known: every Borel set can be represented by a Borel code, a well-founded tree whose leaves encode open sets and whose inner nodes designate how to combine them (intersect, union, complement).


Taking a computability-theoretic view, it looks like starting from a Borel code $X$ of height $\alpha$, it will take about $\alpha$-many jumps of $X$ to compute open codes for such sets $U$ and $\{D\_n\}\_{n\in\omega}$.


Do you know of a reference where this (or the analogous fact, if I missed any detail) is already proved?


Similarly, is there any paper which has already analyzed the reverse math strength of the statement ``Every Borel set has the Property of Baire''?



Degree of unsolvability of finding a open approximation to a Borel set, given its Borel code
I think this is a well known fact.


For example, let $\alpha$ be a recursive ordinal and $B=\{g\mid g\mbox{ is a }0^{(\alpha)}\mbox{-generic real}\}$. Then $B$ is a hyperarithmetic set and so has a recursive Borel code $X$. 


But no real in $B$ is recursive in $0^{(\alpha)}$ and so any open approximation must not be recursive in $0^{(\alpha)}$.


