Q:

Conjugacy problem in a conjugacy separable group

Here is a question that has been bothering me for some time:
Let G be a finitely generated conjugacy separable group with solvable word problem. Does it follow that the conjugacy problem in G is solvable?
Background. A group G is said to be conjugacy separable is for any two non-conjugate elements x,y in G there is a homomorphism from G to a finite group F such that the images of x and y are not conjugate in F. Equivalently, G is conjugacy separable if each conjugacy class is closed in the profinite topology on G.
A well-known theorem of Mal'cev states that a finitely presented conjugacy separable group has solvable conjugacy problem (in this case it is possible to recursively enumerate all the finite quotients, simultaneously checking conjugacy of the images of two given elements in each of them).
On the first page of the paper 'Conjugacy separability of certain torsion groups.'
(Arch. Math. (Basel) 68 (1997), no. 6, 441--449.) Wilson and Zalesskii claim that the conjugacy problem is solvable in finitely generated recursively presented conjugacy separable groups (which, of course, implies a positive answer to my question), and refer to a work of J. McKinsey, 'The decision problem for some classes of sentences without quantifiers' (J. Symbolic Logic 8, 61 – 76 (1943)). 
However, I could not find anything in the latter paper that would allow to deal with infinite recursive presentations. Moreover, the corresponding property for residually finite groups simply fails. More precisely, there exist finitely generated residually finite recursively (infinitely!) presented groups with unsolvable word problem (cf. 'A Finitely Generated Residually Finite Group with an Unsolvable Word Problem' by S. Meskin, Proceedings of the American Mathematical Society, Vol. 43, No. 1 (Mar., 1974), pp. 8-10).

A:

I think that the issue here may be: if you have a finitely generated, residually finite group, with solvable word problem, then can you detect a homomorphism to a finite group? 
By this, I mean you have finite set of generators, and an algorithm which will tell you when a word in that set of generators gives the trivial element. One can enumerate potential homomorphisms to a finite group, by sending every generator to every possible element in the finite group. You can tell if such an assignment does not give a homomorphism, by finding an word in the generators which is trivial in the group, but which is not sent to 1 in the finite group. But if it is indeed a homomorphism, you might never definitively know, since you will always find that trivial elements are sent to the trivial element. 
A related question is: can you tell when a recursively defined set of polynomial equations defines a trivial affine variety (a single point)? We know that only finitely many polynomials are needed to cut out the variety by the Nullstellensatz, but how do we know how to choose such a finite set algorithmically? If one knew how to do this, then one could answer your question. This might be something well-known to algebraic geometers or logicians. 

