# solvable word problem without algorithm

Let $G$ be a finitely generated group. I wonder if there are examples where:

1) The word problem is known to be solvable in $G$ but there is no algorithm known.

2) The word problem is known to be solvable in $G$ but it is also known that no algorithm for solving the problem can be exhibite.

3) the same as 1) and 2) but with other decisional problems.

$\$

Is 2) really possible? The question relies on the difference between "$\exists x$" and "showing an $x$". It seems to me that if $G$ has solvable problem then, by definition, an algorithm $A$ that solves the problem exists. Since algorithms are build up from finite objects, in principle I can enumerate all of them and eventually find $A$ (but how can I be sure that $A$ solves the word problem for $G$?). Am I making a big confusion or the question makes sense?

-
2) should be formulated in a way to make sense, what's the input? Right now it sounds like "given a non-empty subset of positive integers, can we exhibit an element in this set?" –  YCor Jul 8 at 12:37
Do you mean is there a fg group with a solvable word problem but for which it is undecidable if a Turing machine accepts the word problem? –  Benjamin Steinberg Jul 8 at 13:52
Basically there is a big difference between knowing an algorithm exists and constructing it. –  Benjamin Steinberg Jul 8 at 14:00
@YCor There are in fact similar results to (2) in graph theory; the Robertson-Seymour theorem essentially says that every family of graphs that's closed under the operation of taking minors is the compliment of a union of cones, but there can be no algorithm for taking a description of a minor-closed family and producing the minimal elements of its compliment; see mathoverflow.net/a/48025/7092 –  Steven Stadnicki Jul 8 at 15:47
@StevenStadnicki I'm aware that these kind of results exist, but they ought to be stated in a proper way, which is, I'm afraid, not the case. What's the input? A "f.g. group with solvable word problem" is not an input. Should it be understood that the input is a recursive presentation and the question is whether, when the resulting group has solvable word problem, the output provides a algorithm? Possibly there are other interpretations of the question, and for this reason I don't consider it's asked in a proper way. –  YCor Jul 8 at 19:05