>>140
Tがω無矛盾というのがいる？

いまPr(g(A))=∃x(Pr'(x
g(A)))をTの公理からの可証性述語とします。たぶん<=が問題になる。対偶を示します。

TでAの証明がない
⇒どの自然数kもT|-Aの証明になりえない
⇒任意のkでPA|-¬Pr'(k
g(A))
⇒任意のkでT|-¬Pr'(k
g(A))
⇒Tがω無矛盾ならばT|-∃x(Pr'(x
g(A)))ではない
⇒T|-Pr(g(A))ではない。