I am working on a problem and I am wondering if what I am trying can even be done.
Assume that we are given a finite group $G$ by it's presentation via generators and relations. For example $$G = \langle a,b\mid a^2=b^2, a^4=1, bab^{-1}=a^{-1} \rangle .$$ I would like to know if there is a way to obtain from this set of relations a finite axiomatization of the group in the sense of Tarskis finite basis problem.
For this group in particular one can produce the finite basis directly with relative ease (it is the quaternion group), I am however wondering if it could be done this way in order to apply the method to some more complex groups.
I would like to know if there is a way to obtain from this set of relations a finite axiomatization of the group in the sense of Tarskis finite basis problem.
I interpret the question to mean:
Is there an algorithm that accepts as input a finite group presentation and that provides as output a finite basis of identities for the presented group.
The answer is No. The existence of such an algorithm would be inconsistent with the following two facts:
For the first item see the discussion here. For the second item, proceed as follows. Suppose that $\Sigma=\{w_1\approx 1, \ldots,w_k\approx 1\}$ is a finite set of identities, and we wish to determine if this set is a basis of identities for the one-element group. For this it is necessary and sufficient that for every $p$ we have $\mathbb Z_p\not\models \Sigma$. One can check this for all $p$ simultaneously, as follows. For each identity $(w_i\approx 1)\in \Sigma$, where $w_i=w_i(x_1,\ldots,x_m)$, create all specializations $w_i(x,1,1,\ldots,1)\approx 1$, $w_i(1,x,1,\ldots,1)\approx 1$, $\ldots,$ $w_i(1,1,1,\ldots,x)\approx 1$ and collect the results into a set $\Gamma = \{x^{n_1}\approx 1, \ldots, x^{n_r}\approx 1\}$ of identities involving the variable $x$ only. Argue that $\mathbb Z_p\models \Sigma$ iff $\mathbb Z_p\models \Gamma$ iff $p$ divides $\gcd(n_1,\ldots,n_r)$. Thus $\Sigma$ is a basis of identities for the one-element group iff $\gcd(n_1,\ldots,n_r)=1$.
Now let me say why the algorithm sought in the original post is inconsistent with Items 1 and 2. If the desired algorithm existed, then one could input a finite group presentation, convert it to a basis of identities with the algorithm, then (using Item 2 above) test if the basis axiomatizes the one-element group. This would provide an algorithm to test if a finite presentation presents the one-element group, contradicting Item 1 above.