Can someone provide intuition for Alfsen's proof of the existence and uniqueness of the Haar measure on locally compact groups? I am trying to understand Alfsen's proof of the existence and uniqueness of the Haar measure on locally compact groups:
Alfsen, Erik M., A simplified constructive proof of the existence and uniqueness of Haar measure, Math. Scand. 12 (1963), 106-116 (1964). ZBL0274.43001.
I am not entirely sure what the underlying idea is behind this proof. My thoughts on this are as follows:

*

*The identify measures with linear functionals, so the proof reduces to constructing a particular linear functional on the space $L^{+}$ of compactly supported positive functions defined on $G$.

*In particular, we need to find an admissible functional. The existence and uniqueness of this then implies the  existence and uniqueness of the Haar measure.

*We associate to the class of admissible functionals a pre-ordering, denoted in words by 'are comparable', which allows us to 'compare' two functionals.

*Proposition 2.1: We show that two admissible functionals that have comparable pre-orderings are unique up to a multiplicative positive scalar.

*Our problem now reduces to finding one admissible that is comparable with any other.

*We define a coarser pre-ordering on $L^{+}$, known as relative size (equation 2.5)

*We show that this particular pre-ordering is itself a pre-ordering associated to some admissible.

*We deduce this problem to proving that equation 2.6 holds. We prove this using the separation property for functions in $L_{V}^{+}$. see prop. 2.3, whose proof ends before the remark on page 111.

*The remainder of the paper is dedicated to proving that the separation theorem property actually holds.
"QED"

There is very little material explaining this paper other than the paper itself, so any further information about it would be much appreciated. Thanks.
 A: It seems that you more or less have a decent understanding of the proof, so I'm not sure if I can add much of value.
The first important step is that he defines an admissible functional on $L^+$ in a way so as to make existence and uniqueness, modlulo some positive multiple, of an admissible functional equivalent to existence and uniqueness of a Haar measure (via the Riesz representation theorem). Next he introduces a pre-ordering on $L^+$ associated to an admissible functional and deduces that any two functionals giving a comparable pre-order differ only by a positive multiplicative constant.
This leads to the realization that it would be nice to find a pre-order which is comparable with any pre-order induced by an admissible functional. For if this were the case and this pre-order were associated with an admissible functional, then this would give existence and uniqueness (once more modulo multiplication by a positive constant) of an admissible functional. He shows that the first part is indeed the case in Prop. 2.2.
Now all that is left is showing that the pre-order is associated wit an admissible functional. This boils down to proving (2.6). He shows that (2.6) is equivalent to a separation property (S) and then, as you mentioned, spends the rest of the paper proving (S).
I feel like I've mostly repeated what you wrote, but as I said you pretty much get the gist of it. Did you have any specific questions/issues?
Edit: The idea is the following: We know that $\mathrm{supp}(f)$ is contained in some compact subset $C$ of $G$. This implies that $\mathrm{supp}(f)$ can be covered by a finite number of left translates of $\{\varphi > \frac{1}{2}\|\varphi\|_\infty\}$, where $\|\cdot\|_\infty$ denotes the sup norm.
Edit 2: Generally, the notation $u^+$ denotes the positive part of $u$; that is, $u^+ := \max(u,0)$. In this context, that would mean $\left(f - \frac{1}{n}\right)^+ = \max\left(f-\frac{1}{n},0\right)$. That would seem to make sense in this context, so I would assume that is what he means.
