Do decidable properties of finitely presented groups depend only on the profinitization? This is a just-for-fun question inspired by this one. Let $P$ be a property of finitely presentable groups. Suppose that


*

*The truth of $P(G)$ only depends on the isomorphism class of $G$.

*Given a finite presentation of $G$, the truth of $P(G)$ is computable.
Let $\hat{G}$ denote the profinite completion of $G$. Is it possible to have groups $G$ and $H$, and such a property $P$, so that $\hat{G} = \hat{H}$ but $P(G) \neq P(H)$?
For example, is there a computable property which separates Higman's group from the trivial group?
 A: In this paper, Owen Cotton-Barratt and I construct two finitely presentable groups with isomorphic profinite completions, but such that one is conjugacy separable (implying solvable conjugacy problem) and the other has unsolvable conjugacy problem.
(The construction is very much in the spirit of the paper of Bridson that Daniel Groves mentioned in the comments.)
EDIT:
Sorry, I only just noticed requirement 2.  Since almost no properties are computable from a finite presentation, and yet the class of properties computable from a finite presentation is mysterious (eg does it include having a proper finite-index subgroup?), I don't see how you'll get any interesting answers with condition 2.
FURTHER EDIT:
As Bjorn explained to me in the comments to David's answer, it's not nearly as hard as I had thought to build two fp groups with the same profinite completion.  Indeed, there are virtually abelian examples.  As one can solve the isomorphism problem for virtually abelian groups, it follows that there examples of computable properties that are not determined by the profinite completion, as David's answer shows.
A: OK, I think I have an example of two groups with the same profinitization and a computable property which distinguishes them. The point is that very fine detail about the commutator subgroups can't be seen in the profinitization.
Let $q$ be prime and let $K$ be the $q$-th cyclotomic field.
Choose $q$ such that the class group of $K$ is not trivial. Let $I$ be a trivial ideal of $\mathcal{O}_K$ and $J$ a nontrivial ideal. Our groups $G$ and $H$ will be $(\mathbb{Z}/q) \ltimes I$ and $(\mathbb{Z}/q) \ltimes J$.
For any group $B$, let $B' = [B,B]$ and $B'' = [B', B']$. Note that $B/B'$ acts on $B'/B''$ by conjugation. Our computable criterion is the following:

$B/B' \cong \mathbb{Z}/q \times \mathbb{Z}/q =: A$, the action of the group ring $\mathbb{Z}[A]$ on $B'/B''$ factors through a map $\mathbb{Z}[A] \to \mathcal{O}_K$ and, as such, $B'/B''$ is a free $\mathcal{O}_K$ module.

We leave it as an exercise that $G$ satisfies this condition and $H$ does not. 
I believe this condition should be computable. We can go from a finite presentation of $B$ to one of $B'$. (UPDATE I have revised this argument.) Abelianizations are computable, so we can check whether $B/B'$ has the right format. If it does, then $B'$ has finite index in $B$. I think we can use this to get a finite presentation of $B'$: Let $\Delta$ be a two-dimensional $CW$-complex with one vertex, an edge for each generator of $B$ and a two cell for each relation. Let $\Delta'$ be the cover of $B$ corresponding to $B'$. Since $B$ has finite index in $B'$, $\Delta'$ will have finitely many cells, and we get a finite presentation of $B'$.
We can the compute the abelianization of $B'$ and, I think, the action of the abelianization of $B$ on that of $B'$ should be computable. Note that there are only $q^2$ maps from $\mathbb{Z}[A]$ to $\mathcal{O}_K$, so we can just check them each in turn. The class of a finite generated module for a Dedekind domain should be computable by standard number theory methods, although I admit I couldn't describe them.
The fact that these two groups have the same profinitization is relatively well known. Let $\hat{I}$ and $\hat{J}$ denote the profinite completions of $I$ and $J$. The profinite completions of $G$ and $H$ are $\mathbb{Z}/n \ltimes \hat{I}$ and $\mathbb{Z}/n \ltimes \hat{J}$.
We can identify $\hat{I}$ and $\hat{J}$ with submodules of $\mathbb{A}^0_K$, the integral adeles of $K$. Since $I$ and $J$ are locally principal, these are principal ideals in the ring $\mathbb{A}^0_K$. They are thus equivalent as $\mathbb{A}^0_K$ modules, and thus as $\mathcal{O}_K$ modules. 
A: Is it decidable from a presentation whether or not a group is large, i.e. admits a homomorphism onto the nonabelian free group on two letters? This seems totally unlikely, and surely either Henry or Daniel would know, but I like the following theorem anyway, so I'll advertise. Lackenby showed (`Detecting large groups', GR/0702571) that largeness is a property of the profinite completion of discrete finitely presented groups.
