「自然数論を含む帰納的に記述できる公理系が、無矛盾であれば、自身の無矛盾性を証明できない」
ゲーデルの不完全性定理はこのようなものであると言われています。
無矛盾とは、ある命題Ａについて、
「Ａが証明された ＆ 非Ａが証明された」ということがない、ということです。
なぜなら「Ａが証明された ＆ 非Ａが証明された」は、
両立しない事柄が同時に証明されているので矛盾だからです。
ゲーデルの不完全性定理の結論については、なるほどなあと分かります。
これは例えて言うならば、二次元に住む住人が、世界全体の模様を知ることができないということと同じことです。
世界全体の模様を知るためには三次元へと飛び出る必要があります。
地球が丸いことや地球が青いことは、宇宙に出て外から地球を眺めてはじめて分かることなのです。
ところで、カットの法則というものがあるようです。要するに、
Ａ → Ｂ、Ｂ → Ｃ なら Ａ → Ｃ
ということです（Ａ → Ｂ → Ｃ から、Ｂをカットできるということらしい）。
これの応用で、カット除去定理というものがあり、これは、
Ａ → Ｃ から Ａ → Ｂ → Ｃ を復元するものです。
そして、カット除去定理を用いて、
？ → 矛盾する証明
という式を復元することで、
「どこまで復元しても、体系内で矛盾する証明は証明できない」ゆえに
「体系は矛盾していない」という結論を導き、
これをもって無矛盾性の証明がなされたといわれることがあるらしいのですが…
これはどうなのでしょうか。
「体系内で矛盾する証明は証明できない」という前提の部分で、
「体系は矛盾していない」という結論を先取りしているような…
もしそうなら、証明としては失敗しているということになります。
（推論としては成り立つのでしょう。）
ゲーデルが証明したかったのは、
「体系内では体系の無矛盾性を証明できない」ということだと考えられます。
つまり、体系を飛び出して別次元へ行けば証明は可能になるかもしれないという、次元の話です。
しかし、ゲーデルの証明を理解することは難しい…
難しい原因として、おそらく証明が間違っているのではないかと推測されます。
ゲーデルが示したかった結論それ自体は、なるほどなあと分かることなのですが、
証明の手法には混乱があるのでは…
理屈で言えば、「体系内では体系の無矛盾性を証明できない」こともまた、体系内では証明ができないはずなのです。
正確には、
「体系内では、『体系内で体系の無矛盾性を証明できるか証明できないか』のいずれについても証明ができない」
ということになると思います。ややこしいなあ。