Ehrenfeucht games and ordinal addition (Q1377635): Difference between revisions

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.