>>418 T を PA を含む帰納的な理論、Prov(y,x) を T の標準的な可証性述語、 P が T の証明図、A が T の論理式のとき、g(P), g(A) をそれぞれ P, A のゲーデル数を表す数字とする。 このとき、ゲーデルの第一不完全性定理は次の表現可能性と対角化補題 から導くことができる。
P が論理式 A の T での証明図 ⇔ Prov(g(P),g(A)) が T で証明可能.
一方、Prov'(y,x) ≡ Prov(y,x)∧¬∃z＜y Dispr(z,x) とおくと、 T が無矛盾という仮定の下で、次が成立する。 ロッサーの不完全性定理は、これよりゲーデルの第一不完全性定理と 同様の方法で証明できる。
P が論理式 A の T での証明図 ⇔ Prov'(g(P),g(A)) が T で証明可能
ところが、Prov*(y,x) ≡ Prov(y,x)∧¬∃z Dispr(z,x) とおくと、 T が無矛盾という仮定があったとしても、 「P が論理式 A の T での証明図」と「Prov*(g(P),g(A)) が T で証明可能」 との同等性が証明できない。
