Can the fact that all analytic sets are Lebesgue measurable be proven in $Z_2$, or in some weak subsystem such as $\Pi^1_1\text{CA}_0$? Conversely, can certain set existence axioms be derived from the assumption that all analytic sets are Lebesgue measurable?
1 Answer
I believe $\Delta^1_2$CA$_0$ does indeed suffice; however, I don't see a way to pull this down to $\Pi^1_1$CA$_0$.
This is contrary to my previous claim; my error was with respect to the strength of the relevant choice principle.
Let me briefly outline the classical proof:
First, we show a version of Lebesgue regularity: that for any analytic set $A$, the outer measure of $A$ exists and that there is a $G_\delta$ (and hence measurable) set $B$ with $A\subseteq B\subseteq cl(A)$ and $m(X)=0$ for all measurable $X\subseteq B\setminus A$.
Next, let $A$ be an analytic set. Fixing a continuous function $f$ whose image is $A$, we let $A_\sigma$ be the image of $f$ restricted to the set of reals beginning with $\sigma$ (for $\sigma\in\omega^{<\omega}$) and we let $B_\sigma$ be the set corresponding to $A_\sigma$ per the bulletpoint above.
Looking to the $B_\sigma$s for a moment, it's not hard to show that for all $\sigma\in\omega^{<\omega}$, the set $$Z_\sigma:=B_\sigma\setminus\bigcup_{n\in\omega}B_{\sigma n}$$ is measurable and is contained in $B_\sigma\setminus A_\sigma$. But from this it follows that $Z_\sigma$ is null.
Elementary setjuggling shows that $$B\setminus A\subseteq\bigcup_{\sigma\in\omega^{<\omega}}Z_\sigma.$$ Since the union of countably many null sets is null, we have that $B\setminus A$ is measurable; since $B$ is measurable, this implies that $A$ is also measurable, and so we're done.
Now, translating this into the context of reverse mathematics, we run into three important points:
We need to talk about codes for sets of reals, rather than sets of reals themselves. Luckily, we're basically looking here at the first couple levels of the Borel hierarchy and at analytic sets, so we have reasonable coding notions.
We need to be able to do basic "setjuggling" with these codes. But this winds up being straightforward.
Finally, we need to be able to prove basic facts about Lebesgue measure: in particular, that the measurable (coded) sets are closed under countable Boolean combinations and that the union of countably many null sets is null. This is the difficult bit: it involves choosing "nearly optimal" covers in a concrete way: e.g. to show that $\bigcup_{n\in\omega} X_n$ is null if each $X_n$ is null, we really want a sequence $(\mathcal{O}_{n,k})_{n,k\in\omega}$ such that $\mathcal{O}_{n,k}$ is an open cover of $X_n$ with total measure ${1\over k+1}$. When the $X_n$s are given uniformly by analytic codes  as in our situation here  the set of legal choices for $\mathcal{O}_{n,k}$ is a nonempty $\Pi^1_1$ set uniformly in $n,k$.
So the question now is: how strong is $\Pi^1_1$ choice? Unfortunately (and contra my original claim) it turns out that it is rather strong indeed. In fact, it is equivalent to $\Delta^1_2$CA$_0$; this follows from Theorem VII.$6.9(1)$, page $298$, in Simpson's book together with Carl's observation that $\Pi^1_1$choice is equivalent to $\Sigma^1_2$choice.
So the above argument gives a proof of the result in a weakbutnottooweak subsystem of Z$_2$.

2$\begingroup$ $\Pi^1_1$choice was the only thing outside of ATR$_0$ that proof uses, right? Is $\text{ATR}_0+\Pi^1_1\text{choice}$ strictly weaker than $\Pi^1_1\text{CA}_0$? $\endgroup$ Nov 14, 2018 at 21:00

$\begingroup$ @AlexMennen Yes, that's right (although I can't rule out the possibility of avoiding $\Pi^1_1$AC via cleverness, of course). As to your second question, I think the answer is yes, but annoyingly I can't find any sources on it! I'll do a more serious literature dive tomorrow (or, y'know, try it myself). $\endgroup$ Nov 14, 2018 at 23:49

$\begingroup$ @CarlMummert Crud, you're right  and $\Sigma^1_2$ choice is stronger than $\Pi^1_1$CA$_0$. Edited! $\endgroup$ Nov 15, 2018 at 17:06

1$\begingroup$ Why $\Pi^1_1$CA is not sufficient? You just need to prove that every $\Pi^1_1$set is measurable. To prove this, you need to prove that the set $\omega_1^x=\omega_1^{CK}$ has measure 1 and then prove every Borel set is measurable. $\endgroup$– 喻 良Nov 16, 2018 at 0:42

1$\begingroup$ @AlexMennen There is a natural "rank" function $e_A:\mathbb{R}\rightarrow \omega_1\cup\{\infty\}$ associated to a $\Pi^1_1$ set $A$, given by sending $r$ to the rank of the tree $T_r$ corresponding to the question "$r\in A?$" (where this rank is $\infty$ iff $r\not\in A$). The key point now is that we always have $$e_A(r)<\infty\iff e_A(r)<\omega_1^{CK}(r),$$ and hence for measure$1$ many $r$s we have $r\in A\iff e_A(r)<\infty\iff e_A(r)<\omega_1^{CK}$. The set $\{r: e_A(r)<\omega_1^{CK}\}$ is Borel, hence measurable. $\endgroup$ Nov 19, 2018 at 4:04