Is having a Frobenius pair first-order expressible in the language of groups? 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.
 A: 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.
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).]
