まぢで？

第二不完全性定理に必要とされるらしい、第一不完全性定理の内容を、体系T内で形式化する、という内容にまだ触れていないので、わからないことが多いですが、

T├　¬Pr（ゲーデル文に対応する数項）がTで証明可能でない
T├　 ¬Pr（ゲーデル文に対応する数項）がTで証明可能でない　→　Con（T）がTで証明可能でない
よって
T├　Con（T）がTで証明可能でない

ということですか？
あと、
¬Pr（ゲーデル文に対応する数項）がTで証明可能でない、を、どんな形で、論理式の形で表すのかがわからないのですが・