Weak weak Koenig's lemma (WWKL for short) is defined in Chapter X of Simpson's SOSOA as follows:
if a binary tree has positive measure, then it has a path.
I am interested in $\Sigma_1^1$-WWKL, i.e. WWKL generalised to $\Sigma_1^1$-trees. Does ACA$_0$ prove $\Sigma_1^1$-WWKL?
To be absolutely clear, by $\Sigma_1^1$-WWKL, I mean the usual statement of WWKL in which elementhood in the tree as in `$\sigma\in T$' is given by a $\Sigma_1^1$-formula $\varphi_T(\sigma)$.
ACA$_0$ does not appear to be strong enough to make sense of "positive measure" as the tree is given by a $Σ^1_1$ formula rather than a set. However, if we also assume $Σ^1_1$ induction, then we get bounded $Σ^1_1$ comprehension, and thereby positive measure makes sense.
In any case, $Σ^1_1$-WWKL fails in the minimal $ω$-model of ACA; and "there is a non-arithmetic real" is a $Σ^1_2$ statement provable in ACA + $Σ^1_1$-WWKL but not in ACA. (Recall that ACA is ACA$_0$ with full induction.)
To see this, choose a reasonable enumeration $x$ of arithmetic subsets of $ω$ (reals), e.g. enumerate arithmetic formulas and pick those that define a real not defined previously (but repeating some reals also works for us). The enumeration will not exist as a set in the minimal $ω$-model of ACA, but is defined by a $Δ^1_1$ formula. Define the 0-1 $Σ^1_1$ tree $T$ as $s∈T$ iff for every odd length prefix $t$ of $s$, $t$ does not agree with $x_{\lfloor |t|/2 \rfloor}$. By construction, and regardless of what $x$ is, $T$ is positive measure, but there is no path through $T$ that was enumerated in $x$.
Despite the above failure of conservativity, a random real provides a path with positive probability. Thus, I expect that by forcing to add random reals, ACA + $Σ^1_1$-WWKL is $Π^1_1$ conservative over ACA.
