不完全性定理についてのゲーデルの証明

 g[g]は無限ループ…。あれ？私は不完全性定理を理解していたはずなのに理解できないぞ。valid-proofQ の表現に与式が g[g] であるかを有限時間でチェックするような有限長の表現の改変を加えることはできないということ？