忍者ブログ
証明論 (2) で言及したカット除去定理を証明する。

まず、「ミックス」と呼ばれる新たな証明ルールを導入する。
\[\cfrac{\Gamma \rightarrow \Theta \qquad \Delta \rightarrow \Lambda}{\Gamma, \Delta^* \rightarrow \Theta^*, \Lambda}\] ここで $\Theta^*, \Delta^*$ はそれぞれ、$\Theta, \Delta$ から論理式 $\mathfrak{M}$ を除いたものとする(ここで $\mathfrak{M}$ は「ミックス式」と呼ばれる)。ミックスとカットは、交換・縮約・薄めを何回か適用することにより、たがいに変換可能である。

演習:ミックスとカットがたがいに変換可能であることを確かめよ。

つぎに、証明の複雑さを測るふたつの尺度である次数 $dg$ および階数 $rk$ を導入する。$dg$ とはミックス式の論理演算子の個数を表し、$rk$ はミックスが適用された式から数えて最後にミックス式が現れるシーケントの個数である。ここで $rk_l, rk_r$ をそれぞれミックスが適用された式より左側/右側の階数とし、$rk=rk_l+rk_r$ とする。ミックスが現れる証明においてはミックスが適用された式の直前にかならずミックス式が現れるので $rk > 1$ となる。ミックスが用いられる証明を $\Pi$ とするとその証明の次数および階数はそれぞれ $gd(\Pi), rk(\Pi)$ で表される。また、ミックス式に同じ論理演算子が複数回現れる場合、それぞれをひとつとして数える。

例:つぎの証明の次数は 1 であり階数は 3 である。
\[
\cfrac{\cfrac{\mathfrak{F}(\mathfrak{a}) \rightarrow \mathfrak{F}(\mathfrak{a})}{\mathfrak{F}(\mathfrak{a}) \rightarrow \exists \mathfrak{x} \mathfrak{F}(\mathfrak{x})} \qquad \cfrac{\exists \mathfrak{x} \mathfrak{F}(\mathfrak{x}) \rightarrow \exists \mathfrak{x} \mathfrak{F}(\mathfrak{x})}{\neg \exists \mathfrak{x} \mathfrak{F}(\mathfrak{x}), \exists \mathfrak{x} \mathfrak{F}(\mathfrak{x}) \rightarrow}}{\mathfrak{F}(\mathfrak{a}), \neg \exists \mathfrak{x} \mathfrak{F}(\mathfrak{x}) \rightarrow}
\] 上で述べたとおり、カットとミックスはたがいに変換可能なので、カット除去定理を証明するには任意の証明からミックスが取り除けることを示せばよい。そのような方針のもと、次数と階数にかんする二重帰納法でカット除去定理を証明する。

Case 1: $rk=2$ の場合
Case 1.1.1: ミックス式が始式として、つまり $\mathfrak{M} \rightarrow \mathfrak{M}$ のかたちでミックスが適用される左の式に現れる場合
この場合、ミックスは以下のかたちとなる。
\[
\cfrac{\mathfrak{M} \rightarrow \mathfrak{M} \qquad \Delta \rightarrow \Lambda}{\mathfrak{M}, \Delta^* \rightarrow \Lambda}
\] これは、以下のようにミックスを用いず証明可能である。
\[
\cfrac{\cfrac{\Delta \rightarrow \Lambda}{\vdots}}{\mathfrak{M}, \Delta^* \rightarrow \Lambda}
\] ここで $\vdots$ によって省略された箇所は、何回かの交換によってミックス式 $\mathfrak{M}$ を $\Delta$ の外に掃き出し、縮約で複数のミックス式をひとつにまとめている。
Case: 1.1.2 ミックス式が始式として、つまり $\mathfrak{M} \rightarrow \mathfrak{M}$ のかたちでミックスが適用される右の式に現れる場合
Case 1.1 の場合と同様に証明する。

Case 1.2: ミックス式が $\mathfrak{A} \& \mathfrak{B}$ というかたちの場合
この場合、ミックスは以下のかたちとなる。
\[
\cfrac{\cfrac{\Gamma \rightarrow \Theta, \mathfrak{A} \qquad \Gamma \rightarrow \Theta, \mathfrak{B}}{\Gamma \rightarrow \Theta, \mathfrak{A} \& \mathfrak{B}} \qquad \cfrac{\mathfrak{A}, \Delta \rightarrow \Lambda}{\mathfrak{A} \& \mathfrak{B}, \Delta \rightarrow \Lambda}}{\Gamma, \Delta \rightarrow \Theta, \Lambda}
\] 帰納法の仮定により、以下はミックスなしで証明可能である。
\[
\cfrac{\Gamma \rightarrow \Theta, \mathfrak{A} \qquad \mathfrak{A}, \Delta \rightarrow \Lambda}{\Gamma, \Delta^* \rightarrow \Theta^*, \Lambda}
\] こうして得られた $\Gamma, \Delta^* \rightarrow \Theta^*, \Lambda$ に薄めと交換を何回か適用すると目的の式である $\Gamma, \Delta \rightarrow \Theta, \Lambda$ が得られる。

Case 1.3: ミックス式が $\mathfrak{A} \vee \mathfrak{B}$ というかたちの場合
Case 1.2 の場合と同様に証明する。

Case 1.4: ミックス式が $\forall \mathfrak{x} \mathfrak{F}(\mathfrak{x})$ というかたちの場合
この場合、ミックスは以下のかたちとなる。
\[
\cfrac{\cfrac{\Gamma \rightarrow \Theta, \mathfrak{F}(\mathfrak{a})}{\Gamma \rightarrow \Theta, \forall \mathfrak{x} \mathfrak{F}(\mathfrak{x})} \qquad \cfrac{\mathfrak{F}(\mathfrak{b}), \Delta \rightarrow \Lambda}{\forall \mathfrak{x} \mathfrak{F}(\mathfrak{x}), \Delta \rightarrow \Lambda}}{\Gamma, \Delta \rightarrow \Theta, \Lambda}
\] ここで、「$\Gamma \rightarrow \Theta, \mathfrak{F}(\mathfrak{a})$ が証明可能であるなら $\Gamma \rightarrow \Theta, \mathfrak{F}(\mathfrak{b})$ も証明可能である」という補題を用いる。すると、帰納法の仮定により、以下がミックスなしで証明可能である。
\[
\cfrac{\Gamma \rightarrow \Theta, \mathfrak{F}(\mathfrak{b}) \qquad \mathfrak{F}(\mathfrak{b}), \Delta \rightarrow \Lambda}{\Gamma, \Delta^* \rightarrow \Theta^*, \Lambda}
\] こうして得られた $\Gamma, \Delta^* \rightarrow \Theta^*, \Lambda$ に、Case 1.2 の場合と同様に薄めと交換を何回か適用して目的の式である $\Gamma, \Delta \rightarrow \Theta, \Lambda$ を得る。

演習:上で用いた補題を証明せよ。

Case 1.5: ミックス式が $\exists \mathfrak{x} \mathfrak{F}(\mathfrak{x})$ というかたちの場合
Case 1.4 の場合と同様に証明する。

演習:ミックス式が $\mathfrak{A} \supset \mathfrak{B}$ というかたちを持つ場合と $\neg \mathfrak{A}$ というかたちを持つ場合のそれぞれ証明せよ。

次回は $rk(\Pi)>2$ の場合を証明する。
PR
この記事にコメントする
お名前
メールアドレス
URL
コメント
カレンダー
10 2017/11 12
S M T W T F S
1 3 4
5 6 7 8 9 10 11
12 13 14 15 16 17 18
19 20 21 22 23 24 25
26 27 28 29 30
最新コメント
最新トラックバック
メール
ブログ作成者(はやし)に直接訴えたいことがある、という場合は、下のアドレスにメールをどうぞ。

thayashi#ucalgary.ca
(#を@に置換してください)

ブログ内検索
Google
WWW を検索 このブログ内を検索

はやしのブログ内で紹介された
 書籍の検索はこちら
 音盤の検索はこちら
ランダムおすすめ
(忍者ブログに引越してから、うまくうごかなくなってしまいました。いつか、直します)
Randombook
このブログで紹介したことのある本をランダム表示。
Randomusic
このブログで紹介したことのある音をランダム表示。
自分がらみのリンク
はやしのブログ書籍一覧
このブログで言及された書籍の一覧。
はやしのブログ音盤一覧
このブログで言及された音盤の一覧。
最近のおすすめ本
最近のおすすめ音

Copyright © [ はやしのブログ ]
No right reserved except those which belong to someone else.
Special Template : 忍者ブログ de テンプレート and ブログアクセスアップ
Special Thanks : 忍者ブログ
Commercial message : [PR]