Cheng space

Cheng spaces


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 σ\sigma-ideal of null subsets (or a δ\delta-filter of full subsets), there is no essential difference classically.

Some of the abstract nonsense below is original research (by Toby Bartels and Todd Trimble), but based heavily on Cheng's work as described in Bishop & Bridges?.


From a constructive perspective, there are a couple of related problems with the classical theory of measurable spaces. One is that the notion of σ\sigma-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 σ\sigma-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 (A,B)(A,B) such that ABA \cup B is full —with (A,¬A)(A,\neg{A}) 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 σ\sigma-algebra must actually be measurable by any measure used).


Let XX be a set. We’ll define the structure of a Cheng space on XX in several steps.

The Boolean semi-algebra of disjoint pairs

A disjoint pair in XX is a pair (A,B)(A,B) of subsets of XX such that the intersection ABA \cap B is empty. Every set AA defines a disjoint pair [A]=(A,¬A)[A] = (A,\neg{A}), but many disjoint pairs are not of this form; the extreme counterexample (unless XX is empty) is (,)(\empty,\empty). We order disjoint pairs by the usual order on the first component and the opposite on the second:

(A,B)(C,D)ACBD. (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:

  • =[]=(,X) \empty = [\empty] = (\empty, X) ;
  • X=[X]=(X,) X = [X] = (X, \empty) ;
  • (A,B)(C,D)=(AC,BD) (A,B) \cup (C,D) = (A \cup C, B \cap D) ;
  • (A,B)(C,D)=(AC,BD) (A,B) \cap (C,D) = (A \cap C, B \cup D) ;
  • i(A i,B i)=( iA i, iB i) \bigcup_i (A_i,B_i) = (\bigcup_i A_i, \bigcap_i B_i) ;
  • i(A i,B i)=( iA i, iB i) \bigcap_i (A_i,B_i) = (\bigcap_i A_i, \bigcup_i B_i) .

(Note that we do not write [A][A] as AA except when AA is given as \empty or XX, because for example, [AB]=[A][B][A \cap B] = [A] \cap [B], 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 (A,B)(A,B), not using the complements of AA and BB (which usually are not even disjoint) but instead simply by reversing them:

¬(A,B)=(B,A). \neg(A,B) = (B,A) .

Then an actual de Morgan duality holds for these operations:

  • ¬ i(A i,B i)= i¬(A i,B i) \neg\bigcup_i (A_i,B_i) = \bigcap_i \neg(A_i,B_i) ;
  • ¬ i(A i,B i)= i¬(A i,B i) \neg\bigcap_i (A_i,B_i) = \bigcup_i \neg(A_i,B_i) ;
  • ¬¬(A,B)=(A,B) \neg\neg(A,B) = (A,B) , the famous double negation law.

We can go on to define the relative complement (A,B)(C,D)(A,B) \setminus (C,D) and symmetric difference (A,B)(C,D)(A,B) \uplus (C,D) in terms of complements, intersections, and unions as usual, and they obey many of the usual classical laws. (For instance, \uplus 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 (A,B)¬(A,B)=(AB,)(A,B) \cup \neg(A,B) = (A \cup B, \empty) (and similarly for intersection) and there is no requirement that AB=XA \cup B = X. 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.

This is all a special case of the Chu construction; the poset of disjoint pairs in XX is Chu TV(PX,)Chu_{TV}(P X, \empty), where TVTV is the enriching category of truth values.

The σ\sigma-semi-algebra of complemented pairs

Given a set XX, a σ\sigma-semi-algebra on XX is a collection \mathcal{M} of disjoint pairs in XX, called complemented pairs, such that: 1. []=(,X)[\empty] = (\empty,X) is a complemented pair; 2. If (A,B)(A,B) is a complemented pair, then so is its complement (B,A)(B,A); 3. If (A 1,B 1),(A 2,B 2),(A 3,B 3),(A_1,B_1), (A_2,B_2), (A_3,B_3), \ldots are complemented pairs, then so is their union ( iA i, iB i)(\bigcup_i A_i, \bigcap_i B_i).

The arguments above that \mathcal{M} is closed under countable intersections, relative complements, and symmetric differences goes through. (We can also define analogous notions of semi-algebra, δ\delta-semi-ring, and other variations of σ\sigma-algebra.)

Finally, a Cheng measurable space or simply a Cheng space is a set equipped with a σ\sigma-semi-algebra.

(Incidentally, the reason why we do not use the term ‘measurable pair’ is that AA and BB may easily both be measurable in some sense yet without having (A,B)(A,B) as a complemented pair. In particular, (,)(\empty,\empty) is rarely a complemented pair —although that is not forbidden either—, yet it is hard to call it non-measurable.)

Measurable sets and functions

A subset AA of a Cheng space XX is measurable if there is some complemented pair (A,B)(A,B). A subset SS is full if, for some complemented pair (A,B)(A,B), SS contains the union ABA \cup B. Conversely, SS is null if, for some such (A,B)(A,B), SS is disjoint from ABA \cup B.

Given two Cheng measurable spaces XX and YY, an almost function from XX to YY is a partial function from XX to YY such that the domain of ff is full. An almost function is measurable if, given any complemented pair (C,D)(C,D) in YY, there is a complemented pair (A,B)(A,B) such that {p:X|pAf(p)C}\{p\colon X \;|\; p \in A \iff f(p) \in C\} and {p:X|pBf(p)D)\{p\colon X \;|\; p \in B \iff f(p) \in D) are both full.

Two (measurable) functions are almost equal if their equaliser is full.

Cheng spaces, measurable almost functions between them, and almost equality between them form a category ChengSpCheng Sp.


A Cheng space is complete if, whenever (A,B)(A,B) is a complemented pair and ACA \Leftrightarrow C and BDB \Leftrightarrow D are full, then (C,D)(C,D) is a complemented pair. In particular, every full set and every null set is measurable.

Given any Cheng space (X,)(X,\mathcal{M}), its completion (X,¯)(X,\bar{\mathcal{M}}) has the same underlying set XX but a disjoint pair (C,D)(C,D) is ¯\bar{\mathcal{M}}-complemented iff, for some \mathcal{M}-complemented pair (A,B)(A,B), both ACA \Leftrightarrow C and BDB \Leftrightarrow D are \mathcal{M}-full.

A Cheng space is complete iff it is its own completion; the completion of any Cheng space is complete. The identity function on XX is measurable in either direction between (X,)(X,\mathcal{M}) and (X,¯)(X,\bar{\mathcal{M}}), so they are isomorphic in ChengSpCheng Sp. Accordingly, the full subcategory of ChengSpCheng Sp on the complete spaces is equivalent to ChengSpCheng Sp 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.

Measures on Cheng spaces

We will define the notion of a positive measure on a Cheng space; it’s straightforward to generalise to other sorts of measures as described at measure.

Given a Cheng space (X,)(X,\mathcal{M}), a positive measure on (X,)(X,\mathcal{M}) is a function μ\mu from \mathcal{M} to [0,][0,\infty] such that:

  • absolute continuity: μ(A,B)=0\mu(A,B) = 0 if BB is full;
  • inclusion-exclusion: μ(AC,BD)+μ(AC,BD)=μ(A,B)+μ(C,D)\mu(A \cap C, B \cup D) + \mu(A \cup C, B \cap D) = \mu(A,B) + \mu(C,D);
  • subadditivity?: μ( iA i, iB i) iμ(A i,B i)\mu(\bigcup_i A_i, \bigcap_i B_i) \leq \sum_i \mu(A_i,B_i) for an infinite sequence of complemented pairs.

We think of μ(A,B)\mu(A,B) as the measure of AA; thanks to absolute continuity, either AA or BB alone is enough to determine μ(A,B)\mu(A,B).

Last revised on July 30, 2012 at 12:21:05. See the history of this page for a list of all contributions to it.