Is there a measure theory for proper classes? This question is naive, but I didn't get an answer at MSE: Is it straightforward to extend measure theory to proper classes?
Of course when one tries to define measures on "large sets" problems of non-measurability arise (e.g. non-Lebesgue measurable sets, Ulam's theorem, etc.). But setting those aside (since they arise already for measures over sets), are there any special problems that dealing with proper classes would raise?
To be a little bit more precise (and I'm afraid I can't do any better at the moment), let $\Omega$ be a proper class. If you prefer that we have something concrete, then let $\Omega$ be the proper class of all ordinals, for instance. Is there anything wrong with saying that a measure is a real-valued function with the usual properties (countable additivity, etc.) on a collection of sub-classes of $\Omega$?
In other words, can the usual definition of a measure be extended straightforwardly to proper classes or are there problems lurking here?
If this isn't entirely straightforward and you know of any references, I would appreciate them.
 A: As a sledgehammer, working in Higher Order Set Theory (HOST) as proposed in

*

*Rhea, Alec, An Axiomatic Approach to Higher Order Set Theory. (2022)
https://doi.org/10.48550/arXiv.2206.10060
you can just go ahead and collect up proper classes inside other proper classes, no need to move higher up the hierarchy or inevitable collapse downwards due to membership issues. I designed this theory to work with things like topology, analysis, measure theory, etc. over the surreals without having to worry about anything too subtle, and it works equally well for measure theory on arbitrary proper classes -- no subtleties lurking about.
This theory is equiconsistent with ZFC plus a countable collection of inaccessible cardinals, however, so it is significantly stronger in consistency strength than most standard set theories. If there's anything you'd like me to elaborate on please don't hesitate to ask.
A: One might hope to handle proper classes as objects by working in one of the standard second-order set theories. For example, there is Gödel–Bernays set theory GBC, which has classes as objects, and includes familiar class axioms, including the first-order class comprehension axiom, which asserts that every first-order definable property defines a class. Kelley–Morse set theory KM extends this comprehension axiom to allow second-order definitions, where the second-order quantifiers range over classes. There is an emerging literature classifying various second-order theories over GBC, analyzing the strength of various principles such as the existence of forcing relations for class forcing, the existence of first-order truth predicates and transfinite class recursions. The principle CC or class comprehension is commonly considered as a strengthening of KM.
So, with these second-order theories, one can handle the existence of classes.
An immediate problem for your proposal, however, is that a measure on the classes is not itself a class object, but a third-order object, a meta class. Specifically, a measure would be a map associating every class with a real number. For this reason, even the second-order set theories do not seem able in general to handle arbitrary measures.
One way around this issue (as suggested by David Roberts in the comments), which will work when the collection of measurable classes is comparatively small, is to consider measures that are codeable entirely into a single class. For example, one could consider the underlying collection of measurable sets as the set of sections $M\subset  V\times V$, where sections are $M_x=\{y\mid (x,y)\in M\}$, and then consider the measure as a class function $\mu:V\to\mathbb{R}$. When the collection of measurable classes is indexable by $V$, then this approach works fine in the second-order frameworks such as KM. Probably one will usually want to augment KM with stronger axioms such as the class DC schema, which is not provable in KM. This method of coding into classes by sections is common in many other context — for example, one can construct class binary relations $\Gamma$ on Ord that code "metaordinals" higher than Ord, and then aim to undertake class recursions of length $\Gamma$. This is the underlying idea in the principle ETR.
Another natural way to handle larger class measures is to find definable measures, avoiding the need to code up the entire collection of measurable classes into a single class. These measures would be definable associations of every class $X\subseteq\newcommand\Ord{\mathrm{Ord}}\Ord$ with its measure
$$X\mapsto \mu(X).$$
And indeed, there are some extremely natural instances of this, which appear already in the set-theoretic literature.
Consider for example the club measure, defined on $X\subseteq\Ord$ so that $\mu(X)=1$, if $X$ contains a closed unbounded class $C\subseteq X\subseteq\Ord$, and $\mu(X)=0$, if $X$ is disjoint from a closed unbounded class $X\cap C=\varnothing$. This is a second-order definable map, since we say $X$ has measure one if there is a club class inside $X$, and measure $0$ if there is a club class disjoint from $X$. The positive classes are exactly the stationary classes, those that have nontrivial intersection with every club class.
One can prove in KM+CC that this measure is countably additive and indeed $\kappa$-additive for every cardinal $\kappa$. The main point is that if one has a $\kappa$-sequence of measure one sets $X_\alpha$, containing clubs $C_\alpha\subseteq X_\alpha$, then by CC one can choose particular such clubs $C_\alpha$, and the intersection of any set number of closed unbounded classes of ordinals remains club. So there is a single club class $C$ contained in every $X_\alpha$, and so $\bigcap_\alpha X_\alpha$ has measure one.
Meanwhile, an intriguing situation occurs with this measure without the CC axiom. Namely, without CC one cannot in general pick the club classes $C_\alpha$, and in some joint work with myself, Vika Gitman and Asaf Karagila, we proved that it is consistent with mere KM that this measure is not countably additive.

*

*Gitman, Victoria; Hamkins, Joel David; Karagila, Asaf, Kelley–Morse set theory does not prove the class Fodor principle, Fundam. Math. 254, No. 2, 133-154 (2021). ZBL07419456.

This observation can be taken as evidence that Kelley-Morse set theory is less robust than might have been imagined, and for such kind of uses of proper classes, one will often want to augment it with CC or much more.
