Return to Answer

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.

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.

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. 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.

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.

Another natural way to handle 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.

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.