11
$\begingroup$

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.

Improve this question
$\endgroup$
10
  • 1
    $\begingroup$ You want $n$ to be the quantifier depth, not the number of quantifiers? Otherwise removing symbols added by definitions involving quantifiers could drastically raise the number of quantifiers in a formula $\endgroup$
    – Will Sawin
    Commented Nov 30 at 23:41
  • $\begingroup$ Can you express the relation $x_0<x_1< x_2 < \dots< x_n$ in $(\mathbb N; +)$ using fewer than $n$ quantifiers? $\exists y_1 \dots \exists y_n : x_1 = x_0+y_1, x_2=x_1+y_2,\dots, x_n = x_{n-1}+y_n$ does it but I don't see a better way $\endgroup$
    – Will Sawin
    Commented Dec 1 at 2:05
  • $\begingroup$ @WillSawin Ah, sorry, I should have clarified - I'm looking at unary formulas. Fixed! (I'm used to PA and similar, where there's no essential difference between relations and unary relations, and so I was sloppy.) $\endgroup$
    – Noah Schweber
    Commented Dec 1 at 2:06
  • $\begingroup$ I agree that for unary formulas this is not a counterexample, but I still don't understand the argument: The quantifier elimination for $\mathbb (N,+)$ involves infinitely many predicates of the form $ \exists y : y+ \dots + y =x $. It happens to be the case that all these predicates involve one quantifier, and that arbitrary linear combinations of them can still be expressed with one quantifier. But isn't it possible to have a quantifier elimination after some finite expansion by definition that adds infinitely many predicates that represent unary formulas with arbitrarily many quantifiers? $\endgroup$
    – Will Sawin
    Commented Dec 1 at 2:16
  • 1
    $\begingroup$ Well, it could be construed as a two-sorted expansion of Presburger, with the second sort consisting of the ordinals, and an isomorphism of the Presburger sort with the $\omega$ of the second sort. But I understand that this may be stretching the intended notion of expansion too far. One could make (a countable version of) the structure one-sorted by fixing a bijection of the domain of the ordinal sort with $\omega$, but this might very well break decidability. $\endgroup$
    – Emil Jeřábek
    Commented Dec 1 at 9:01

0

Reset to default

You must log in to answer this question.