カット除去定理の応用
$ \$は論理記号$ \lnot,\land,\lor,\to,\forall,\existsのいずれかを表すとする.
$ \$が現れないシークエント$ \Gamma \Rightarrow \Deltaは,$ \$右/左規則とカット規則無しで証明できる. proof:
次が言える.
1. シーケントに$ \$が増えるのは$ \$右/左規則のどちらかを使ったときに限る.
2. 既にあるシーケントから$ \$を消すには,カット規則を使わざるをえない. 3. 前提より,任意のシーケントはカット規則無しでも証明できる.
よって、結論のシーケントに$ \$が入っていないなら,$ \$右/左規則の両方を1度も使っていないことが示される.
remark:
$ \Rightarrow \botは$ \bf LKで証明されない.すなわち$ \bf LKは無矛盾.