Is there a natural "algebraic" first order theory $T$ and a formula $\varphi$ such that $\varphi$ has high quantifier complexity over $T$?
By "algebraic" I mean not explicitly arithmetic or set theoretic; examples I have in mind are theories of graph/group/ring. By natural I mean $\varphi$ should be a property that originates in non-logical context (so it should not be obtained by, e.g. coding arithmetic). By high I mean $\varphi$ should be at least $\Sigma_3$ or $\Pi_3$; I have the feeling that many properties about groups are either $\forall\exists$ or not expressible in first order logic at all.
Admittedly these requirements are quite vague; basically I want to exclude theories like $\mathsf{PA}$ or $\mathsf{ZFC}$. Also note that my question is different from this one.