「無矛盾」なのに「無矛盾であることが矛盾」

先日の記事で
「無矛盾」ならば「無矛盾であることが無矛盾」
であることが当たり前であるかのように書きました。
しかしながら
「無矛盾」なのに「無矛盾であることが矛盾」
であるような体系も存在しまぷ。
今日は、そのことについての話ですー。

不完全性定理が適用できるような無矛盾な公理系Tを固定して考えます。
不完全性定理により、Tにおいて、T自身が無矛盾であることを意味していると解釈できる文Con(T)が存在して、Con(T)も¬Con(T)も証明不可能です。
したがって、Tに¬Con(T)を付け加えた体系T+¬Con(T)もまた無矛盾になります。
ここで、任意の命題Aについて
T \vdash Con(T+A) \rightarrow Con(T)
なので、その対偶をとると
T \vdash \neg Con(T) \rightarrow \neg Con(T+A)
となります。
よって、帰納定理により
T+\neg Con(T) \vdash \neg Con(T+A)
が成り立ちます。
ここで、Aとして¬Con(T)をとると
T+\neg Con(T) \vdash \neg Con(T+\neg Con(T))
となります。
見やすいようにT+¬Con(T)をT'とおくと
T' \vdash \neg Con(T')
となるので、T'は無矛盾であるにも関わらず、T'自身の無矛盾性を表していると解釈できる文Con(T')の否定を証明可能で、言い換えるとT'自身が矛盾していることを表していると解釈できる文¬Con(T')を証明可能なのです。
要約すると、T'は無矛盾なのに、自分は矛盾しているという主張を証明可能、ということになります。
自分は矛盾している!と間違ったことを主張している無矛盾な体系。なかなか面白いですね。

さて、T'においてはCon(T')は間違った主張、すなわち
偽です
偽であることが証明可能です
その否定が証明可能です。
偽である命題を仮定するとどんなことでも導けますので、
偽であることが証明可能な命題を仮定するとどんなことでも導けますので
否定を証明可能な命題を仮定するとどんなことでも導けますので、
T' \vdash Con(T') \rightarrow \neg Con(T')…(1)
が成り立ちます。
これを無理やりに解釈すると、T'は
「自分が無矛盾ならば自分が矛盾している」
ということを証明可能な、無矛盾な体系、ということになります。
うーん、ワケワカメ。イミフ!

一応断っておきますと、ここでの各々の解釈は単なる言葉遊びであって、数学的に新しい知見が得られるものではありませんし、数学的に厳密なものでもありません。
つまり、例えば、(1)は正しいにしても、それを言葉によって解釈するところは数学的ではない、ということです。
大体、(1)には意味などないのです。形式化された文であるのみです。
さらに言うと、Con(T)という文にしても、それをT自身の無矛盾性を表していると解釈するのは人間の勝手で、形式化された事柄について意味を考えることには、意味不明な主張ができあがって興味深いということ以外に、意味があるとは私には思えません。