カット除去定理からの無矛盾性証明
Thm
$ \Rightarrow \botは$ \bf LKで証明されない.すなわち$ \bf LKは無矛盾.
proof:
もし証明されるとすると
$ \Rightarrow \botと$ \mathrm{L\bot}規則$ \bot \Rightarrowにカットを当てて空シーケント$ \Rightarrowが証明可能
カット除去定理よりカットなしでも$ \Rightarrowは証明可能. しかしカット以外の規則で空シーケントを結論することは出来ない.
よって破綻する.
一般化
$ \mathrm{L\bot}規則$ \frac{}{\bot, \Gamma \Rightarrow \Delta}のある(一般的な)体系でカット除去定理が成り立つなら,シーケント$ \Rightarrow \botは証明されない. すなわちそのような体系は証明論的に無矛盾.
proof:同上.
memo