■

[記号論理学]Cut-elimination Theorem について　その2

さて、小ネタ第二弾である。小ネタの割に温め過ぎて、えらく時間が経ってしまった。

カット除去定理の証明の記述は複雑だが、結局は証明の書き換えのアルゴリズムなのであって、構成的なところがいいのである（非構成的な証明もたしかあったような）。しかし、本当に書き換えているところを見せているテキストを見たことがないので、実際にやってみる。例としては、たぶん次のが非自明で、一番簡単なものではないかと思う。


\displaystyle\frac{\displaystyle\frac{A\to A\quad\quad B \to B}{A,A \supset B \to B}(\supset left)\quad \displaystyle\frac{B\to B\quad\quad C \to C}{B,B \supset C \to C}(\supset left)}{A,A \supset B, B \supset C \to C}(cut)


cutされているBは論理記号を含んでいないので、この証明図の次数は0であり、証明図の左の階数と右の階数はどちらも2なので、証明図の階数\rhoはその和の4である。まず証明図のすぐ上の右に適用される書き換えルールは、テキストでいうところの 2.123.3 であり、


\displaystyle\frac{\Pi \to \Sigma \quad\quad \displaystyle\frac{\Gamma \to \Theta,A \quad\quad B,\Delta \to \Lambda}{A \supset B,\Gamma,\Delta \to \Theta,\Lambda}(\supset left)}{\Pi,(A \supset B)^*,\Gamma^*,\Delta^* \to \Sigma^*, \Theta,\Lambda}(cut)

を

\displaystyle\frac{\displaystyle\frac{\Pi \to \Sigma \quad\quad \Gamma \to \Theta,A}{\Pi,\Gamma^* \to \Sigma^*,\Theta,A}(cut) \quad\quad \displaystyle\frac{\displaystyle\frac{\Pi \to \Sigma \quad\quad B,\Delta \to \Lambda}{\Pi,B^*,\Delta^* \to \Sigma^*,\Lambda}(cut)}{B,\Pi,\Delta^* \to \Sigma^*,\Lambda}(w left)}{A \supset B,\Pi,\Gamma^*,\Pi,\Delta^* \to \Sigma^*,\Theta,\Sigma^*,\Lambda}(\supset left)


に書き換えろとある。式をぐっと睨むと、


\displaystyle\frac{\displaystyle\frac{A,A \supset B \to B \quad\quad B \to B}{A,A \supset B \to B}(cut) \quad\quad \displaystyle\frac{\displaystyle\frac{A,A \supset B \to B \quad\quad C \to C}{A,A \supset B,C \to C}(cut)}{C,A,A \supset B \to C}(w left)}{B \supset C,A,A \supset B,A,A \supset B \to C}(\supset left)
となるが、増えた上のcutはすぐに解消できて（左上はそのまま証明をもってきて、右上はC\to Cの左辺がcut式Bを含んでいないので、正確にはcutですらない）、整理すると


\displaystyle\frac{\displaystyle\frac{A\to A\quad\quad B \to B}{A,A \supset B \to B}(\supset left)\quad \displaystyle\frac{C\to C}{A,A \supset B,C \to C}(wleft)}{A,A \supset B, B \supset C \to C}(\supset left)

となる。



さて、この続きでカット除去可能な論理と計算との関係をもう少し調べようかと思っていたところ、ほったらかしになってはや半年以上過ぎてしまった。まあ、Wikiに乗ってる以上の事がわかったわけではないが、カット除去可能な論理では証明可能なものは正規形と呼ばれる標準的な証明が手続き的に得られ、逆に証明不可能なものはその途中で手続きが実行できなくなってそれと知れるという性質があるそうな。これは一見すごくよさそうで、すべての論理がうまい公理を導入して証明可能な命題の集合を変えずにカット除去可能になるとしたらすごくいい話に思えるかもしれない。あれ？ちょっと待てよ。不完全性定理はどこへいった？　はい、実はカット除去可能な論理から派生する計算はTuring completeにならない事が知られており、これはまあざっくり言うと、カット除去可能というのは計算が必ず停止するアルゴリズムに対応しており、それは原始帰納的関数の範囲の計算に対応するということになる。帰納的関数をすべて計算するには力が足らないのである。