So this question of mine arises from the hint of an exercise in Kanamori's "The Higher Infinite", where we try to prove that $\operatorname{Det}(\Pi^1_n)$ implies the Baire property, perfect set property and Lebesgue measurability for $\Sigma^1_{n+1}$ sets.
First assume $\langle s_i : i<\omega\rangle$ is a $\Delta^0_0$ enumeration of $^{<\omega}\omega$ and that for any $s\in {^{<\omega}\omega}$, $O_s = \{x\in {^\omega\omega}: s \subseteq x\}.$
Assume $A$ is $\Sigma^1_{n+1}$. And let, $$O_A = \bigcup\{ O_s: O_s - A \text{ is meager}\}.$$ I want to show that $B = A - O_A$ is also $\Sigma^1_{n+1}$.
The most natural thing to do now would be to prove that $O_A$ is at most $\Pi^1_{n+1}$. At first we have:
$$O_A(x)\leftrightarrow \exists^0i(O_{s_i} - A \text{ is meager } \land x \in O_{s_i})$$
Now the only troublesome part is the "$O_{s_i} - A \text{ is meager }$" part.
The only way I know of to translate this to arithmetic, would be to use a game theoretic equivalent statement, mainly that the second player has a winning strategy for $G^{**}_\omega(O_{s_i} - A)$, where each player plays a finite sequence of natural numbers and the first player wins if the infinite concatenation is in the above set, otherwise the second player wins. But this approach has a problem. It starts with asserting the existence of a winning strategy, which isn't what we want, since we want the above assertion to be $\Pi^1_{n+1}$.
So my question is, how do we render "$O_{s_i} - A \text{ is meager }$" as a $\Pi^1_{n+1}$ formula, knowing that $A$ is $\Sigma^1_{n+1}$?
