Carathéodory Measurable Sets of an Outer Measure

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $X$ be a set, let $\mathcal{P}(X)$ be its power set, whose elements are exactly the subsets of $X$, and let $\mu^{*}$ be an outer measure on $X$, a map $\mu^{*}:\mathcal{P}(X)\to[0,\infty]$ with $[0,\infty]$ as in The Extended Real Line, Its Order, and [0,∞] (ii). Let $+$ be the sum on $[0,\infty]$, and let $A\cap E$ and $A\setminus E$ be the intersection and difference of sets $A$ and $E$. For $A,E\in\mathcal{P}(X)$, $A\cap E$ and $A\setminus E$ are subclasses of $A$, hence sets by Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper (i), and subsets of $X$; so they lie in $\mathcal{P}(X)$, and $\mu^{*}(A\cap E)+\mu^{*}(A\setminus E)\in[0,\infty]$.

(i) A subset $E$ of $X$ is Carathéodory measurable with respect to $\mu^{*}$, or $\mu^{*}$-measurable, if

$$\mu^{*}(A)=\mu^{*}(A\cap E)+\mu^{*}(A\setminus E)$$

for every subset $A$ of $X$.

(ii) The class $\mathcal{M}(\mu^{*})=\{E\in\mathcal{P}(X):E\text{ is }\mu^{*}\text{-measurable}\}$ of all $\mu^{*}$-measurable subsets of $X$ is a set, with $\mathcal{M}(\mu^{*})\subseteq\mathcal{P}(X)$: its defining condition on $E$ is expressed by a predicative formula, so it is a subclass of the set $\mathcal{P}(X)$, hence a set by Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper (i). (Under the guard $E\in\mathcal{P}(X)\wedge A\in\mathcal{P}(X)$, $E$ and $A$ are terms of type $\mathcal{P}(X)$ by Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (i); so are $A\cap E$ and $A\setminus E$, as the conditions $z=A\cap E$ and $z=A\setminus E$ have the predicative forms of Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (ix); $\mu^{*}(A)$, $\mu^{*}(A\cap E)$ and $\mu^{*}(A\setminus E)$ are values of the map $\mu^{*}$ at these terms, terms of type $[0,\infty]$ by Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (iii), and so is $\mu^{*}(A\cap E)+\mu^{*}(A\setminus E)$, the value of the map $+$ at their pair, by Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (iv) and Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (iii); the condition is an equation between these terms, expressed by a predicative formula by Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (v), quantified over the elements $A$ of the set $\mathcal{P}(X)$, a quantifier over a set variable.) Thus, for every set $E$, $E\in\mathcal{M}(\mu^{*})$ if and only if $E\subseteq X$ and $E$ is $\mu^{*}$-measurable.