Given group theory axioms
- $\forall x\forall y\forall z,~x(yz)=(xy)z$
- $\forall x,ex=xe=x$
- $\forall x\exists y, xy=yx=e$
How to formalize the theorem that "a group of prime rank is cyclic"? Since "$|G|$ is a prime" is a predicate that refers to the domain of a model itself, how can we formalize it within this first order theory?
I'll answer to the clearer version I gave in the comments. If that's not what you want then you can tell me.
For the rest of this answer, we consider theories over the language $L=\{\cdot, e\}$ (or $\{\cdot, e ,^{-1}\}$ would work as well)
There cannot be a theory $T$ such that if $G$ is a group, then $G$ is finite of prime order iff $G\models T$.
Indeed, there are infinitely many primes so the compactness theorem implies there is no such theory $T$ (by the usual theorem "If a theory $T$ has arbitrarily large finite models, then it has models of arbitrarily large (possibly infinite) cardinality")
Similarly, by the usual trick of adding constants (see for instance the beginning of a proof of the upward Löwenheim-Skolem theorem), and by noting that a cyclic group is at most countable, there is no first order theory $\Sigma$ in $L$ such that $G\models \Sigma$ iff $G$ is cyclic.
Therefore, the theorem "A group of prime order is cyclic" cannot be stated in the form "If $G\models T$ then $G\models \Sigma$", or a fortiori in the form "$\mathbf{Grp} \vdash \phi \to \psi$" where $\mathbf{Grp}$ is the theory of groups in $L$.