If is a well-ordering on the set S, then the height of an element t∈S, written ht(t), is the order type of {s∈S|s≺t}. The height of S, ht(S), is the order type of (S,≺).

In the case of a relation which is only well-founded, say on S, the definition of height is ht(t)=sup{ht(s)+1|s⊰t}. Here the function sup is the supremum which calculates the least number greater than or equal to all of the numbers of the argument set, e.g. sup{1,2,3,4}=4. The height is then the order type of the longest path. The height of (S,⊰) is defined as ht(s)=sup{ht(s)+1|s∈S}.


Doets, Kees. From Logic to Logic Programming. MIT Press, 1994.