体系SKにおいて定理Bを導く

戸次大介という人の数理論理学という本の第二部第7章のヒルベルト証明論のところの練習問題。

「BCWB'C*がいずれもSKの定理であることを証明せよ」 とりあえずBだけできた。

1. (φ→(ψ→χ))→((φ→ψ)→(φ→χ)) : S
2. (φ→(ψ→χ))→((φ→ψ)→(φ→χ))→((ψ→χ)→((φ→(ψ→χ))→((φ→ψ)→(φ→χ)))) : K
3. (ψ→χ)→((φ→(ψ→χ))→((φ→ψ)→(φ→χ))) : 1, 2, MP
4. ((ψ→χ)→((φ→(ψ→χ))→((φ→ψ)→(φ→χ))))→(((ψ→χ)→(φ→(ψ→χ)))→((ψ→χ)→(φ→ψ)→(φ→χ))) : S
5. ((ψ→χ)→(φ→(ψ→χ)))→((ψ→χ)→(φ→ψ)→(φ→χ)) : 3, 4, MP
6. (ψ→χ)→(φ→(ψ→χ)) : K
7. (ψ→χ)→(φ→ψ)→(φ→χ) : 5, 6, MP

この本は練習問題の回答が載ってないからつらい。 結局、WikipediaのC,B,W,Kシステムのページ見て、 SKIコンビネータとの関係を類推しながらやった。

定理Iの証明を読んでみて、関数適応とMP規則の適用が対応するに違いない！…とか思ってたら、普通にWikipediaに書いてあった…

規則MPが、

P,P→Q⇒Q

だから、引数がPに、関数がP→Qに、値がQに対応するんだろうな。