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é. (shrink)

In Storybrooke, the city in which Once Upon a Time takes place, live many characters of fantastic stories. A plethora of princesses resides in this town, and their history, like their representation, undergoes important variations. Moving away from the role of “damsel in distress” often found in fairy tales and their adaptations, Emma, Snow White or Little Red Riding Hood, gain independence and freedom. However, clichés are tough and heroines often get involved in stereotypical love stories, where motherhood seems to (...) be the only possible destiny. Between literary revivals and mutations, we are now going to study these female figures and their evolution through two forms: the tale and the series. (shrink)

We show here that the first order theory of the positive integers equipped with multiplication remains decidable when one adds to the language the usual order restricted to the prime numbers. We see moreover that the complexity of the latter theory is a tower of exponentials, of height O(n).