Decidability of word problem for group admitting certain action Let $G$ be a group acting highly transitively (and faithfully) on a set $S$. Suppose that $G$ is finitely presented, and that every stabilizer in $G$ of a finite subset of $S$ is finitely generated. I think I can prove that $G$ embeds in a finitely presented simple group, which in particular implies $G$ has decidable word problem, but I'd like a better understanding of why such a $G$ should have decidable word problem. Is there a pre-existing (and/or more direct) reason that a group admitting such an action should have decidable word problem?
(Edit: Here an action of a group $G$ on a set $S$ is called highly transitive if for all $n\in\mathbb{N}$ the induced action of $G$ on the set of $n$-tuples of distinct elements of $S$ is transitive.)
 A: Yes. There is such a reason.
I will write a subset of $G$ is RE if the set of those words over the generators for $G$ which represent elements of the subset is recursively enumerable.
As IJL argued, since $G$ is finitely presented the subset $\{1\}$ of $G$ containing only the identity is RE. It remains to show that $G \setminus \{1\}$ is RE.
Fix $s$ and $t$ in $S$ and let $H$ be the stabiliser of $s$. Since $H$ is finitely generated $H$ is RE.
Let $f$ be some element of $G$ which moves $s$ and fixes $t$.
Let $M$ be the set of elements of $G$ which conjugate $f$ into $H$. Note that $M$ is RE and $1 \notin M$ but any element $g$ of $G$ with $(t)g = s$ is in $M$.
Let $N$ be the set of elements of $G$ conjugate to some element of $M$. Note that $N$ is RE.
$G$ acts $2$-transitively on $S$ so $N$ is in the set of elements of $G$ which move at least one point of $S$. Which is to say that $N = G \setminus \{1\}$.
In short: $G \setminus \{1\} = \left\{ g \in G \mid \textrm{there exists } h \in G \textrm{ with } f^{\left(g^h\right)} \in H \right\}$.
A: Is there an algorithm to distinguish the elements of the set $S$?  If so, here is a word problem algorithm.  This doesn't seem to use any transitivity properties, just faithfulness.
Start with the positive integer $n=1$.  Given a word $w$ in the generators for $G$, run the standard algorithm to decide if the word can be obtained by freely reducing a product of at most $n$ conjugates of relators by words of length at most $n$ in the generators.  At the same time, take an enumerated list $s_1,s_2,\ldots$ consisting of all of the elements of $S$, and decide whether the $w.s_n\neq s_n$.  If neither of these happens, increase $n$ by one and repeat.
