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¨utte 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.

• Type: Conference
• Year: 2007
• Where: CIE
• Authors: Gyesik Lee
• Keywords: CIE 2007, Maximal Order Type, Order Type, Rooted Binary Trees