Kleene–Brouwer order


In descriptive set theory, the Kleene–Brouwer order or Lusin–Sierpiński order is a linear order on finite sequences over some linearly ordered set, that differs from the more commonly used lexicographic order in how it handles the case when one sequence is a prefix of the other. In the Kleene–Brouwer order, the prefix is later than the longer sequence containing it, rather than earlier.
The Kleene–Brouwer order generalizes the notion of a postorder traversal from finite trees to trees that are not necessarily finite. For trees over a well-ordered set, the Kleene–Brouwer order is itself a well-ordering if and only if the tree has no infinite branch. It is named after Stephen Cole Kleene, Luitzen Egbertus Jan Brouwer, Nikolai Luzin, and Wacław Sierpiński.

Definition

If and are finite sequences of elements from, we say that when there is an such that either:
Here, the notation refers to the prefix of up to but not including.
In simple terms, whenever is a prefix of or is to the "left" of on the first place they differ.

Tree interpretation

A tree, in descriptive set theory, is defined as a set of finite sequences that is closed under prefix operations. The parent in the tree of any sequence is the shorter sequence formed by removing its final element. Thus, any set of finite sequences can be augmented to form a tree, and the Kleene–Brouwer order is a natural ordering that may be given to this tree. It is a generalization to potentially-infinite trees of the postorder traversal of a finite tree: at every node of the tree, the child subtrees are given their left to right ordering, and the node itself comes after all its children. The fact that the Kleene–Brouwer order is a linear ordering follows immediately from this, as any three sequences on which transitivity is to be tested form a finite tree on which the Kleene–Brouwer order coincides with the postorder.
The significance of the Kleene–Brouwer ordering comes from the fact that if is well-ordered, then a tree over is well-founded if and only if the Kleene–Brouwer ordering is a well-ordering of the elements of the tree.

Recursion theory

In recursion theory, the Kleene–Brouwer order may be applied to the computation trees of implementations of total recursive functionals. A computation tree is well-founded if and only if the computation performed by it is total recursive. Each state in a computation tree may be assigned an ordinal number, the supremum of the ordinal numbers where ranges over the children of in the tree. In this way, the total recursive functionals themselves can be classified into a hierarchy, according to the minimum value of the ordinal at the root of a computation tree, minimized over all computation trees that implement the functional. The Kleene–Brouwer order of a well-founded computation tree is itself a recursive well-ordering, and at least as large as the ordinal assigned to the tree, from which it follows that the levels of this hierarchy are indexed by recursive ordinals.

History

This ordering was used by, and then again by. Brouwer does not cite any references, but Moschovakis argues that he may either have seen, or have been influenced by earlier work of the same authors leading to this work. Much later, studied the same ordering, and credited it to Brouwer.