This question is very close to this old MSE question of mine, which is still unanswered.

Is there an (ideally reasonably-natural!) expansion of the structure $(\mathbb{N};+)$ in a finite language whose first-order theory is computable but such that, for each $n$, there is an $n$-quantifier formula in a single free variable not defining the same set as any $<n$-quantifier formula?

For example, adjoining exponentiation with base $2$ does not work since its quantifier hierarchy collapses (due to Cherlin/Point, see here). Indeed, all the decidability results I'm familiar with for theories of arithmetic rely on quantifier elimination after some finite expansion by definitions, and so won't help here.

This question is very close to this old MSE question of mine, which is still unanswered.

Is there an (ideally reasonably-natural!) expansion of the structure $(\mathbb{N};+)$ in a finite language whose first-order theory is computable but such that, for each $n$, there is a quantifier-rank-$n$ formula in a single free variable not defining the same set as any $<n$-quantifier-rank formula?

Here quantifier rank is determined by the number of alternations of quantifier types when the formula is put into prenex normal form; so e.g. "$\forall x,y,z\exists w\forall u,v\theta$" has quantifier rank $3$ assuming $\theta$ is quantifier-free.

For example, adjoining exponentiation with base $2$ does not work since its quantifier hierarchy collapses (due to Cherlin/Point, see here). Indeed, all the decidability results I'm familiar with for theories of arithmetic rely on quantifier elimination after some finite expansion by definitions, and so won't help here.

This question is very close to this old MSE question of mine, which is still unanswered.

Is there an (ideally reasonably-natural!) expansion of the structure $(\mathbb{N};+)$ in a finite language whose first-order theory is computable but such that, for each $n$, there is an $n$-quantifier formula not defining the same relation as any $<n$-quantifier formula?

For example, adjoining exponentiation with base $2$ does not work since its quantifier hierarchy collapses (due to Cherlin/Point, see here). Indeed, all the decidability results I'm familiar with for theories of arithmetic rely on quantifier elimination after some finite expansion by definitions, and so won't help here.

This question is very close to this old MSE question of mine, which is still unanswered.

Is there an (ideally reasonably-natural!) expansion of the structure $(\mathbb{N};+)$ in a finite language whose first-order theory is computable but such that, for each $n$, there is an $n$-quantifier formula in a single free variable not defining the same set as any $<n$-quantifier formula?

For example, adjoining exponentiation with base $2$ does not work since its quantifier hierarchy collapses (due to Cherlin/Point, see here). Indeed, all the decidability results I'm familiar with for theories of arithmetic rely on quantifier elimination after some finite expansion by definitions, and so won't help here.