Ehrenfeucht games and ordinal addition (Q1377635)

In 1965 R. Büchi proved that the theory of addition of every ordinal is decidable. In the reviewed paper, it is proved that the theory of ordinal addition of any fixed ordinal \(\omega^\alpha\), where \(\alpha< \omega^\omega\), admits a quantifier elimination. The proof is based on Ehrenfeucht games. It is shown that quantifier elimination goes through generalized power.