Is there a 0-1 law for the theory of groups?
For each first order sentence $\phi$ in the language of groups, define :
$$p_N(\phi)=\frac{\text{number of nonisomorphic groups $G$ of order} \le N\text{ such that } \phi \text{ is valid in } G}{\text{number of nonisomorphic groups of order} \le N}$$
Thus, $p_N(\phi)$ can be regarded as the probability that $\phi$ is valid in a randomly chosen group of order $\le N$.
Now define $$p(\phi)=\lim_{N \to \infty}p_N(\phi)$$ if this limit exists.
We say that the theory of groups fulfills a first order zero-one law if for every sentence $\phi$, $p(\phi)$ exists and equals either $0$ or $1$. I'm asking myself whether this 0-1 law holds indeed in group theory.
Since it is conjectured that "almost every group is a 2-group", statements like $\exists x: x\ne 1 \wedge x^2=1 \wedge \forall y:xy=yx$ (meaning $2|Z(G)$) or $\forall x: x^3=1 \to x=1$ (no element has order 3) should have probability $1$ and I don't see any possibility to construct any sentence with $p\not \in \{0,1\}$. Am I missing an obvious counterexample, or can you show (under the condition that almost every group is indeed a 2-group) that the theory of finite groups fulfills this 0-1 law?
Sharing the question within MO has brought some interesting comments - I send you there for reference - but in the last 2 years there has been no new contribution. So I'm wrapping it up for the less technical scope of SE:
As per now, a FO 0-1 law for group theory as defined by Dominik doesn't exist and may never exist.
The consensus seems to be that an accepted and complete view of what group theoretic concepts correspond to in a classical logic framework is needed to address the problem but - as per now - it is not available.
The actual methods available to cross-translate group theoretic concepts into logic ones seem to suggest that such a law cannot exist for the whole group theory or even for finite group theory. Limiting laws have infact been identified such that group theoretical entities can be partitioned into different classes exhibiting different logical behaviours (i.e. quantification over functions which is ubiquitous in group theory; but also abelianity appears to be relevant). While yet to be proven, some of these classes can be expected to obey a 0-1 law for FOL while some others can be expected to not obey it.