Kleene–Brouwer order

From Wikipedia, the free encyclopedia

In descriptive set theory, the Kleene–Brouwer order is a linear order on finite sequences of some set X.

Specifically, if t and s are finite sequences of elements from X which first differ in the nth place, we say that t < _KBs when:

• s(n) is undefined (ie. t properly extends s), or
• both s(n) and t(n) are defined, and t(n) < s(n).

Its importance comes from the fact that a tree is well-founded if and only if the Kleene–Brouwer ordering is a well-ordering of the elements of the tree.