It is well known that the isomorphism problem for finitely presented groups is unsolvable. That is to say that if $G$ and $G'$are both fp- groups, then in general it is impossible to provide an algorithm that will determine whether or not they are the same. This remains true even if $G'$ is replaced with the trivial group. This raises two questions.
- Does there exist a group $G$ such that the isomorphism problem with the trivial group is undecidable? In other words, is their a group such that the triviality of $G$ is independent of ZFC?
2.Is there an explicit example of such a group (undecidable isomorphism problem with the trivial group) with the presentation written out explicitly?
Remarks and corrections
I realize that I have two notions of undecidability going through my head. Th first is whether or not their is a procedure (using Turing machines, for example) to answer the question. I suppose that this means asking whether or not the function that returns one if the group is trivial and zero if it is non-trivial is un-computable (for my example). In formulating the question I was think that I was using some (vague) correspondence or relationship between provability and computability. I do have further questions about the exact relationship and perhaps how to leverage the two notions against one another to obtain uncompuatbility and unprovability results. After all I think that their is some Howard-Curry correspondence, but I do not know if that helps me with my problem. Ultimately my question is:
1'. Does there exist an fp group $G$ such that within ZFC, the statements "$G$ is a trivial group" and "$G$ is not a trivial group" are independent of the axioms of ZFC.
2'. Is there an explicit example of such a group in (1') with generators and relation explicitly in the literature?
3' For both 1' and 2', where in the literature?