自分自身の無矛盾性が証明できる強い自然数の理論体系
https://yoriyukiy.com/2018/10/17/%E8%87%AA%E5%88%86%E8%87%AA%E8%BA%AB%E3%81%AE%E7%84%A1%E7%9F%9B%E7%9B%BE%E6%80%A7%E3%81%8C%E8%A8%BC%E6%98%8E%E3%81%A7%E3%81%8D%E3%82%8B%E5%BC%B7%E3%81%84%E8%87%AA%E7%84%B6%E6%95%B0%E3%81%AE%E7%90%86/
Löbの条件の二つ目 T ⊢ Prov(⌜φ→ψ⌝)∧Prov(⌜φ⌝)→Prov(⌜ψ⌝) 、もしカットありの二階算術で成り立つなら、カット除去すればカットなしの二階算術でも成り立つのではと思ってしまって、ちょっと混乱。
⊢ だけでなく Prov もカットを許容するかで二種類あるんだな。
これらを ⊢_{cut}, Prov_{cut} と ⊢_{cut-free}, Prov_{cut-free} と書き分けることにして、
T ⊢_{cut} Prov_{cut}(⌜φ→ψ⌝)∧Prov_{cut}(⌜φ⌝) → Prov_{cut}(⌜ψ⌝) … (1)
は成り立つのだろうし、
T ⊢_{cut} Prov_{cut-free}(⌜χ⌝) → Prov_{cut}(⌜χ⌝) … (2)
は自明だ。ここで更に
T ⊢_{cut} Prov_{cut}(⌜χ⌝) → Prov_{cut-free}(⌜χ⌝) … (3)
も成り立つのであれば、これらから
T ⊢_{cut} Prov_{cut-free}(⌜φ→ψ⌝)∧Prov_{cut-free}(⌜φ⌝) → Prov_{cut-free}(⌜ψ⌝) … (4)
が導けて、これにカット除去を適用して、
T ⊢_{cut-free} Prov_{cut-free}(⌜φ→ψ⌝)∧Prov_{cut-free}(⌜φ⌝) → Prov_{cut-free}(⌜ψ⌝) … (5)
が言えてしまう。
これが言えないという話だから、何が間違っているのかと考えてみると、怪しいのは (3) で、もしそうだとすると「竹内予想は(カットあり)二階算術の内部では証明できない」ということなのだろうか(適当)。
#ns
自分自身の無矛盾性が証明できる強い自然数の理論体系
