Is there a homomorphism of finitely presented groups $f:G\to H$ and an element $h\in H$ such that the statement "$f^{1}(h)$ is empty" is independent of ZFC?

$\begingroup$ It seems to me that any homomorphism between finitely presented groups is computable, whatever it means. Do I miss something? $\endgroup$ – YCor Apr 21 at 17:48

$\begingroup$ We can take $f$ a morphism taking everything to identity. Then for appropriate $H$ we have that ZFC can't tell whether $H$ is nontrivial, so it can't check the nontriviality on all generators. $\endgroup$ – Wojowu Apr 21 at 17:50

$\begingroup$ @Wojowu isn't the preimage of the identity always nonempty? $\endgroup$ – Oniqa Apr 21 at 17:51

$\begingroup$ @Oniqa But ZFC won't be able to prove that these elements are or aren't identity. $\endgroup$ – Wojowu Apr 21 at 17:53

$\begingroup$ @Wojowu but the identity is certainly getting sent to the identity $\endgroup$ – Oniqa Apr 21 at 17:54
The answer is yes, as a consequence of my answer to your other question.
Namely, in that answer, we have a finite group presentation $H$ and a word $h$ such that the question $h=1$ in $H$ is independent of ZFC. So if we take $G$ to be trivial and $f:G\to H$ the unique homomorphism, we have the statement "$f^{1}(h)$ is nonempty" being independent of ZFC.
The general lesson of that answer supplies also an answer to Benjamin Steinberg's comment here concerning a confusion between computable undecidability and ZFC or logical undecidability. The general lesson, which I argue on the other post, is that every computably undecidable enumerable decision problem is saturated with logical undecidability. So the two notions of undecidability are actually intimately connected.

$\begingroup$ But the independence from ZFC thing seems to make some assumptions about cardinals $\endgroup$ – Benjamin Steinberg Apr 22 at 2:11

$\begingroup$ @BenjaminSteinberg The $\Sigma_1$correctness was only for the very general fact. Meanwhile, the example at the end of my other answer produces a ZFC independent instance assuming only Con(ZFC), which is required in order to have anything independent of ZFC. $\endgroup$ – Joel David Hamkins Apr 22 at 8:35