Here is an interpretation of "measurable set" and "measurable function" that indeed yields closure under addition.
For $A\subseteq\Bbb R$, $r\in[0,\infty]$, let $I_A^r$ be the set of functions $f:\Bbb N\to\Bbb R^2$ such that $f_1(n)\le f_2(n)$, $A\subseteq\bigcup_n [f_1(n),f_2(n)]$, and $\sum_n(f_2(n)-f_1(n))\le r$. This is the set of countable closed interval covers of $A$ of total size $\le r$.
The outer volume is defined as $\lambda^*(A)=\inf\{r\mid I_A^r\ne\emptyset\}$. There are no changes here besides giving the interval covers a name. Clearly this satisfies the identity $$\lambda^*(A)\le r\iff\forall x, f\in I_A^x:x\le r,$$ and in particular $f\in I_A^r$ implies $\lambda^*(A)\le r$.
An outer volume witness, denoted $f\in[\lambda^*(A)\le r]$, is a member of $\prod_{r<x<\infty}I_A^x$. That is, it is a function which associates to every $r<x<\infty$ some $f(x)\in I_A^x$.
- The empty function is an outer volume witness for $[\lambda^*(A)\le \infty]$.
- If $f\in I_A^r$, then the constant function $x\mapsto f$ is in $[\lambda^*(A)\le r]$.
- As the notation suggests $f\in[\lambda^*(A)\le r]$ implies $\lambda^*(A)\le r$.
- Conversely, if we assume countable choice $[\lambda^*(A)\le \lambda^*(A)]$ is nonempty for every $A$.
There is an analogue of countable additivity for witnesses. If $(f_n),(A_n),(r_n)$ are sequences such that $f_n\in[\lambda^*(A_n)\le r_n]$, then there is a definable term $g\in[\lambda^*(\bigcup_nA_n)\le \sum_nr_n]$. More precisely, if $\sum_nr_n=\infty$ we can use the empty function, otherwise we can take $g(x,n)=f_{j_1(n)}\left(r_{j_1(n)}+\frac{x-\sum_ir_i}{2^{j_1(n)}},j_2(n)\right)$ where $j:\Bbb N\to\Bbb N^2$ is a fixed bijection.
A measurability witness $f\in[A\in{\cal L}]$ is a member of $$\prod_{E\subseteq\Bbb R}\prod_{x\in\Bbb R}\prod_{g\in I_A^x}\prod_{y\in(x,\infty)}\bigcup_{t\in\Bbb R}(I_{A\cap E}^t\times I_{A\setminus E}^{y-t}).$$ In other words, for each test set $E\subseteq\Bbb R$, $x\in\Bbb R$, and an interval covering $g\in I_A^x$, plus a "wiggle factor" $y>x$, the witness provides coverings $f_1(E,x,g,y)\in I_{A\cap E}^t$ and $f_2(E,x,g,y)\in I_{A\setminus E}^{y-t}$ for some $t$. (To be fully "constructive" here we could use a sigma type for $t$, that is a disjoint union instead of a regular union, but it's not necessary to keep track of $t$ here.)
Put together, these witnesses establish $\lambda^*(A\cap E)\le t$ and $\lambda^*(A\setminus E)\le y-t$, so that $\lambda^*(A\cap E)+\lambda^*(A\setminus E)\le y$. Since this is true for every $y>x$, we have $\lambda^*(A\cap E)+\lambda^*(A\setminus E)\le x$. This is valid for any $x$ for which an interval covering $g\in I_A^x$ can be provided, which is the case for all $x>\lambda^*(A)$. Thus $\lambda^*(A\cap E)+\lambda^*(A\setminus E)\le \lambda^*(A)$, and since the reverse inequality is a result of finite subadditivity of $\lambda^*$, we have $\lambda^*(A)=\lambda^*(A\cap E)+\lambda^*(A\setminus E)$, so $A\in{\cal L}$ under the Carathéodory definition.
Rather than the Carathéodory definition, we will use witnesses to define measurability. That is, we say $A$ is measurable and write $A\in{\cal L}$ if $[A\in{\cal L}]$ is nonempty. This is a fairly significant deviation from the standard definition, because one needs full choice (or at least choice on families of size $2^\frak c$) to establish that $\lambda^*(A)=\lambda^*(A\cap E)+\lambda^*(A\setminus E)$ implies $A\in{\cal L}$.
The standard facts about measurable sets translate readily to this framework. There are definable terms $F,G$ such that $f\in[A\in{\cal L}],g\in[B\in{\cal L}]$ implies $F(f)\in[\Bbb R\setminus A\in{\cal L}]$ and $G(f,g)\in[A\cup B\in{\cal L}]$, and given a countable sequence $f_n\in[A_n\in{\cal L}]$, we have $H(f)\in[\bigcup_nA_n\in{\cal L}]$ (and we also have $\lambda(\bigcup_nA_n)=\sum_n\lambda(A_n)$ if the $A_n$ are disjoint).
Finally, we have the definition of measurable function. A measurable function witness $w\in[f:{\cal L\to B}]$ is a member of $\prod_{O\in\tau}[f^{-1}(O)\in{\cal L}]$, where $\tau$ is the topology of $\Bbb R$ (so $O$ is an open set). Equivalently we can let the product range only over elements of the form $(a,\infty)$. A function is measurable, $f:{\cal L\to B}$, if $[f:{\cal L\to B}]$ is nonempty.
By keeping everything "constructive", the problems of selecting interval sequences goes away. The proof of the sum of measurable functions is a special case of the following:
Theorem: If $f,g$ are measurable functions and $\ast:\Bbb R^2\to\Bbb R$ is a continuous binary function, then the function $f\ast g$ defined by $(f\ast g)(x)=f(x)\ast g(x)$ is measurable.
Proof: Given witnesses $u\in[f:{\cal L\to B}],v\in[g:{\cal L\to B}]$, let $O$ be an open set. Then $\ast^{-1}(O)$ is an open subset of $\Bbb R^2$. Fix a countable basis $\cal B$ for $\Bbb R$ (for example, open intervals with rational), so that ${\cal B}^2$, the set of rectangles in $\cal B$, is a countable basis for $\Bbb R^2$, and let $(B_n)_n=(B_n^1\times B_n^2)_n$ enumerate the elements of the basis. Let $C_n=f^{-1}(B_n^1)\cap g^{-1}(B_n^2)$ if $B_n\subseteq O$, otherwise $C_n=\emptyset$; then we can define $w_n\in[C_n\in{\cal L}]$ in terms of $u,v$, and hence also $p\in[\bigcup_nC_n\in{\cal L}]$. Since $\bigcup_nC_n=(f\ast g)^{-1}(O)$, this proves that $f\ast g$ is measurable.
