Note on a Proof of the Extended Kirby—Paris Theorem on Labeled Finite Trees

Buchholz [2] extended a certain game of unlabeled finite trees of Kirby—Paris [6] to the case of labeled finite trees whose nodes have labels from ω + 1 = {0, 1, 2, . . . , ω}, and proved that this game stops in finite time. He used an infinitary notion of ‘well-founded infinite trees’ to prove this property on the finite-tree game. In this note, we avoid the use of any infinitary notion and reduce the infinitary technique to a finitary technique, by utilizing Takeuti's system of ordinal diagrams [7]. Also we generalize Buchholz's game by introducing higher ordinal numbers as the labels of the trees, and show the termination property of this generalized game.