あたりまえのことみたいですね。

＞T├　Con（T）で 　　　　　　　　　　　　　　　　　　　　　　　　　・・・①
＞T├　Con（T）→￢Pr（ゲーデル文に対応する数項）　　　　・・・②
＞だったら T├　￢Pr（ゲーデル文に対応する数項） 　　　　・・・③

MP？

②の対偶（？）
￢Pr（ゲーデル文に対応する数項）がTで証明可能でない　→　Con（T）がTで証明可能でない
と
第一不完全性定理から、￢Pr（ゲーデル文に対応する数項）がTで証明可能でない
から
Con（T）がTで証明可能でない
が出てくる、ということですか？