MathOverflow will be down for maintenance for approximately 3 hours, starting Monday evening (06/24/2013) at approximately 9:00 PM Eastern time (UTC-4).
show/hide this revision's text 3 Added negative answer to main question assuming that the set of decidable properties to be used is listable

I'm not yet sure about

EDIT: As for your first "main question" asking whether decidable properties can distinguish every pair of non-isomorphic finitely presented groups, but I am pretty sure that I'll prove the answer following negative result:

There is going to be no c.e. set $\mathcal{F}$ of decidable properties such that there are any two non-isomorphic finitely presented groups that cannot can be distinguished by some $\phi \in \mathcal{F}$.

(Call a set $\mathcal{F}$ of decidable properties c.e. if there is a Turing machine that produces a sequence of algorithms, each of which is guaranteed to compute a decidable property, such that these decidable properties are exactly the ones in $\mathcal{F}$.)

Proof: Suppose that $\mathcal{F}$ exists. Then we could decide whether an arbitrary finitely presented group $G$ is trivial as follows: By day, search for an isomorphism between $G$ and $\{1\}$ (this search is possible since the isomorphism relation is c.e.) By night, search for a decidable property $\phi \in \mathcal{F}$ such that $\phi$ distinguishes $G$ and $\{1\}$. If $\mathcal{F}$ does what it claims to, then one of these processes will terminate and tell you whether $G \simeq \{1\}$. But triviality is known to be an undecidable property. $\square$

This leaves open the question of whether there is a non-c.e. $\mathcal{F}$ that does the job, but even if there were one, it wouldn't be of much use from the practical point of view!
show/hide this revision's text 2 fixed typos

The isomorphism relation for finitely presented groups is c.e., and in fact is Turing equivalent to the halting problem.

Proof: To check whether two finitely presented groups $G$ and $H$ are isomorphic, search for data that might describe maps $G \to H$ and $H \to G$ and for words that show that it is a consequence of the relations that the composition in either order maps each generator to itself, and verify that the relations of $G$ maps map to $1$ in $H$ and vice versa so that the maps are well-defined and that the remaining data shows that they are inverse isomorphisms. Thus the isomorphism relation is c.e. It is also no easier than the halting problem, because an algorithm even for deciding whether a finitely presented group is trivial could be used to solve the halting problem. (That is how it is known that triviality is an undecidable property, by reductions passing through the word problem along the way.) $\square$

I'm not yet sure about your first question, but I am pretty sure that the answer is going to be that there are finitely presented groups that cannot be distinguished by decidable properties.
show/hide this revision's text 1

The isomorphism relation for finitely presented groups is c.e., and in fact is Turing equivalent to the halting problem.

Proof: To check whether two finitely presented groups $G$ and $H$ are isomorphic, search for data that might describe maps $G \to H$ and $H \to G$ and words that show that it is a consequence of the relations that the composition in either order maps each generator to itself, and verify that the relations of $G$ maps to $1$ in $H$ and vice versa so that the maps are well-defined and that the remaining data shows that they are inverse isomorphisms. Thus the isomorphism relation is c.e. It is also no easier than the halting problem, because an algorithm even for deciding whether a finitely presented group is trivial could be used to solve the halting problem. (That is how it is known that triviality is an undecidable property, by reductions passing through the word problem along the way.) $\square$

I'm not yet sure about your first question, but I am pretty sure that the answer is going to be that there are finitely presented groups that cannot be distinguished by decidable properties.