Computability and logic

Hello,
I am almost half way through Boolos's Computability and logic. It has a
truly magnificent graph of the logical dependence of the chapters,
which I have prestudied with deepest care and respect.

The landscape is outstanding!

Please, may I ask for a reading suggestion, as well as, perhaps, some
kind commentary, as regards a mathematical formulation of a substring
replacement?
With the poorest of tools (intuition) at my disposal at the moment, I
repeatedly tried to give the problem some formulation, but to no avail.
I merely fail to substitute (and compare, of course) formally, and
without the aid of intuition.
I realize that _properly formulated definitions of truth/provability
predicates involve diagonalization, still, in the end, one does apply
rules of inference to theorems (or a state to the tape), whereas I fail
to provide anything plausible _mathematically.

I would not dare ask if I knew the answer were a matter of another
several months or so of self-study.

Thank you very much indeed, and I am sorry for all intrusion.
Tom

.