＞不完全性定理の証明はそれほど難しくはないのです。

てゆーか、面倒くさい。算術だけで言語の処理系を作るのに近いからね。

＞肯定も否定も出来ない自己言及を形式的体系にどう組み込むか

ただ解決のヒントは、すでにカントルやラッセルのパラドックスに
秘められてたわけだからね。あとは証明のチェックが計算可能で
あることを示せばよい。といってもそこが実際は面倒なわけだが。

＞厳密さを如何にステップバイステップで示すか

実際にはヒルベルトもその弟子も
「証明のチェックが計算可能であること」
には文句をつけなかったんだけどね。