私はずっと>>577を念頭に置いてましたので、形式的証明とは完全性定理が存在を主張しているところのものです。