Here, $E_1$ denotes the set of arithmetic formulas starting with a bounded existential quantifier, followed by a quantifierfree 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.
I don’t see how an $E_1$ formula would give a polynomialtime 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 polynomialtime computable functions, this becomes an $E_1$ formula. Meanwhile, there are $E_1$ formulas in the basic language of arithmetic expressing some NPcomplete predicates, such as $\phi(a,b,c)=\exists x\le c\\,\exists y\le c\\,(x^2=a+by)$ (due to Adleman and Manders). It is even consistent with the current state of knowledge that every NP predicate is definable by an $E_1$ formula (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 for a relevant discussion. Of course, a positive answer would in particular imply that primality is $E_1$definable. Even if the general statement does not hold, 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. 

