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

(

X

,

<

)

{\displaystyle (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

{\displaystyle t}

and

s

{\displaystyle s}

are finite sequences of elements from

X

{\displaystyle X}

, we say that

t

<

K

B

s

{\displaystyle t<_{KB}s}

when there is an

n

{\displaystyle n}

such that either:

t

↾

n

=

s

↾

n

{\displaystyle t\upharpoonright n=s\upharpoonright n}

and

t

(

n

)

{\displaystyle t(n)}

is defined but

s

(

n

)

{\displaystyle s(n)}

is undefined (i.e.

t

{\displaystyle t}

properly extends

s

{\displaystyle s}

), or

both

s

(

n

)

{\displaystyle s(n)}

and

t

(

n

)

{\displaystyle t(n)}

are defined,

t

(

n

)

<

s

(

n

)

{\displaystyle t(n)<s(n)}

, and

t

↾

n

=

s

↾

n

{\displaystyle t\upharpoonright n=s\upharpoonright n}

.

Here, the notation

t

↾

n

{\displaystyle t\upharpoonright n}

refers to the prefix of

t

{\displaystyle t}

up to but not including

t

(

n

)

{\displaystyle t(n)}

.

In simple terms,

t

<

K

B

s

{\displaystyle t<_{KB}s}

whenever

s

{\displaystyle s}

is a prefix of

t

{\displaystyle t}

(i.e.

s

{\displaystyle s}

terminates before

t

{\displaystyle t}

, and they are equal up to that point) or

t

{\displaystyle t}

is to the "left" of

s

{\displaystyle s}

on the first place they differ.