The following is more or less taken from page 6 of C. Smorynski's "Self-Reference and Modal Logic". (Springer, 1985)
(I couldn't get raised brackets to indicate codification (Gödel numbering), so I use a box.
The overline is assigning a name.
The detail I would like clarification on is in...