ゲーデルの第一不完全性定理

すべての論理式と、証明候補となる論理式の有限列に、それぞれ一意な自然数(ゲーデル数)を割り当てる。「数 $y$ が、数 $x$ が表す論理式の証明を符号化している」という関係を決定可能な算術関係 $\mathrm{Prf}(y,x)$ として表現する。対角線論法を用いて、命題 $G$ を構成する。これを展開すると $\neg\exists y\, \mathrm{Prf}(y,\ulcorner G\urcorner)$(すなわち $G$ の証明を符号化する数は存在しないという主張)になる。$F\vdash G$ の場合と $F\vdash\neg G$ の場合をそれぞれ検討すると、前者は無矛盾性と矛盾し、後者は $\omega$-無矛盾性(ロッサーの改良により通常の無矛盾性に弱められる)と矛盾するため、$F$ はどちらも証明できないが、$G$ 自体は真である。