Group presentation in the category of finite group

Question

Context: I'm trying to deal with presentations in the framework of Gonthier et al. formalization of the group theory in the proof assistant Coq. It was used to machine check the Feit-Thompson odd order theorem. In this formalisation, all groups are assumed to be finite and it would be a lot of work to remove the assumption. Actually, roughly speaking, all sets are assumed to be finite.

Summary question: Is there a finite group $G$ with a presentation where one of the relation can be deduced by the kownledge that $G$ is finite.

I'd like to define a presentation as follows: Let $I$ be a finite set and $R$ be a finite collection of word in $I$. For any finite group $G$, and any map $g:I\to G$, I say that $(g, R)$ is a presentation of $G$ iff

1. $\{g(i) | i \in I\}$ generate $G$;
2. The relations $R$ holds in $G$, that is for any $r\in R$, then $\prod_{i : r} g(i) = 1$;
3. For any finite group $H$ and any map $h : I \to H$, if $\prod_{i : r} h(i) = 1$ holds for any $r\in R$, then there is a group morphism $\phi : G \to H$ such that $\phi(g(i))=h(i)$ for all $i\in I$.

Allow me to stress once again that the universal properties of condition 3. only holds for finite groups.

My question is: does this coincide whith the usual definition of presentation ?

In particular, I'd like to prove that any word in the $\{g(i)\}$ is $1$ if it can be written as a concatenation of relators or their conjugates. But in order to do that I usually need to consider the quotient of the free group by the normal subgroup generated by the relators. However to prove that this quotient is finite, I need the exact propoerty I'm trying to prove.

Here is a rephrasing of my question:

Suppose that a finite group $H$ satisfies some relations $R$ ($R$ finite) on some generators $h_i$ ($I$ finite). Suppose that a word $w$ in the $h_i$ is equal to $1$ in $H$ but can't be written as a concatenation of the conjugate of the relators in $R$. Does there always exists a finite group $H'$ such that $H$ is a homomorphic image of $H'$ but $w$ is not $1$ in $H'$ ?

[edit] added ($R$ and $I$ finite in the above rephasing).

Answer 1

A well-known example, due to G. Higman, of an infinite finitely presented group with no nontrivial finite quotients is $$G = \langle a,b,c,d \mid a^{-1}ba=b^2,b^{-1}cb=c^2,c^{-1}dc=d^2,d^{-1}ad=a^2 \rangle.$$ Proving it has no nontrivial finite quotients is elementary and a nice exercise. The idea is to prove that $f(a) < f(b) < f(c) < f(d) < f(a)$, where $f(g)$ is the smallest prime factor of the order of $g$ in a candidate for a nontrivial finite quotient.

Proving it infinite can be done using the fact that the group is an amalgamated product of two HNN extensions: see here for example.

But according to your definition of a presentation of a finite group, this presentation would define the trivial group, because there are no other finite homomorphic images of $G$.

So the answer to your question is no, your definition of a presentation of a finite group is not equivalent to the standard notion of a group presentation.