Abstract

We show in this paper that the theory of ordinal addition of any fixed ordinal ωα, with α less than ωω, admits a quantifier elimination. This in particular gives a new proof for the decidability result first established in 1965 by R. Büchi using transfinite automata. Our proof is based on the Ehrenfeucht games, and we show that quantifier elimination go through generalized power.RésuméOn montre ici que, pour tout ordinal α inférieur à ωω, la théorie additive de ωα admet une élimination des quantificateurs. On obtient ainsi une nouvelle preuve de la décidabilité de ces théories . On utilise ici les jeux d'Ehrenfeucht, avec un formalisme à la Ferrante et Rackoff, et on montre que le fait d'admettre une élimination des quantificateurs se transmet par produit généralisé