I am trying to figure out whether or not the following property is first-order expressible in the language of groups.
$$\text{$G$ has a subgroup $H$ with which it forms a Frobenius pair $(H,G)$.}$$
My search online yielded no answers. Even if there is a positive or negative result, it seems to be not very well-known.



Is having a Frobenius pair first-order expressible in the language of groups?
I'll answer here positively the natural variant of the question:



> 
> does there exist a 1st order sentence such that for every finite group $G$, the group $G$ is Frobenius over some subgroup iff the given sentence holds in $G$.
> 
> 
> 


In a sense, this sound to me like a more natural question, since Frobenius pairs are really motivated by finite group theory, and such a result allows to extend the notion to pseudofinite groups.


(Concerning infinite groups, my bet would be that the result is false although I can't prove it at the moment.)


In a group $G$ and $g\in G$, write $C\_g$ the centralizer of $g$, and $L\_g=\{h:[g,hgh^{-1}]=g\}$. Let $A\_G$ be the set of elements of $G$ which commute with all their conjugates (i.e., are contained in some abelian normal subgroup). Let $B\_G$ be the set of $g\in G$ such that $C\_g$ is a normal subgroup, and $B'\_G$ the set of $g\in B\_G$ such that every element of $G\smallsetminus C\_g$ acts by conjugation on $C\_g$ with no nontrivial fixed point. Let $D\_G$ be the set of $g\in G$ such that $L\_g$ is a subgroup.


**Proposition.** A group is Frobenius iff there exists $z\in B'\_G\smallsetminus\{1\}$ and $h\in D\_G\smallsetminus\{1\}$ such that $G=C\_z\rtimes L\_h$.


*Proof:* For basic facts on Frobenius pairs see the [Wikipedia page](https://en.wikipedia.org/wiki/Frobenius_group).
Suppose $G=K\rtimes H$ is Frobenius. So $K$ is nilpotent (Thompson) and nontrivial, choose any central $z\in G$: then $K=C\_z$ and $z\in B'\_G$. Also, $H$ is a Frobenius complement, and hence has a nontrivial solvable radical (follows from results of Zassenhaus: it is indeed either solvable and nontrivial, or has a normal copy of $\mathrm{SL}\_2(\mathbf{F}\_5)$, which has a nontrivial center), hence has a nontrivial abelian normal subgroup; choose $h$ therein. Then $L\_h=H$ follows easily: choose $g\in L\_h$ since if $[h,ghg^{-1}]=1$ and the centralizer of $h$ is contained in $H$ it follows that $ghg^{-1}\in H$ and in turn $g\in H$ follows.


Conversely, if $G$ has these properties, then it is straightforward that $L\_h$ is malnormal (i.e. $L\_h\smallsetminus\{1\}$ is disjoint each from its conjugates by elements not in $L\_h$) and this implies that $G$ is Frobenius.$\Box$


Now the property of the proposition is obviously expressible by a first-order sentence $F\_0$ in $G$. Hence for every finite group $G$, $G$ satisfies $F\_0$ iff $G$ is Frobenius.


In particular, we can define a pseudofinite group to be Frobenius iff it satisfies $F\_0$. Note that this does not depend on $F\_0$. This can be defined directly as: a group $G$ is pseudofinite Frobenius if for every 1st order sentence $F$ satisfied by $G$ there exists a finite Frobenius group satisfying $F$.


While the latter could be defined in any case, the existence of $F\_0$ above ensures the following: if a group $G$ is pseudofinite Frobenius, then there exists a 1st order formula $F$ such that every finite group $G'$ satisfying $F$ is Frobenius. (More informally: it means that a pseudofinite group cannot be both pseudo-Frobenius and pseudo-(non-Frobenius).)


[For context, there also exists a first-order formula that characterizes, among finite groups, the solvable ones (Wilson). But there is none that characterizes, among finite groups, the nilpotent ones (YC-Wilson).]


