Arithmetic generally does not admit any non-trivial quantifier elimination. I will talk about one exception, where the negation of an induction axiom is included in the theory. Here the Weak Koenig Lemma from reverse mathematics arises as a model completion.
This work is joint with Marta Fiori-Carones (Novosibirsk), Leszek Aleksander Kolodziejczyk (Warsaw) and Keita Yokoyama (Sendai).