>>15は正確には
第二不完全性定理の証明のために、証明を形式化して自然数にコーディングするとき
と言うべきなのかな、たぶんだけど

>>18
不完全性定理の証明がヒルベルト的思想に適う形で成されたのであって、
別にヒルベルトが不完全性定理を証明しようとしてたわけではないでしょ