Binary Trees and (Maximal) Order Types.

Concerning the set of rooted binary trees, one shows that Higman's Lemma and Dershowitz's recursive path ordering can be used for the decision of its maximal order type according to the homeomorphic embedding relation as well as of the order type according to its canonical linearization, well-known in proof theory as the Feferman-Schütte notation system without terms for addition. This will be done by showing that the ordinal ωn + 1 can be found as the (maximal) order type of a set in a cumulative hierarchy of sets of rooted binary trees. [ABSTRACT FROM AUTHOR]