Quantifier elimination for the reals with a predicate for the powers of two

Jeremy Avigad, Yimu Yin

In 1985, van den Dries showed that the theory of the reals with a predicate for the integer powers of two admits quantifier elimination in an expanded language, and is hence decida…