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.

Copyright © 2014 Barry Watson. All rights reserved.