Prewellordering


In set theory, a prewellordering is a binary relation that is transitive, connex, and wellfounded. In other words, if is a prewellordering on a set, and if we define by
then is an equivalence relation on, and induces a wellordering on the quotient. The order-type of this induced wellordering is an ordinal, referred to as the length of the prewellordering.
A norm on a set is a map from into the ordinals. Every norm induces a prewellordering; if is a norm, the associated prewellordering is given by
Conversely, every prewellordering is induced by a unique regular norm.

Prewellordering property

If is a pointclass of subsets of some collection of Polish spaces, closed under Cartesian product, and if is a prewellordering of some subset of some element of, then is said to be a -prewellordering of if the relations and are elements of, where for,
is said to have the prewellordering property if every set in admits a -prewellordering.
The prewellordering property is related to the stronger scale property; in practice, many pointclasses having the prewellordering property also have the scale property, which allows drawing stronger conclusions.

Examples

and both have the prewellordering property; this is provable in ZFC alone. Assuming sufficient large cardinals, for every, and
have the prewellordering property.

Consequences

Reduction

If is an adequate pointclass with the prewellordering property, then it also has the reduction property: For any space and any sets, and both in, the union may be partitioned into sets, both in, such that and.

Separation

If is an adequate pointclass whose dual pointclass has the prewellordering property, then has the separation property: For any space and any sets, and disjoint sets both in, there is a set such that both and its complement are in, with and.
For example, has the prewellordering property, so has the separation property. This means that if and are disjoint analytic subsets of some Polish space, then there is a Borel subset of such that includes and is disjoint from.