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

62 Views Asked by At

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

1

There are 1 best solutions below

3
On BEST ANSWER

I assume that you refer to Exercise 27.14 in Kanamori's book. In that case, the answer will be rather disappointing:

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.

This doesn't answer the lightface question, though. I'll take a look at that later.