証明のできる・できない

様相論理の世界で「可能的に可能的であることが必然的に必然的ならば・・・」とかいう命題に意味があるか、とかいう話があるけどそれに似た疑問。

ある命題Xについて
「Xが証明できない、ということを証明できる」
この形は良く見る。ではもっと入れ子式の証明、例えば
「Xが証明できない、ということが証明できない、ということが証明できない、ということが証明できる」
とかはどうだろうか。こういう形はあまり見ない。
こういう命題に意味があるだろうか？そして実際の数学でこうした構造が出てくることがあるだろうか？

ちょっと記号を導入してみる。
命題Xを証明できる（という事実？を）ことを
　☆X
と書く。
命題Xは証明できないという（論理的帰結？）を
　★X
と書く。
この時、ゲーデルの不完全性定理だと、ある特殊な命題について
☆★G
という形をもつことになる（適当に言ってるので嘘かもしれない）。

これのもっと入れ子なバージョンは意味があるだろうか？
☆★★★★★★★★★★X

ゴールドバッハの予想がこれで解けたりしないだろうか？

(追記)
結構適当な思いつきのようなエントリーではあるけど、実のところこの話はある程度僕が興味を持つ話とつながってる。
僕は、人間は全てを知る事は出来ない、と思っているのだけど（これは概ね常識的な立場だと思う）、
しかし同時に
何をどの程度知る事ができないか、についての、数学的または物理学的理論を欲しいと思っている（そしてそれは手に入るだろう、と妄想している）
しかし単純に、何かを知りえない、と示すのは、おそらくとても難しいと思う。
だがひょっとすると、「何を知りえないかを知りえない」ということを示すのは、もう少し簡単に出来るんじゃないか、などと思ったりする。
というわけでこういう話が気になる。

関連リンク

論理指標 - 生物を数理的に考える 2008年10月9日
こちらのブログでは、ある種の入れ子構造におけるその入れ子の数を「論理指標」と読んでいる。この言葉で言うなら、高階の論理指標の領域に、何か面白い話はないか、というのがこのエントリーの内容、ということになる。