I would like to know if the Reverse Mathematics has a conclusion for this axiom ($\text{LM}$:Every set of $\mathbb{R}$ is Lebesgue measurable).

I have tried to translate this axiom into a halting problem like $\text{LPO}$, but without success.

  • $\begingroup$ I asked a related problem on MO a while ago, and am still interested. But could you first clarify your base theory? I assume it's something like intuitionistic ZF or weaker $\endgroup$
    – Lxm
    Dec 23, 2022 at 22:53
  • $\begingroup$ @Lxm If, like me, you are just looking for the halting problem form of this axiom (LM), or want to find an ordinal $\alpha$ such that $WF_\alpha\models Con(IZF+LM)$, then IZF is enough. If you want to do reverse mathematical research, then you need to use KP as the ground model. If you're searching for a constructive interpretation of the LM, then you need MLTT(Martin-Löf Type Theory). If you are prepared to work on a constructive model of the real analysis, just use Cubical Agda. $\endgroup$ Dec 24, 2022 at 16:56
  • $\begingroup$ @Lxm I doubt that neither here nor MO can solve our problem. Probably need to move the problem to cs.stackexchange, cstheory.stackexchange or proofassistants.stackexchange. $\endgroup$ Dec 24, 2022 at 17:00
  • 1
    $\begingroup$ First, how do you define the Lebesgue measurability in a constructive manner? The standard definition of Lebesgue measurability relies on Borel sets, whose formulation heavily relies on LEM. There are some ways to avoid this, like, using the formulation by Bishop. Your question could be meaningless unless you provide a formulation of Lebesgue measurability over the background theory you want to analyze. $\endgroup$
    – Hanul Jeon
    Dec 29, 2022 at 3:56
  • $\begingroup$ Second, your comment suggests your understanding of logic needs improvement. What is $\mathsf{WF}_\alpha$? $\mathsf{IZF+LEM}$ is $\mathsf{ZF}$, so why do you use $\mathsf{IZF+LEM}$? Also, you mixed up models with theories, which are completely different notions. And, what is the relationship between LEM and the halting problem? $\endgroup$
    – Hanul Jeon
    Dec 29, 2022 at 3:59


You must log in to answer this question.