自然数の無矛盾性は超現順序数を以てしても証明できない？

ヘンキン文とやらを解析してみようか・・・。

Ｈ＝「証明できる命題」
⇔
Ｈ⇔Provable(Ｈ)
⇔
（￢Ｈ∨Provable(Ｈ)）∧（￢Provable(Ｈ)∨Ｈ）
⇔
（￢Ｈ∨Ｈ）∧（￢Provable(Ｈ）∨Provable(Ｈ)）
⇔
Ｔ∧Ｔ
⇔
Ｔ

途中において、Provable(Ｈ)⇒Ｈ
ゆえに、
「Ｈの定義」⇔Ｔ，かつ「Ｈの定義」⇒Ｈ∨￢Provable(Ｈ)、この結果は、￢Provable(Ｈ)∨Ｈ⇔Ｔでなければ不合理である！

定義などより「Ｈは定理を表す」ことがよく知られており、合わせて「定理であるかまたは定理が証明できない、は全称である」ということになる。

まー、これも「不完全性定理と合わせて正しいのかなあ～？」というところだ・・・。


続いて“ゲーデル命題の不合理”とは、

Ｇ＝「証明できない命題」
⇔
Ｇ⇔￢Provable(Ｇ)
⇔
（￢Ｇ∨￢Provable(Ｇ)）∧（Provable(Ｇ)∨Ｇ）
⇔
（￢Ｇ∨Ｇ）∧（Provable(Ｇ)∨￢Provable(Ｇ)）
⇔
Ｔ∧Ｔ
⇔
Ｔ

途中において」、Provable(Ｇ)⇒Ｇ
ゆえに、
「Ｇの定義」⇔Ｔ，かつ「Ｇの定義」⇒Ｇ、この結果は（一見するだけで）「あまりにも不合理」にみえます！

なぜならば、Ｔ⊂Ｇ　を意味するからです！

ところが
数学基礎論などによる成果などを思うにつけ「自然数集合の無矛盾性は自然数全体を内包するより大きな集合を以てしても証明できない」という意味なのでしょうかね？


ぞっとしない、というよりも、なんだか、ぞくっときますね・・・。