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?