意味論を経由せずに無矛盾性を証明できるか？
証明体系の無矛盾性，すなわち体系$ \mathcal{S}で$ \mathcal{S} \nvdash \bot（ここでは爆発律はあるものとする）について
シークエント計算ではシンタクティカルなカット除去定理が存在するなら体系内で完結して示すことが出来る もし$ \Rightarrow \botなら，始式$ \bot \Rightarrowとのカットで$ \Rightarrowが出てくる．これはカットなしで証明できるとのことだが，どう考えてもおかしい（そんなルールは無いので）
私は知らないし多分出来ないと思うのだが…
という2つの体系についてのことを考えると，なぜ片方は出来て，片方は出来ないのか：ということを考えると，これが結局シークエント計算は何らかの形で論理式の記号に意味を与えているのではないか，という発想の根源だと勝手に思っているのだが，違うのだろうか．