Can Carathéodory's Extension Lemma be proven without use of the Carathéodory's Restriction Lemma? Either the Extension Lemma or the Restriction Lemma below may be used to directly construct the Lebesgue measure, yet the only proof I know of the former lemma uses the latter. Can the Extension Lemma be proven without use of the Restriction Lemma?

Carathéodory's Extension Lemma: let $\mu_0:\Sigma_0\to [0,\infty]$ be a pre-measure on the algebra $\Sigma_0$ of $X$. Then $\mu_0$ can be extended to a measure
$$\mu:\Sigma\to[0,\infty]$$
where $\Sigma:=\sigma(\Sigma_0)$ and $\mu|_{\Sigma_0}=\mu_0$. Furhermore, if $\mu_0$ is finite, then the extension $\mu$ is unique.
Carathéodory's Restriction Lemma: let $\mu^*:2^X\to [0,\infty]$ be an outer measure on the power set $2^X$ of $X$. Then $\mu^*$ can be restricted to a measure
$$\mu:\Sigma\to[0,\infty]$$
where $\Sigma := \Big\{ C \in 2^X : C \text{ is Caratheodory measurable} \Big\}$ and $\mu := \mu^*|_{\Sigma}$.
Note: I've never seen the 'Restriction Lemma' named as such, but I find the name appropriate.
 A: *

*Not-answer 1: https://terrytao.wordpress.com/2009/01/03/254a-notes-0a-an-alternate-approach-to-the-caratheodory-extension-theorem/, by defining the outer measure $\mu^*$ from the premeasure $\mu_0$ in the standard "infimum" definition, showing that $\mu^*(A\triangle B)$ defines a pseudometric on $2^X$, and then showing that the closure (w.r.t. this pseudometric) of the elementary sets $\Sigma_0$ forms a $\sigma$-algebra on $X$, and then verifying all the necessary properties.
I add this answer since it is a sort of first step into more abstract approaches to the "Extension Theorem" (CET) compared to the more hands-on standard proof of CET; namely it metrizes/topologizes the space of subsets of $X$, which I think is a pretty radical idea, especially for say students only familiar with the standard proof.


*Not-answer 2: on this road towards "abstraction", one big "biome" is functional analysis. One can also construct the Lebesgue measure (and lots of other cool measures that Caratheodory extension doesn't help with, see What are non-obvious examples of measures obtained from linear functionals by the Riesz representation theorem? or Advantages of Riesz theorem over Caratheodory Extension theorem) from the Riesz(-Markov-Kakutani) representation theorem.
The "standard" proof, e.g. this blogpost by Terry Tao, proceeds by much the same philosophy as the Caratheodory extension theorem, and in fact overlaps it significantly: we know the values of  $\int f d\mu:= \ell(f)$ (for $f\in C_c(X,\mathbb R)$) for some hypothetical measure $\mu$, and to recover $\mu$, we want to take $f = 1_A$ an indicator function. Of course we can't do this as $1_A$ is not continuous, but we can take supremums of $\int f d \mu := \ell(f)$ over all $f\leq 1_A$ (can't do infimums over $g\geq 1_A$, since $\bar A$ may not be compact so there may be no $g\in C_c(X,\mathbb R)$ s.t. $g\geq 1_A$); this works particularly well for open sets $A$ for technical reasons (lower semi-continuity).
Having done one approximation step ($C_c$ functions to indicators of opens $1_U$) much as in the philosophy of CET, Tao does another approximation, this time basically exactly like CET (in fact in some approaches, literally exactly like CET) of defining outer and inner measure by approximation by outer open or inner compact sets respectively (compact sets measure defined via subtraction of measure of some open set), and verifying all the necessary properties (by far the hardest/most technical step is finite additivity for open sets).


*Not-answer 3: going further along the road of abstraction, we see that there is a more functional-analytic/category-theoretic flavored proof mentioned in this link: Proofs of the Riesz–Markov–Kakutani representation theorem. I can not describe it better than the answer posted in that link by MSE user Tomasz Kania.


*Maybe-answer: going even further along this road of abstraction, we have a very recent paper https://arxiv.org/pdf/2210.01720.pdf "A categorical proof of the Caratheodory extension theorem" by Ruben Van Belle. This paper only defines outer premeasures/measures on the algebra $\cal B$ or $\sigma(\cal B)$ (never on $2^X$ for instance), so I do think this proof satisfies your requirement. However, at a skim the "analytical" portions of the paper look very similar to the expressions one finds in the standard proofs of CET, so I don't think the core analytical ideas are any different from the standard proof; it just writes everything in a different language, that just doesn't happen to mention $2^X$.
