A Cheng space is a version of a measurable space developed by Henry Cheng? for constructive mathematics. Even in classical mathematics, however, Cheng spaces are more general than standard measure spaces. On the other hand, if we equip a measurable space with a -ideal of null subsets (or a -filter of full subsets), there is no essential difference classically.
From a constructive perspective, there are a couple of related problems with the classical theory of measurable spaces. One is that the notion of -algebra is highly suspicious, because it relies on an operation, complementation, that behaves very differently in intuitionistic logic. The other is that, even you acept the definition of -algebra (after all, the Lebesgue-measurable sets on the real line do still form one), there may be very few measurable functions. (It is possible in constructive mathematics that every function from the real line to itself, regardless of measurability, is continuous.)
Indeed, if we set aside the general theory of measurable spaces and simply do Lebesgue measure ad hoc in a constructive (even predicative) way, we find that instead of measurable functions we really want measurable partial functions whose domain of definition is a full subset, the almost functions. This suggests that if we want to define the concept of measurable function, then we have to know what the full sets are, so we need a measurable space equipped with such a notion. But since this is usually defined relative to a measure, well after the structure of the measurable space has been given, we are at an impasse.
There is a way out, due to Henry Cheng?, for both of these problems at once. Instead of dealing with individual subsets, we will deal with pairs of disjoint subsets. The intuition is that we use disjoint pairs such that is full —with being the motivating example in the classical theory—, but we let the Cheng measurability structure itself tell us which pairs those are. Once we fix a particular measure, we may find additional pairs whose union is full, somewhat like finding additional measurable sets when taking the completion in the classical theory (although taking the completion is a separate phenomenon here), but that's all right; the important thing is that each pair chosen really is full in any measure used (much as each set in a classical -algebra must actually be measurable by any measure used).
Let be a set. We’ll define the structure of a Cheng space on in several steps.
A disjoint pair in is a pair of subsets of such that the intersection is empty. Every set defines a disjoint pair , but many disjoint pairs are not of this form; the extreme counterexample (unless is empty) is . We order disjoint pairs by the usual order on the first component and the opposite on the second:
(A,B) \subseteq (C,D) \;\Leftrightarrow\; A \subseteq C \;\wedge\; B \supseteq D .
Similarly, we make the usual operations on sets into operations on disjoint pairs by applying formal de Morgan duality to the second component:
(Note that we do not write as except when is given as or , because for example, , while classically valid, may fail constructively.)
These operations form the disjoint pairs into a lattice; in fact, it is both a complete lattice and a distributive lattice, but it is not constructively completely distributive in either direction. (Compare the fact that a power set is, constructively, completely distributive only in one direction, making it a frame; here the directions are mixed by the formal duality and so neither works. On the other hand, that the power set is a frame is used to show that the infinitary operations do define disjoint pairs.)
Finally, we define the complement of , not using the complements of and (which usually are not even disjoint) but instead simply by reversing them:
\neg(A,B) = (B,A) .
Then an actual de Morgan duality holds for these operations:
We can go on to define the relative complement and symmetric difference in terms of complements, intersections, and unions as usual, and they obey many of the usual classical laws. (For instance, is —through a fairly lengthy calculation— associative, which is not constructively true of symmetric difference on a power set.)
At this point, the reader could be forgiven for thinking that we have cleverly pulled a Boolean algebra out of a mere Heyting algebra, but this is not true; aside from the give-away that this lattice is not constructively completely distributive, it is not even classically a Boolean algebra. This is because (and similarly for intersection) and there is no requirement that . What we have instead is a complete Boolean rig, aka semi-ring with unit; to keep consistent with the usual terminology of measure theory, I'll call such a thing a Boolean semi-algebra.
Given a set , a -semi-algebra on is a collection of disjoint pairs in , called complemented pairs, such that:
The arguments above that is closed under countable intersections, relative complements, and symmetric differences goes through. (We can also define analogous notions of semi-algebra, -semi-ring, and other variations of -algebra.)
Finally, a Cheng measurable space or simply a Cheng space is a set equipped with a -semi-algebra.
(Incidentally, the reason why we do not use the term ‘measurable pair’ is that and may easily both be measurable in some sense yet without having as a complemented pair. In particular, is rarely a complemented pair —although that is not forbidden either—, yet it is hard to call it non-measurable.)
A subset of a Cheng space is measurable if there is some complemented pair . A subset is full if, for some complemented pair , contains the union . Conversely, is null if, for some such , is disjoint from .
Given two Cheng measurable spaces and , an almost function from to is a partial function from to such that the domain of is full. An almost function is measurable if, given any complemented pair in , there is a complemented pair such that and are both full.
Cheng spaces, measurable almost functions between them, and almost equality between them form a category .
A Cheng space is complete if, whenever is a complemented pair and and are full, then is a complemented pair. In particular, every full set and every null set is measurable.
Given any Cheng space , its completion has the same underlying set but a disjoint pair is -complemented iff, for some -complemented pair , both and are -full.
A Cheng space is complete iff it is its own completion; the completion of any Cheng space is complete. The identity function on is measurable in either direction between and , so they are isomorphic in . Accordingly, the full subcategory of on the complete spaces is equivalent to itself (via its inclusion functor).
When restricted to complete spaces, the definition of measurable function is simpler: any partial function under which the preimage of any complemented pair is complemented.
Given a Cheng space , a positive measure on is a function from to such that:
We think of as the measure of ; thanks to absolute continuity, either or alone is enough to determine .