ゲーデル命題の否定をゲーデルの如く定式化すること自体が数学の無矛盾性と同値

Ｇ⇔￢Plovable(Ｇ)
⇔
（￢Ｇ∨￢Plovable(Ｇ)）∧（Plovable(Ｇ)∨Ｇ）
⇔
Ｇ∧￢Plobable(Ｇ)
⇔
「ＧでありＧは証明できない」

あー、ノーマルな計算もあったんだ、それにしてもなんという多義性！

ここで、Ｇ⇔「Ｇの定義」を確認しておきたい・・。

￢Ｇ⇔Plovable(Ｇ)
⇔
（Ｇ∨Plovable(Ｇ)）∧（￢Plovable(Ｇ)∨￢Ｇ）
⇔
Ｇ

昔やった「￢Ｇをこう定義すること自体がＧ」が出てきた。ソフティケートすると

Ｇ⇔「￢Ｇの定義」

ゲーデルの論証を信用するならば標題のようなことになるが、ひょっとしたら「￢Ｇの定義は証明できない」なのかもシレマセン・・・。

さらに、

「￢Ｇをゲーデルの如く定義すること自体は全称であり否定されない」
かつ
「￢Ｇをゲーデルの如く定義したならばＧ」

後者が（じつは）同値だったのだから、
「￢Ｇをゲーデルの如く定義すること自体がＧ」

合わせて（さらにゲーデルの論証を信じたならば）

「Ｇそのものが全称であり否定されない」⇔「数学は無矛盾である」

ここでは定義はゲーデルの物しか使っておりません、し、計算の二重性はＧ⇔Ｔによって合理化されます。

「数学の無矛盾性は数学の意味において積極的に証明されないが否定されないがゆえに真である」

Ｇ⇔数学の無矛盾性、だったならば・・、ね？


これだけの結論を引き出すために止むを得なかったとはいえ、途中の混乱をお詫び申し上げます！