レーブの定理 - 人生の役に立たない数学

「スマリヤンの決定不能の論理パズル（白揚社 2008年）」という本にレーブの定理がわかりやすく紹介されていたので、それを紹介したいと思います。
レーブの定理
任意の命題 $k,C$ について、もし4型の推論者が $BC\supset C$ と $k\equiv (Bk\supset C)$ を信じるならば、 $C$ を信じる。
ここで、 $Bk$ というのは、「命題 $k$ を信じている」という意味で、4型の推論者とは以下の推論規則に従う人です。
$(A1a)(p\equiv 1)\supset Bp$
$(A1b)Bp\wedge B(p\supset q)\supset Bq$
$(A2)B(Bp\wedge B(p\supset q)\supset Bq)$
$(A3)Bp\supset BBp$
$(A4)B(Bp\supset BBp)$
証明する前に補題を２つほど示します。
補題１
$B(p\supset(q\supset r))\supset B(Bp\supset(Bq\supset Br))$
証明　 $(1)B(B(p\supset q)\supset (Bp\supset Bq) )$ 　∵(A2)と同値

　　　 $(2)BB(p\supset q)\supset B(Bp\supset Bq)$ 　∵(1),(A1b)より

　　　 $(3)BB(p\supset (q\supset r) )\supset B(Bp\supset B(q\supset r) )$

　　　　　　∵(2)の $q$ を $q\supset r$ に置き換え

　　　 $(4)B( (B(q\supset r)\supset (Bq\supset Br) )$

　　　　　 $\supset ( (Bp\supset B(q\supset r) )\supset (Bp\supset (Bq\supset Br) ) ) )$

　　　　　　∵ $(Y\supset Z)\supset( (X\supset Y)\supset(X\supset Z) )$ の $X$ を $Bp$ , $Y$ を $B(q\supset r)$ ,

　　　　　　　 $Z$ を $(Bq\supset Br)$ に置き換え

　　　 $(5)B( (Bp\supset B(q\supset r) )\supset (Bp\supset (Bq\supset Br) ) )$ 　∵(1),(4),(A1b)より

　　　 $(6)B(Bp\supset B(q\supset r) )\supset B(Bp\supset (Bq\supset Br) )$ 　∵(5),(A1b)より

　　　 $(7)BB(p\supset (q\supset r))\supset B(Bp\supset (Bq\supset Br) )$ 　∵(3),(6)より

　　　 $(8)B(p\supset(q\supset r))\supset BB(p\supset(q\supset r))$ 　∵(A3)より

　　　　∴ $B(p\supset(q\supset r))\supset B(Bp\supset(Bq\supset Br))$ 　∵(7),(8)より

補題２（本では、補題１）
$B(p\supset (Bp\supset q) )\supset B(Bp\supset Bq)$
証明　 $(1)B(p\supset (Bp\supset q) )\supset B(Bp\supset (BBp\supset Bq) )$ 　∵補題１より

　　　 $(2)B(Bp\supset BBp)$ 　∵(4)より

　　　 $(3)B( (Bp\supset BBp)\supset ( (Bp\supset (BBp\supset Bq) )\supset (Bp\supset Bq) ) )$

　　　　　　∵ $(X\supset Y)\supset ( (X\supset (Y\supset Z) )\supset (X\supset Z) )$ の $X$ を $Bp$ , $Y$ を $BBp$ ,

　　　　　　　 $Z$ を $Bq$ に置き換え

　　　 $(4)B( (Bp\supset (BBp\supset Bq) )\supset (Bp\supset Bq) )$ 　∵(2),(3),(A1b)より

　　　　∴ $B(p\supset (Bp\supset q) )\supset B(Bp\supset Bq)$ ∵(1),(4),(A1b)より

ではレーブの定理を証明します。
レーブの定理
$B(BC\supset C)\wedge B(k\equiv (Bk\supset C))\supset BC$
証明　 $(1)B(k\equiv (Bk\supset C))\supset B(Bk\supset BC)$ 　∵補題２より

　　　 $(2)B( (Bk\supset BC\wedge BC\supset C)\supset (Bk\supset C))$

　　　　　　∵ $( (X\supset Y)\wedge (Y\supset Z))\supset (X\supset Z)$ の $X$ を $Bk$ , $Y$ を $BC$ ,

　　　　　　　 $Z$ を $C$ に置き換え

　　　 $(3)B(BC\supset C)\wedge B(k\equiv (Bk\supset C))\supset B(Bk\supset C)$ ∵(1),(2),(A1b)より

　　　 $(4)B(Bk\supset C)\wedge B( (Bk\supset C)\equiv k)\supset Bk$ 　∵(A1b)より

　　　 $(5)Bk\supset BBk$ 　∵(A3)より

　　　 $(6)BBk\wedge B(Bk\supset C)\supset BC$ 　∵(A1b)より

　　　　∴ $B(BC\supset C)\wedge B(k\equiv (Bk\supset C))\supset BC$ 　∵(3),(4),(5),(6)より

これで、レーブの定理が示せました。
実は、本はまだ半分までしか読んでないので、これがレーブの定理の全てなのかは分かりません。（まだ読んでないとこにも出てきていたので）
実際にはもっと詳しく書いてあるので、興味があったらぜひ読んでみてください。