The field of reals with a predicate for the powers of two (Q1094412)

Let L be the language of ordered rings augmented by a 1-place relation symbol. Consider the ordered field \({\mathbb{R}}\) of reals together with the multiplicative group \(2^{{\mathbb{Z}}}=\{2^ n:n\in {\mathbb{Z}}\}\) as an L- structure. The author provides a set \(\Sigma\) of axioms for the complete, decidable L-theory \(Th({\mathbb{R}},2^{{\mathbb{Z}}})\). Augmenting L by countably many 1-place relation symbols and \(\Sigma\) by defining axioms for the new symbols, one gets a theory which admits elimination of quantifiers.