# What is the proof that equational logic is undecidable?

Following section 8 of Equational Logic by George McNulty, I understand the approach of reducing this decision to the halting problem by modelling Turing machines with equational theories. The construction is as follows:

Let $$M$$ be a Turing machine with instructions of the form $$(a,b,q,r,D)$$, where $$a$$ is the letter read by $$M$$, $$b$$ is what will replace the letter on the tape (namely $$a$$), $$q$$ is the current state, $$r$$ is the new state, and D is the direction the head moves along the tape (either $$R$$ or $$L$$). We can then build a theory $$\Sigma$$ by, for each letter $$c$$ in our alphabet, adding in the equation

$$F_cG_qF_ax = G_rF_cF_bx$$

for each instruction $$(a,b,q,r,L)$$, and

$$F_cG_qF_ax = F_cF_bG_rx$$

for each instruction $$(a,b,q,r,R)$$.

Note that $$F_x$$ and $$G_y$$ are simply unary operators. We also introduce unary operators H to represent the point beyond which the tape is blank, and J to represent the halting state.

Equipped with this construction, it is clear that every Turing machine computation details a proof in our theory. This tells us that if $$M$$ halts, then

$$\Sigma_M \vdash HG_{q_0}Hx = HJHx,$$

where $$q_0$$ is the initial state, and we assume we are launching $$M$$ on the blank tape.

On the other hand, if we could show that $$\Sigma_M \vdash HG_(q_0)Hx = HJHx$$ implies that $$M$$ halts then we would be done. This is the direction I don't understand. I am having trouble following McNulty's proof.

We do know that if $$\Sigma_M \vdash HG_{q_0}Hx = HJHx$$, then there is a proof of this from our theory because equational logic is complete. Naively, one might think that this proof gives us exactly the steps $$M$$ will take when launched on the blank tape. If the proof is essentially just a list of axioms, then this would be true. But what if the proof uses other rules and is more complex? I am willing to believe that one could still extract the sequence of steps the turing machine will take, but how?