In the end, the reason to choose things in that way is because it works, but in this case it's possible to explain what's going on. For a warm-up, you can get some intuition for the method by looking at an easier English example of the same phenomenon: >", when preceded by itself in quotation marks, yields a true sentence.", when preceded by itself in quotation marks, yields a true sentence. To explain the proof you gave, I will use $|n|$ to denote the formula that has Gödel number $n$. In the proof above, $H(n)$ should be read as asserting $F([|n|(n)])$, that is: >$H(n)$ says: $F$ holds of the number of the formula obtained by substituting $n$ into $|n|$ Thus $H([H])$ says, > $F$ holds of the number of the formula obtained by substituting $[H]$ into $|[H]|$ that is, > $F$ holds of the number of the formula obtained by substituting $[H]$ into $H$ So $H([H])$ asserts $F([H([H])])$. (For informal clarity, I have intensionally not used underlines here.) ---- Addendum. It's impossible in general to construct a formula $J$ such that $J$ is literally the same formula as $F([J])$. Any typical Gödel numbering has the property that $n < [F(\underline n)]$ for every formula $F(x)$ and number $n$. But if $J = F([\underline J])$ then $[J] = [F(\underline {[J]})]$. So, if our proof method is going to work with an arbitrary Gödel numbering, is has to be more indirect. The proof gives a formula $H$ so that $H([H])$ is provably equivalent to $F([H([H])])$, but not literally the same formula. This may help explain why proof proceeds the way it does.