Let $L$ be the firstorder language with binary function symbol $+$, unary function symbol $E$. Let $T$ be the set of sentences over this language that are true in the natural numbers, with $+$ interpreted in the usual way, and $E(n$) interpreted as $2^n$. Is the set $T$ recursive?
Take the 2minute tour
×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

As Marty explained in this answer, this question is the central topic of the paper On the expansion $\langle \mathbb{N},+,2^x\rangle$ of Presburger arithmetic, by Françoise Point, based on a joint proceedings paper with G. Cherlin on a result credited to Alexei L. Semenov. 

