Since true statements are not defamatory in the USA or my own country of residence, I don't see why I shouldn't name Daniel Biss. One of the errors was noticed in this question.

@StevenClontz "Countable chain condition" is listed there as P29 with a checkmark. In any case, the underlying fact is that an arbitrary product of separable spaces is ccc. The proof is the original application of the $\Delta$-system lemma.

@Hans It seems you are caught up in thinking infinite-dimensional groups might behave like Lie groups if they are compact. This is not so. It isn't the case that people have formulated the theorems about Lie groups "conservatively', it really is the case that a general compact group doesn't behave at all like a Lie group, even if connected. Once you leave the compact setting, the behaviour of the exponential map is even wilder, e.g. in the case of $\mathrm{Diff}(S^1)$ or the unitary group of an infinite-dimensional Hilbert space in the strong/weak operator topology.

In algebraic geometry, the maximal spectrum is not of much use for a local ring, and fails to distinguish between local rings and fields, so the prime spectrum is used (there are other good reasons as well). The reason we don't use the prime spectrum in Banach algebra theory is that in general there are a lot of weird prime ideals in $C(X)$ that don't have a geometric interpretation. Examples can be found in Gillman and Jerison's Rings of Continuous Functions. (Of course, if anyone knows a use for these ideals, other than as counterexamples, I'd be glad to hear it.)

Try Takesaki's Theory of Operator Algebras I or Sakai's C$^*$-algebras and W$^*$-algebras. It will help you to know the following convention: "von Neumann algebra" = "weakly closed *-subalgebra of some $B(\mathcal{H})$", "W$^*$-algebra" = "(abstract) C$^*$-algebra *-isomorphic to a von Neumann algebra". The various topologies on a W$^*$-algebra $A$ are defined using its predual $A_*$.

The reason you thought of Pedersen is probably that he invented definitions of lower semicontinuous, Baire and Borel functions in the noncommutative case, as subsets of $A^{**}$ for $A$ a C$^*$-algebra, as have come up before e.g. here. Unfortunately that theory is intrinsically more difficult than the commutative case.

Historically, Baire started with functions, and couldn't prove that there were functions properly of Baire class higher than 2. Lebesgue provided the first proof that there were functions of arbitrarily large (countable ordinal) Baire class by turning the problem from functions into sets (and Borel classes) and using a diagonal argument. In my example above of the law of large numbers, it is naturally formulated in terms of a set.

@CalebEckhardt I could have made my answer longer by saying that I consider "monotone $\sigma$-complete subalgebras of $\mathbb{R}^X$" and "$\sigma$-complete Boolean subalgebras of $\mathcal{P}(X)$" to both be measure theory, as the proofs for the former tend to be translations of those for the latter, which were discovered first. You never regain the advantages that the "functionals on C(X)" approach has when it can be used to avoid measure theory entirely, which to me is the entire point of it.

@CalebEckhardt Pedersen doesn't work with $C(X)^{**}$ in Analysis Now. He defines outer and inner integrals on $\mathbb{R}^X$ and takes measurable functions to be the set of functions to be where they agree (the function version of Caratheodory's definition of measurable set), just like Bourbaki does. He is not as ideological as Bourbaki, so introduces $\sigma$-algebras and measures soon after.

The set that one wants to prove has measure 1 in the strong law of large numbers is dense with empty interior, so its measure can't be directly expressed using the frame of open sets. Of course, you can extend the valuation to a measure on Borel sets, but then you're doing measure theory anyway.