How strong is “all sets are Lebesgue Measurable” in weaker contexts than ZF?

Famously, Solovay showed that, if $\textrm{ZFC}$ plus $\textrm{IC}$ (the existence of an inaccessible cardinal) is consistent, then so is $\textrm{ZF}$ plus $\textrm{DC}$ (dependent choice) plus $\textrm{LM}$ (all subsets of $\mathbb{R}$ are Lebesgue measurable). And Shelah showed that, conversely, the consistency of $\textrm{ZF}+\textrm{DC}+\textrm{LM}$ implies the consistency of $\textrm{ZFC}+\textrm{IC}$.

Since $\textrm{LM}$ is a statement of third-order arithmetic, it makes sense to consider it in theories weaker than $\textrm{ZF}$ set theory. I am curious what is known about the consistency strength of $\textrm{DC} + \textrm{LM}$ in such weaker contexts. Of specific interest to me is the consistency strength of $\textrm{DC}+\textrm{LM}$ over the base logic of a boolean topos (= higher-order classical logic).

-
So, if I'm not mistaken, your base theory is what is sometimes known as BZ: the usual axioms except no choice, no replacement and comprehension is limited to bounded formulas? – François G. Dorais Sep 10 '13 at 16:11
Is there a usual meaning for "Lebesgue measurable" in such general settings? Might some differing definitions, that are equivalent in ZF, not be provably equivalent in a weaker system? – Gerald Edgar Sep 10 '13 at 18:19
@GeraldEdgar: That's a risk but everything ought to work fine with dependent choice. – François G. Dorais Sep 10 '13 at 18:35
@GeraldEdgar: the usual development of measure theory, including the definition of Lebesgue measurability, goes through directly in higher-order logic + DC. Possibly, more subtle issues arise in weaker contexts. But I would prefer to focus the question on logical settings in which the development of measure theory does go through directly. – Alex Simpson Sep 10 '13 at 19:59
@FrançoisDorais: BZ, as you describe, is equiconsistent with the internal higher-order logic of a boolean topos, but the two are not identical. However, since the question is about consistency strength, the differences are a side issue here. So, by all means, consider the specific question of the last sentence to be about BZ. – Alex Simpson Sep 10 '13 at 20:13

The consistency of ZFC + IC is perhaps a little bit too much to ask, but I believe the next best thing is true:

Conjecture. Every boolean topos1 with dependent choice in which every set of reals is Lebesgue measurable contains a well-founded model of ZFC. In fact, every real is contained in a well-founded model of ZFC.

The proof that Con(ZF + DC + LM) implies Con(ZFC + IC) shows that in any model $V$ of ZF + DC + LM, $\aleph_1$ (of $V$) is an inaccessible cardinal in the constructible universe $L$ and therefore the inner model $L$ satisfies ZFC + IC. In fact, it shows that $\aleph_1$ is inaccessible in $L[a]$ for every real $a$ and therefore $L_{\aleph_1}[a]$ is a well-founded model of ZFC that contains $a$. I will now argue that we can still make sense of "$L_{\aleph_1}[a]$ is a well-founded model of ZFC that contains $a$" in a boolean topos with dependent choice and I will explain why I believe why this is true in a boolean topos with dependent choice in which all sets of reals are Lebesgue measurable.

Since there are no actual material sets around, we must first find a substitute. A boolean topos can still make sense of HC, the collection of all hereditarily countable sets, by amalgamating all countable well-founded extensional structures $(\mathbb{N},E)$. More precisely, one can show that any two such structures have at most one transitive embedding between them and that any two of them can be amalgamated into a third. (All that is needed for this is arithmetic transfinite recursion.) Then the limit of this directed system of countable well-founded extensional structures under transitive embeddings is the required HC.

Once we have HC, we can do a bit of set theory in there, thinking of its elements as actual material sets. In fact, assuming dependent choice, HC is a very nice model: it satisfies comprehension, replacement, choice and the basic combinatorial axioms but it doesn't have powersets, of course, since every set is countable. The ordinals of HC form a well-ordering that we will call $\aleph_1$. Working in HC, one can construct $L_\eta[a]$ for every $\eta \in \aleph_1$ and every $a \subseteq \omega$. Therefore, one can make sense of the substructure $L_{\aleph_1}[a]$ of HC, which is a well-founded model of a fragment of ZFC + $V = L[a]$ and the question whether $L_{\aleph_1}[a]$ is a model of ZFC makes sense.

The key ingredient that connects these ideas with Lebesgue measurability is the following theorem of Raisonnier:

Theorem. Assume ZF + DC. If there is an uncountable well-orderable subset of $\mathbb{R}$ then there is a non-measurable set of reals.

I don't know whether this goes through in a boolean topos with dependent choice. However, since this is a theorem of "ordinary mathematics," I conjecture that it does! The theorem does use some "fancy objects" such as rapid ultrafilters but these do make sense in a boolean topos and, in the presence of dependent choice, so does Lebesgue measure. I could be wrong, but I can't see any immediate obstructions to Raisonnier's Theorem in a boolean topos with dependent choice.

Now, the $a$-constructible reals $\mathbb{R}^{L[a]} = \mathbb{R}\cap L_{\aleph_1}[a]$ form a well-orderable set of reals since $L_{\aleph_1}[a]$ has a definable wellordering. Therefore, assuming that Raisonnier's Theorem goes through, in any boolean topos with dependent choice where all sets of reals are Lebesgue measurable, it must be the case that $\mathbb{R}^{L[a]}$ is countable for every $a \subseteq \omega$. Then, the usual argument that shows that $\aleph_1$ is inaccessible in $L[a]$ goes through to show that $L_{\aleph_1}[a]$ is a model of ZFC.

To summarize, at Alex's request, the above sketches a proof of the following:

Theorem. In a boolean topos with dependent choice where all well-orderable sets of reals are countable, every real is contained in a well-founded model of ZFC.

So the truth of the initial conjecture rests only on the truth of Raisonnier's Theorem in a boolean topos with dependent choice. Note that the conclusion is rather strong. Since the models are well-founded, all $\Sigma^1_2$ statements that are true in such models are also true in the ambient topos. In particular, every such topos proves that ZFC is not only consistent but also $\Sigma^1_2$-sound.

To get the relative consistency of ZFC+IC as in Shelah's Theorem, we would need to continue the construction of $L$ past $\aleph_1$ and show that this leads to a model of ZFC in the limit. It is unlikely that this is possible without some kind of additional completeness assumptions on the topos.

1For the sake of brevity, by "topos" I always mean "topos with a natural number object."

-
Thanks for this plausible answer. My own thoughts had proceeded along similar lines. There is certainly no problem defining $\textrm{HC}$. The construction of $L_\alpha [a]$ seems more delicate. Don't the transfinite stages need some replacement to define them? In "The Strength of Mac Lane Set Theory", Adrian Mathias managed to find a workaround for developing the constructible universe in a theory relatively consistent with BZ. Perhaps his techniques can be applied here. Though this is not a task I wish to carry out myself! – Alex Simpson Sep 10 '13 at 20:49
@AlexSimpson: This is a serious worry but it isn't for two reasons. The first is that we know exactly how much replacement is needed though that is unpublished work of Adrian Mathias and I. The second is that HC does satisfy replacement (in the internal sense) and that is more than enough to make that part work. Much of that is worked out in Simpson's Subsystems of second-order arithmetic under much weaker hypotheses. – François G. Dorais Sep 10 '13 at 22:12
@FrançoisDorais: Thanks for the clarification. I now need (perhaps considerable) time to think about your answer. Are you prepared to formulate your answer as an unequivocal assertion: if Raisonnier's Theorem holds in BZ+DC then Con(BZ+DC+LM) implies Con(ZFC)? What about the implication Con(ZFC) implies Con(BZ+DC+LM)? Thanks. – Alex Simpson Sep 11 '13 at 9:48
@AlexSimpson: Yes, that is the mathematical content of my answer, but note that the conclusion is much stronger than Con(ZFC). Also, I work in a boolean topos directly rather than in BZ, though it is true that BZ+DC+LM proves that ZFC has a well-founded model, modulo Raisonnier's Theorem, in the same manner. A converse is unlikely; Solovay's Theorem is the best upper bound that I know of. – François G. Dorais Sep 11 '13 at 10:10
@FrançoisDorais: I'm finally ticking your answer, having now gone through it in detail. Very nice! It would be good to have the remaining issues resolved some time. Does Raisonnier's Theorem go through in a boolean topos? (Just a matter of checking, but I don't have time for this right now.) More interestingly, in a boolean topos, does (something like) the existence of a well-founded model of ZFC imply the consistency of boolean toposes with LM+DC? – Alex Simpson Sep 13 '13 at 23:02