αに至る正規な証明図ではαの部分論理式しか現れない

現代数理論理学序説 p.45

自然推論NJでは、論理記号'⊥'を含まない論理式αに至る正規な証明図に現れる論理式はαの部分論理式だけである

これの証明のチャレンジしてみました。

正規な推論図であることの別定義

推論図が正規形であることは、以下で定義される集合Nに属することと同値になる。

推論図の集合N, N_0を次のように帰納的に定める

• 長さ1の推論図ΠについてΠ∈N_0
• Π_1∈N_0, Π_2∈Nのとき∈N_0 (推論規則⊃-Eで得られる推論図)
• Π_1∈N_0のとき∈N_0 (推論規則⊥-Eで得られる推論図)
• Π∈N_0のときΠ∈N
• Π_1∈Nのとき∈N (推論規則⊃-Iで得られる推論図)
• 以上からN, N_0に属するとわかる推論図のみが、N, N_0に属する

命題1

Π∈N_0でΠでは(⊥-E)が使われていないとすると、Πには落ちていない仮定の部分論理式しか現れない。
Π∈NでΠでは(⊥-E)が使われていないとすると、Πには落ちていない仮定かΠの結論の部分論理式しか現れない。

証明:

N_0とNの定義に関する帰納法で同時に示す。

Π∈N_0について、Πが長さ1のとき: 明らか。
Π∈N_0について、Π = のとき:

帰納法の仮定から、Π_1にはΠ_1の落ちていない仮定の部分論理式しか現れないし、Π_2にはΠ_2の落ちていない仮定かαの部分論理式しか現れない。
よってα⊃βはΠ_1の落ちていない仮定の部分論理式だから、αの部分論理式はΠ_1の落ちていない仮定の部分論理式。
同じくβもΠ_1の落ちていない仮定の部分論理式だから、ΠにはΠの落ちていない仮定の部分論理式しか現れない。

Π∈Nについて、Π∈N_0のとき: 明らか。
Π∈NについてΠ = のとき:

帰納法の仮定からΠ_1にはΠ_1の落ちていない仮定かβの部分論理式しか現れない。
Π_1の落ちていない仮定とはΠの落ちていない仮定とαのことで、またαかβの部分論理式はα⊃βの部分論理式であることに注意するとΠにはΠの落ちていない仮定かα⊃βの部分論理式しか現れない。

□

命題2

Π∈N_0でΠでは(⊥-E)が使われているとすると、Πの落ちていない仮定に⊥が含まれる。
Π∈NでΠでは(⊥-E)が使われているとすると、Πの落ちていない仮定かΠの結論に⊥が含まれる。

証明:

N_0とNの定義に関する帰納法で同時に示す。

Π∈N_0について、Π = のとき:

Π_1で(⊥-E)が使われている場合は、Π_1に帰納法の仮定を用いることで明らか。
Π_1で(⊥-E)が使われていない場合を考える。
命題1により、Π_1の落ちていない仮定に⊥が現れる。よって成り立つ。

Π∈N_0について、Π = のとき:

Π_1で(⊥-E)が使われている場合は、Π_1に帰納法の仮定を用いることで明らか。
Π_1で(⊥-E)が使われていない場合を考える。このときΠ_2で(⊥-E)が使われている。
帰納法の仮定からΠ_2の落ちていない仮定かαに⊥が含まれる。
Π_1に命題1を使うと、α⊃βはΠ_1の落ちていない仮定の部分論理式になる。
αに⊥が含まれていることとから、Π_1の落ちていない仮定には⊥が含まれる。

Π∈Nについて、Π∈N_0のとき: 明らか。
Π∈NについてΠ = のとき:

帰納法の仮定からΠ_1の落ちていない仮定かβに⊥が含まれる。
Π_1の落ちていない仮定とはΠの落ちていない仮定とαのことであるから、結局Πの落ちていない仮定かαかβに⊥が含まれる。
すなわちΠの落ちていない仮定かα⊃βに⊥が含まれる。

□

系

αに⊥が含まれないとき、αに至る正規な証明図にはαの部分論理式しか現れない

証明:
Πをαに至る正規な証明図とする。Π∈NでありΠはすべての仮定が落ちている。
ここで命題2の対偶から、Πには(⊥-E)が使われていない。よって命題1よりΠにはαの部分論理式しか現れない。

□