Is there an injective group operation for infinite groups? I've been wondering if there is any infinite group $G$ with the property that its group operation $ G \times G \to G$ is injective (or some restriction of it). The reason for this is that I am asked to show that there is a first-order sentence whose models cannot be finite groups. It must also be satisfiable. I know that there is no finite axiomatization of infinite groups, so any satisfiable sentence that eliminates the possibility of finite groups must be the answer.
Any help is greatly appreciated.
 A: No, because $e \times a = a \times e = a$.

The reality is much worse. For any $a \in G$, $aG = G = Ga$, so each element is repeated informally as many times as the order of the group.



*

*Associativity: $\forall x \forall y \forall z [(x \times y) \times z = x \times (y \times z)]$

*Identity: $\forall x [x \times e = x = e \times x]$

*Inverse: $\forall x \exists y [x \times y = e = y \times x]$


I don't see how one can make the domain infinite without introducing a new function, so I'll introduce a unary function $S$, with the following first order axioms:


*$\exists z \forall x [S(x) \ne z]$

*$\forall x \forall y [x=y \iff S(x)=S(y)]$


($S$ is basically the successor function copied from Peano Arithmetic with the two axioms being from the same source.)
A: Here are a few strategies for finding a first-order sentence modeled by no finite group but some infinite group off the top of my head.  


*

*Find a finite presentation $\langle R | S \rangle$ of a group $G$ with no finite quotients, and write down the first-order sentence "there exist elements $R$ satisfying the relations $S$, and one of the elements of $R$ is nonzero."

*The above is doable but hard to do from first principles. A bit easier but probably still hard from first principles is to find a finite presentation of a group $G$ which fails to be residually finite, meaning there is some nonzero $g \in G$ which maps to zero in every finite quotient of $G$. Then write down the first-order sentence "there exist elements $R$ satisfying the relations $S$, and the element $g$ (expressed as a word in the generators $R$) is nonzero."

*So far we haven't used universal quantifiers. Here is one option along these lines, which again involves finding a weird group: there exist infinite groups where all of the nonzero elements are conjugate, but this can't happen in any finite group except the trivial group and $C_2$. So we can write down "for all nonzero elements $g, h$, there exists $k$ such that $g = khk^{-1}$, and also there are at least three elements."
A: If I remember correctly what a first-order sentence is, then here's nontrivial and pretty simple example: $$\exists X, Y \forall a, b, c, d \, ( [a^2X, b^{-1}c^2Yb] ≠ d^3).$$ Equation $[a^2X, b^{-1}c^2Yb]d^{3} = 1$ over groups with coefficients $X, Y$ in four indeterminates have solution over every finite group (by Sylow) and no solution in free group $F \langle X, Y \rangle$. Easy way to see this: apply Schutzenberger lemma — no commutator is a proper power in free group; then obvious homomorphism of free group to upper-triangular $3 \times 3$ matrices over almost any ring (e. g. $\Bbb Z / 2$) detects nontriviality of commutator .
A: Introduce two axioms $ \forall x \forall y (xx = yy \Rightarrow x = y) $ and $ \exists x \forall y (x \neq yy) $ works since it says the function $ f(x) = x^2 $ on $ G $ is injective, but not surjective, which is impossible for finite groups. One can easily check that these two axioms are satisfiable for $ (\mathbb{Z}, +) $.
