Kleene–Brouwer order

In descriptive set theory, the Kleene–Brouwer order or Lusin–Sierpiński order^[1] is a linear order on finite sequences over some linearly ordered set $(X,<)$, 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 $t$ and $s$ are finite sequences of elements from $X$, we say that $t<_{{KB}}s\,$ when there is an $n$ such that either:

• $t\upharpoonright n=s\upharpoonright n$ and $t(n)$ is defined but $s(n)$ is undefined (i.e. $t$ properly extends $s$), or
• both $s(n)$ and $t(n)$ are defined, $t(n)<s(n)$, and $t\upharpoonright n=s\upharpoonright n$.

Here, the notation $t\upharpoonright n$ refers to the prefix of $t$ up to but not including $t(n)$. In simple terms, $t<_{{KB}}s\,$ whenever $s$ is a prefix of $t$ (i.e. $s$ terminates before $t$, and they are equal up to that point) or $t$ is to the "left" of $s$ on the first place they differ.^[1]

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 (that is, that it is transitive as well as being total) follows immediately from this, as any three sequences on which transitivity is to be tested form (with their prefixes) 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 $X$ is well-ordered, then a tree over $X$ is well-founded (having no infinitely long branches) if and only if the Kleene–Brouwer ordering is a well-ordering of the elements of the tree.^[1]

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 $x$ in a computation tree may be assigned an ordinal number $||x||$, the supremum of the ordinal numbers $1+||y||$ where $y$ ranges over the children of $x$ 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.^[2]

History

This ordering was used by Lusin & Sierpinski (1923),^[3] and then again by Brouwer (1924).^[4] Brouwer does not cite any references, but Moschovakis argues that he may either have seen Lusin & Sierpinski (1923), or have been influenced by earlier work of the same authors leading to this work. Much later, Kleene (1955) studied the same ordering, and credited it to Brouwer.^[5]

References

1. Moschovakis, Yiannis (2009), Descriptive Set Theory (2nd ed.), Rhode Island: American Mathematical Society, pp. 148–149, 203–204, ISBN 978-0-8218-4813-5
2. Schwichtenberg, Helmut; Wainer, Stanley S. (2012), "2.8 Recursive type-2 functionals and well-foundedness", Proofs and computations, Perspectives in Logic, Cambridge: Cambridge University Press, pp. 98–101, ISBN 978-0-521-51769-0, MR 2893891.
3. Lusin, Nicolas; Sierpinski, Waclaw (1923), "Sur un ensemble non measurable B", Journal de Mathématiques Pure et Appliquées, 9 (2): 53–72.
4. Brouwer, L. E. J. (1924), "Beweis, dass jede volle Funktion gleichmässig stetig ist", Koninklijke Nederlandse Akademie van Wetenschappen, Proc. Section of Sciences, 27: 189–193. As cited by Kleene (1955).
5. Kleene, S. C. (1955), "On the forms of the predicates in the theory of constructive ordinals. II", American Journal of Mathematics, 77: 405–428, doi:10.2307/2372632, JSTOR 2372632, MR 0070595. See in particular section 26, "A digression concerning recursive linear orderings", pp. 419–422.