Here, $E\_1$ denotes the set of arithmetic formulas starting with a bounded existential quantifier, followed by a quantifier-free formula. Is there an $E\_1$-formula $\phi$ such that $\phi(n)$ holds
iff $n$ is prime? If yes, it is likely to be rather complicated to obtain, as this apparently implies that PRIMES is in P.
Clearly, there is such a $U\_1$-formula (i.e. one starting with a bounded universal quantifier instead). And of course there's this famous prime polynomial, but this gives a $\Sigma\_1$-statement where the variables correspond to exponentiations and factorials, so certainly there can be no polynomial bounds for them.



Is there an $E_1$-definition of primality?
I don’t see how an $E\_1$ formula would give a polynomial-time algorithm. Primality testing has been known to be in NP long before AKS (due to Pratt), and this gives a definition of primes by a $\Sigma^b\_1$ formula (a bounded existential quantifier followed by a formula with logarithmically bounded quantifiers); if we extend the language of arithmetic by sufficiently many polynomial-time computable functions, this becomes an $E\_1$ formula.


Meanwhile, there are $E\_1$ formulas in the basic language of arithmetic expressing some NP-complete predicates, such as $\phi(a,b)=\exists x\le b\,\exists y\le b\,(x^2+ay=b)$ (due to Adleman and Manders). It is even consistent with the current state of knowledge that *every* NP predicate $R(x)$ is definable by an $E\_1$ formula where the bound on the quantifier is allowed to be $2^{(\log x)^c}$ for a constant $c$ (this is known as the “bounded Hilbert’s 10th problem”); there are some conjectures that imply that this is the case, but also some results indicating otherwise, see e.g. [Pollett](http://www.cs.sjsu.edu/faculty/pollett/papers/hilbert10.pdf) for a relevant discussion. Of course, a positive answer would in particular imply that primality definable in such a way. (Note that $E\_1$ itself in the basic language of arithmetic is a strict subset of NP by the nondeterministic time-hierarchy theorem, as every $E\_1$ predicate is computable in nondeterministic time $O(n^2)$, or even $O(n\log n)$ using the best known multiplication algorithms.)


Irrespective of general results like that, it is possible that Pratt’s (or another) NP definition of primality can be expressed as an $E\_1$ formula, but as far as I am aware, this is unknown.


