gr.group theory - Which finitely presented groups can be distinguished by decidable properties?

This question continues the line of inquiry
of these
three
questions.

Question. Which finitely presented groups can be
distinguished by decidable properties?

To be precise, let us say that φ is a decidable property of finitely
presented groups, if there is a class A of finitely
presented groups, closed under group isomorphisms, such that
{ p | 〈p〉 ∈ A } is decidable, where 〈p〉 denotes the group presented by p. That is, we insist that the decision procedure give the same answer for presentations leading to the same group up to isomorphism.

One extreme case, perhaps unlikely, would be that any two non-isomorphic
finitely presented groups can be distinguished by decidable
properties, so that for any two finitely presented
non-isomorphic groups 〈p〉 and 〈q〉,
there is a decidable property φ where φ(p) holds
and φ(q) fails. That would be quite remarkable.

If this is not the case, then there would be two finite group
presentations p and q, such that the groups presented
〈p〉 and 〈q〉 are not isomorphic, but
they have all the same decidable properties. This also
would be remarkable.

Which is the case?

Another way to describe the question is in terms of the
equivalence relation ≡, which I introduced in my
previous question, where p
≡ q if φ(p) and φ(q) have the same answer for
any decidable property φ of finitely presented groups. This
is precisely the equivalence relation of "having all the
same decidable properties". Of course, this includes the
group-isomorphism relation, and the current question is
asking: What is this relation ≡? In particular, is
≡ the same as the group isomorphism relation?
If it is, then any two non-isomorphic finitely presented
groups can be distinguished by decidable properties; if
not, then there are two finitely presented non-isomorphic
groups 〈p〉, 〈q〉 having all the same
decidable properties.

Henry Wilton has emphasized several times that there are
relatively few truly interesting decidable properties of
finitely presented groups. This may very well be true.
Nevertheless, the answers to the previous MO questions on
this topic have provided at least some decidable
properties, and my question here is asking the extent to
which these properties are able to distinguish any two
finitely presented groups.

In particular, in these previous MO questions, Chad Groft
inquired whether there were
any nontrivial decidable properties of finitely presented
groups. John Stillwell's
answer was
that one could decide many questions about the
abelianization of the group. In a subsequent question, I
inquired whether all decidable properties were really about
the abelianization, and David Speyer's
answer was
that no, there were questions about other quotients, such
as whether the group had a nontrivial homomorphism into a
particular finite group, such as A₅. In a third question, David generalized further and inquired
whether all decidable properties depended on the
profinitization, and the answer again was no (provided by David and Henry). So at least
in these cases we have been increasingly able to separate
groups by decidable properties.

A generalization of the question would move beyond the
decidable properties. For example, if we consider the
computably enumerable (c.e.) properties, then we have quite
a lot more ability to distinguish groups. A property is
c.e. if there is a computable algorithm to determine the
positive instances of φ(p), but without requiring the
negative instances to ever converge on an answer. For
example, the word problem for any finitely presented group,
or indeed, for any computably presented group, is
computably enumerable, since if a word is indeed trivial, we will eventually discover this. Using the same idea as David's answer to my question, it follows that the question of
whether a finitely presented group 〈p〉 admits a
nontrivial homomorphism into the integers Z, say, or many other
groups, is computably enumerable. One may simply try out all possible maps of the generators. A generalization of
this establishes:

Theorem. The question of whether one finitely
presented group 〈p〉 maps homomorphically onto (or into) another 〈q〉 is computably enumerable.

The proof is that given p and q, one can look for a map of
the generators of p to the words of q, such that all
relations of p are obeyed by the image in q, and such that
all the generators of q are in the range of the resulting
map. This is a c.e.
property, since one can look for all possible candidates
for the map of the generators of p into words of q, and
check whether the relations are obeyed and the generators
of q are in the range of the map and so on. If they are,
eventually this will be observed, and at the point one can
be confident that 〈p〉 maps onto 〈q〉. More generally, is the isomorphism relation itself c.e.? It is surely computable from the halting problem 0', since we could ask 0' whether the kernel of the proposed map was trivial or not, and it would know the answer.

• Where does the isomorphism relation on finitely
  presented groups fit into the hierarchy of Turing
  degrees? Is it c.e.? Is it Turing equivalent to the Halting problem?

Once one moves to the c.e. properties, it is similarly
natural to move beyond the finitely presented groups to the
computably presented groups (those having a computable
presentation, not necessarily finitely generated). In this
context, the proof above no longer works, and the natural
generalization of the question asks:

• Which computably presented groups are distinguished by
  c.e. properties?

The isomorphism relation on finitely generated computably
presented groups (given the presentations) seems to be
computable from the halting problem for the same reason as
in the proof above, but now one doesn't know at a finite
stage that the proposed map of the generators will
definitely work, since one must still check all the
relations-yet-to-be-enumerated. But 0' knows the answer, so
we get it computably in 0'. In the infinitely generated case,
however, things are more complicated.