In ZFC, we can easily say when a triple $\mathscr{G}=\left\langle G,\cdot,1 \right\rangle $ is a group. Furthermore, we can say when a group is finitely generated: First define a "canonical" finitely generated group on $n$ generators by taking the set of all finite ordered tuples of elements from a fixed set of size $n$ ("words in these elements"), and defining the usual equivalence relation that will make the set of equivalence classes into a group. Second, a f.g. group will be a group isomorphic to some quotient of that canonical f.g. group (I believe we can say all this in ZFC, please correct me if I'm mistaken).
So now the question is - will every statement about f.g. groups be decidable in ZFC? Put differently - can any statement about these groups be independent of ZFC? What about finitely presented groups (where the the group in the quotient is itself f.g.)?
For reference, I think of Whitehead's problem that was shown by Shelah to be independent of ZFC. The main difference is that here we are dealing with things that have some finiteness in them, so it is less clear to me whether they can be so manipulated.