M ≡α M', M →1β N ならば M' →1β N
二つの命題が相互依存になって、二つの証明の帰納法を同時に実行することで解消するという大掛かりな方法になってしまった。
既知とする命題
- 既知の命題1: λx.Q ≡α λy.Q' ⇔ Q' ≡α [y/x]Q かつ [x≡y または y ∉ FV(Q)]
- 既知の命題2: R' ≡α R, λy.Q' ≡α λx.Q ⇒ [R'/y]Q' ≡α [R/x]Q
この二つは補助定理1.2.36により証明できる。
- 既知の命題3: M →1 Nに長さn+1の証明図がある ⇔ Nとα同値なN'が存在しM ▷1 N'に長さnの証明図がある
- 既知の命題4: M →1 Nに長さnの証明図がありN' ≡α N ⇒ M →1 N'に長さnの証明図がある
この二つは明らか。
- 既知の命題5: M ▷1β N ⇒ FV(N) ⊂ FV(M)
M ▷1 Nに至る証明図の長さに関する帰納法で証明できる。
- 既知の命題6: N' ≡ [t/s]N ⇒ [t/s][N/x]M ≡α [t/s][N'/x]M
補助定理1.2.36(2)と定理1.2.37を使ってMの長さに関する帰納法で証明できる。
- 既知の命題7: x ≢ y, y ∉ FV(Q), x ∉ FV(R) ⇒ [Q/x][R/y]M ≡α [R/y][Q/x]M
補助定理1.2.36(2)と定理1.2.37を使ってMの長さに関する帰納法で証明できる。
PredA(n), PredA'(n), PredB(n)
以下のように述語PredA(n), PredA'(n), PredB(n)を定める。
PredA(n) ⇔ M ▷1 N に長さがnの証明図があり、M ≡α M'であるような任意の項M,N,M'に対してM' →1 Nに長さがn+1の証明図がある
PredA'(n) ⇔ M →1 N に長さがnの証明図があり、M ≡α M'であるような任意の項M,N,M'に対してM' →1 Nに長さがnの証明図がある
PredB(n) ⇔ M ▷1 Nに長さがnの証明図があるような任意の項M,Nと変数s,tに対して[t/s]M →1 [t/s]Nに長さがn+1の証明図がある。
このときPredA(n) ⇔ PredA'(n+1)であることはすぐわかる。
以下で次の命題を証明する。
- PredA(1)
- PredA(n-1), PredB(n-1) ⇒ PredA(n) (n = 2,3,...)
- PredB(1)
- PredA(n), PredB(n-1) ⇒ PredB(n) (n = 2,3,...)
これらが成立するとすれば、任意のnについてPredA(n)とPredB(n)が成立することになる。よって任意のnについてPredA'(n)が成立し、目的の命題
が従う。
PredA(1)の証明
M ▷1 Nに長さが1の証明図があり、M ≡α M'であるような任意の項M,N,M'をとる。このときM' →1 Nに長さが2の証明図があることを示せばよい。
M ▷1 Nは公理となるから、
と表せる。
M ≡α M'から
と表せる。
ここでN' ≡ [R'/y]Q'とおく。すると既知の命題2より
となる。
公理型ρより
であり、さらにN' ≡α Nから推論規則κ1より
となる。これを示す証明図の長さは2で得ることができる。
□
PredA(n-1), PredB(n-1) ⇒ PredA(n) (n = 2,3,...)の証明
n ≧ 2を任意にとり、PredA(n-1), PredB(n-1)を仮定する。
M ▷1 Nに長さがnの証明図があり、M ≡α M'であるような任意の項M,N,M'をとる。このときM' →1 Nに長さがn+1の証明図があることを示せばよい。
M ▷1 Nの証明図の最後の推論によって場合分けする。
最後の推論がμのとき
証明図は次の形をしている。
ただしM ≡ PQ, N ≡ PR。
M ≡α M'から
証明図から
次にPredA(n-1)より
よって既知の命題3より、Rとα同値なR'があり、
を満たす。推論規則μにより
さらにP'R' ≡α Nから推論規則κ1により
すなわち
である。これを示す証明図はn+1で得ることができる。
最後の推論がνのとき
最後の推論がμのときと同様。
最後の推論がξのとき
証明図は次の形をしている。
ただしM = λx.Q, N = λx.R
M ≡α M'からM' ≡ λy.Q'と表せ、既知の命題1より
となる。
証明図から
次にPredB(n-1)より
よってPredA'(n) (⇔ PredA(n-1))より
よって既知の命題3より[y/x]Rとα同値なR'があり
を満たす。
x ≢ yを仮定するとy ∉ FV(Q)であり、これとQ ▷1β Rから既知の命題5によりy ∉ FV(R)となる。すなわち
が成立する。
だから既知の命題1よりλy.R' ≡α λx.Rが成立する。
Q' ▷1β R'から推論規則ξより
これとλy.R' ≡α λx.Rから推論規則κ1より
すなわち
である。これを示す証明図はn+1で得ることができる。
□
PredB(1)の証明
M ▷1 Nに長さが1の証明図があるような項M,Nと変数s,tを任意にとる。このとき[t/s]M →1 [t/s]Nに長さが2の証明図があることを示せばよい。
M ▷1 Nは公理だからM ≡ (λx.Q)R, N ≡ [R/x]Qと表せる。
変数z ∉ V(λstx.Q)をとる。
Q' ≡ [t/s][z/x]Q, R' ≡ [t/s]R とおく。
定理1.2.37より[t/s]M ≡α (λz.Q')R'である。
[R'/z]Q' ≡ [R'/z][t/s][z/x]Q ≡α [t/s][R'/z][z/x]Q …既知の命題7より ≡α [t/s][R'/x]Q …補助定理1.2.36の(1)と(2)より ≡α [t/s][R/x]Q …既知の命題6より ≡ [t/s]N |
公理型ρより
である。これと[t/s]M ≡α (λz.Q')R'からPredA(1)により
である。これと[R'/z]Q' ≡α [t/s]Nから既知の命題4より
である。これを示す証明図の長さは2で得ることができる。
PredA(n), PredB(n-1) ⇒ PredB(n) (n = 2,3,...)の証明
n ≧ 2を任意にとり、PredA(n), PredB(n-1)を仮定する。
M ▷1 Nに長さがnの証明図があるような任意の項M,Nと変数s,tをとる。このとき[t/s]M →1 [t/s]Nに長さがn+1の証明図があることを示せばよい。
M ▷1 Nの証明図の最後の推論によって場合分けする。
最後の推論がμのとき
証明図は次の形をしている。
ただしM ≡ PQ, N ≡ PR
証明図から
次にPredB(n-1)より
である。よって[t/s]Rとα同値なR'があり、
を満たす。ここで推論規則μより
さらに推論規則κ1より
すなわち
である。これを示す証明図の長さはn+1で得ることができる。
最後の推論がνのとき
最後の推論がμのときと同様。
最後の推論がξのとき
証明図は次の形をしている。
ただしM ≡ λx.Q, N ≡ λx.R
変数z ∉ V(λts.MN)をとる。
このとき定理1.2.37より
である。
証明図から
次にPredB(n-1)より
既知の命題3より[z/x]Rとα同値なR'があり、
を満たす。再びPredB(n-1)より
既知の命題3より[t/s]R'とα同値なR''があり
を満たす。推論規則ξより
補助定理1.2.36(2)よりR'' ≡α [t/s]R' ≡α [t/s][z/x]R、よってλz.R'' ≡α λz.[t/s][z/x]R ≡α [t/s]λx.Rだから推論規則κ1より
PredA'(n+1) (⇔ PredA(n))により
である。これを示す証明図の長さはn+1で得ることができる。
□
雑感
こんな残念な証明を記事に書き起こすのにずいぶん時間がかかってしまって、とても時間の無駄をした気分ですorz
