Element being trivial in a finitely presented group independent of ZFC

Question

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?

Answer 1

The answer is yes.

This is just an instance of the general phenomenon that every non-computable 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.

Answer 2

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?