「正しいが証明できない文が存在する」
適当に無矛盾な理論$ Tを取る．$ \mathbb{N} \models \varphiだが$ T \nvdash \varphiなる文が存在する．
proof
Gödel文$ Gがそう．
$ \mathbb{N} \models Gまたは$ \mathbb{N} \models \lnot Gのいずれか一方だけが成り立つ．
後者の場合
$ \mathbb{N} \models \lnot Gと仮定すると，$ \lnot Gは$ \Sigma_1文であるから$ \Sigma_1完全性より$ T \vdash \lnot G．
$ Gの定義より$ T \vdash G \leftrightarrow \lnot \Box Gであるから，$ T \vdash \Box Gであり，$ \mathbb{N} \models \Box Gが言えて，$ T \vdash G．よって$ Tは矛盾する．