# Writing down a formula for "X is meager" in second order arithmetic with low complexity

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}$$?

All the notions there are actually boldface, hence it is only necessary to see that $$A - O_A$$ is $$\boldsymbol\Sigma_{n+1}^{1}$$, which is immediate by the assumption on $$A$$ since $$O_A$$ is just open.
• Oh! :) Thanks! Also if they were all lightface, again we could code everything relative to some real that codes the opens that cover $O_A$, I guess. Right? Mar 12, 2020 at 15:46
• @ShervinSorouri I agree. At the moment I don't know if there's a trick to code $O_A$. Mar 12, 2020 at 16:38