Is there an explicit finitely presented group $G$ and an element $g\in G$ such that the statement "$g$ is equal to the identity" is independent of ZFC?

2$\begingroup$ It depends what 'explicit' means; you can define $G = \langle a\rangle/N$, where $N = \langle a\rangle$ or $N = 1$ depending on whether the continuum hypothesis is true. $\endgroup$ – LSpice Apr 21 at 18:30

2$\begingroup$ @LSpice by explicit I mean state the number of generators and then write down the relations $\endgroup$ – Oniqa Apr 21 at 18:37

4$\begingroup$ There are explicit polynomials in $\Bbb Z[x_0,\dots]$ which have roots if and only if ZFC is inconsistent. Surely you can use one of them to engineer a group that is trivial if and only if ZFC is inconsistent. $\endgroup$ – Asaf Karagila♦ Apr 21 at 21:27
The answer is yes.
This is just an instance of the general phenomenon that every noncomputable decision problem is saturated with logical independence. (See this related MO answer.)
Theorem. If $A$ is a computably enumerable undecidable decision problem, such as the word problem for groups, then for any consistent c.e. theory $T$ extending PA, such as ZFC, there must be true instances of $n\notin A$ that are not provable in $T$.
Proof. Suppose that $T$ is a consistent c.e. theory extending PA. It follows that all the true instances of $n\in A$ are provable in PA and hence in $T$. If conversely $T$ proved all true instances of $n\notin A$, then we could decide $A$ as follows: on input $n$ we search, during the day, for positive instances of $n\in A$, since $A$ is c.e., and at night, we search for a proof from $T$ that $n\notin A$. Since $T$ is consistent and proves all true existentials, it can be trusted for any proof of $n\notin A$. So if all such true instances of $n\notin A$ were provable in $T$, then $A$ would be decidable, contrary to assumption. $\Box$
In particular, if ZFC is consistent, then there must be specific concrete instances of the word problem where a word $g$ is nontrivial for a specific presentation, but this is not provable in ZFC.
If you want to get actual independence of ZFC, then you can do so by assuming that ZFC is $\Sigma_1$sound, which means that it proves only true existential arithmetic statements. If there is an inaccessible cardinal or even only a worldly cardinal, then ZFC is $\Sigma_1$sound. But much less is required.
Corollary. If $T$ is a consistent c.e. $\Sigma_1$sound theory, then for any c.e. computable undecidable decision problem $A$, there must be concrete instances $n$ for which $n\in A$ is independent of $T$.
Proof. The point is that if we have a true instance of $n\notin A$ that is not provable in $T$, then also by soundness $T$ will not prove $n\in A$, and so $n\in A$ will be independent of $T$. $\Box$
In particular, assuming ZFC is $\Sigma_1$sound, which is a mild extra assumption about ZFC, then for any nondecidable decision problem, such as the word problem for groups, there will be concrete instances that are independent of ZFC.
But finally, since I expect that you might want not just a proof that there is an explicit instance, but the explicit instance itself, let me describe how one might construct a specific instance. We know that the word problem in groups is undecidable because we can code the halting problem into it. Consider the Turing machine that searches for a proof of a contradiction in ZFC, halting only when found. From this instance of the halting problem, we can construct an group presentation $G$ and a word $g$ which is trivial in $R$ just in case the program halts. In other words, $g=1$ is true in $G$ if and only if $\neg\text{Con}(\text{ZFC})$, and this would be provable in a weak theory. If consistent, ZFC will not prove $g\neq 1$, since that would mean proving its own consistency; but if also $\text{Con}(\text{ZFC})$, then ZFC will not prove $g=1$ in $G$. And so it will be independent. This example also reduces the soundness requirement to mere consistency.

2$\begingroup$ It can only be independent when it is not true. So there is some nonstandard model of ZFC where $g=1$, but in our universe, $g\neq 1$. $\endgroup$ – Joel David Hamkins Apr 21 at 20:50

2$\begingroup$ The general fact used in my answer is that every true existential arithmetic statement is provable in PA and ZFC. So if such a statement is independent, it must not be true. But there are models going both ways, and that is what independence amounts to. $\endgroup$ – Joel David Hamkins Apr 21 at 20:56

2$\begingroup$ @HJRW: You may be interested in the following answer, which not surprisingly is again by Joel. mathoverflow.net/a/27677/33039 Suppose that you prove in $ZFC$ that a $\Pi_1$sentence $\varphi$ (such as "the Turing machine blah blah does not halt") is independent of $ZFC$. In particular, you can prove in $ZFC$ that $Con(ZFC) \rightarrow Con(ZFC+\varphi)$. Then you can prove $\varphi$ from $ZFC+Con(ZFC)$, but not $ZFC$ alone. So this does not contradict that it is independent of $ZFC$. $\endgroup$ – Burak Apr 21 at 21:07

2$\begingroup$ @MaximeRamzi Providing the actual group presentation will be extremely detailed and finicky, since it will involve implementing all the encoding of the halting problem of that rather complicated program into the word problem. I'm not sure if this has ever actually been done in practice. So this is a pureexistence proof of an explicit object, which I fully admit may not be seen as satisfactory except in theory. $\endgroup$ – Joel David Hamkins Apr 21 at 21:07

2$\begingroup$ In this paper arxiv.org/abs/1605.04343, the authors provide a 7910state Turing machine whose behavior is independent of ZFC. I think most people think the true bound is considerably less, but proving this is finicky. $\endgroup$ – Joel David Hamkins Apr 22 at 6:57
For any finite presentation there is an algorithm that will tell you if a word is equal to the identity: 1. Fix some positive integer $n$. 2. Write down all words in the generators that can be written as a product of at most $n$ conjugates of the given relators by elements that can be written as a product of at most $n$ of the given generators and their inverses. 3. If none of these words is equal (as a reduced word) to your given group element, increase the value of $n$ and repeat.
If your word is not equal to the identity, the algorithm will not terminate.
If you had a proof that ZFC could not show that your word was equal to the identity, then doesn't the above algorithm imply that it is not equal to the identity?

2$\begingroup$ @LSpice : that’s not the problem with this answer: IJL is describing the semi algorithm that solves half the word problem in any fp group. $\endgroup$ – HJRW Apr 21 at 20:24

1$\begingroup$ I think the problem is that in some models, the algorithm may terminate after a nonstandard natural number of steps. $\endgroup$ – Tobias Fritz Apr 21 at 20:35

1$\begingroup$ @LSpice; step 3 is to decide if they’re equal as words in the free group. As you say, the word problem in free groups is decidable! $\endgroup$ – HJRW Apr 21 at 20:43

1$\begingroup$ Got it, thanks. Sorry, fuzzy endofsemester thinking here. $\endgroup$ – LSpice Apr 21 at 20:49

4$\begingroup$ Based on JDH’s comments above, this answer just proves that such a g is certainly nontrivial in “the real world”, in the sense that the semialgorithm that tries to prove that g=1 never halts. But apparently that’s not enough to make $g\neq1$ a theorem of ZFC. $\endgroup$ – HJRW Apr 21 at 20:57