証明.

⊢󱁑A⥎A󰎘 を仮定する。 B の構造に関する帰納法を用いる。

まず、 A≡B であるときに命題の主張を示す。 このとき、 B{A:=A󰎘} は B か A󰎘 のいずれかである。 B{A:=A󰎘}≡B のときは、 示すべきは ⊢󱁑B⥎B であるが、 これは明らかに成り立つ。 B{A:=A󰎘}≡A󰎘 のときは、 示すべきは ⊢󱁑B⥎A󰎘 であるが、 今 A≡B だったのでこれは仮定そのものである。 以上により、 この場合は命題の主張が示された。

次に、 A≢B の場合を考える。 B の構造によって場合分けをする。

B≡pn のとき。 今 A≢pn であって pn は自分自身以外に部分式をもたないので、 pn{A:=A󰎘} において置き換えは実際には起こっておらず、 pn{A:=A󰎘}≡pn である。 したがって、 示すべきは ⊢󱁑pn⥎pn であるが、 これは明らかに成り立つ。

B≡⊤ や B≡⊥ のときも、 上の場合と同様に示される。

B≡X∧Y のとき。 帰納法の仮定により、 ⊢󱁑X⥎X{A:=A󰎘}⊢󱁑Y⥎Y{A:=A󰎘} がともに成り立つ。 これに命題 5.1 を使うことで、 ⊢󱁑X∧Y⥎X{A:=A󰎘}∧Y{A:=A󰎘} が分かる。 さて、 今 A≢X∧Y だから、 (X∧Y){A:=A󰎘} における置き換えは (起こっているとしたら) X と Y の内部で起こっている。 したがって、 (X∧Y){A:=A󰎘}≡X{A:=A󰎘}∧Y{A:=A󰎘} と書ける。 これと上の式を合わせれば、 ⊢󱁑X∧Y⥎(X∧Y){A:=A󰎘} が得られるが、 これはまさに示したかった ⊢󱁑B⥎B{A:=A󰎘} である。

B≡X∨Y や B≡X⇀Y や B≡¬X のときも、 上記と同様に命題 5.1 から示される。

B≡◻X のとき。 帰納法の仮定により、 ⊢󱁑X⥎X{A:=A󰎘} が成り立つ。 今度は命題 5.3 を使うことで、 ⊢󱁑◻X⥎◻(X{A:=A󰎘}) が分かる。 今 A≢◻X だから、 (◻X){A:=A󰎘}≡◻(X{A:=A󰎘}) と書くことができ、 これにより、 ⊢󱁑◻X⥎(◻X){A:=A󰎘} が得られた。 これが示したかった式である。

B≡⬦X のときは、 命題 5.5 を使うことで同様の議論で示される。

これで全ての場合が尽くされたので、 命題の主張が示された。

証明.

⊢󱁑A⥎A󰎘 を仮定すれば、 命題 6.1 によって ⊢󱁑B⥎B{A:=A󰎘} が成り立つ。 さらに ⊢󱁑B が成り立っていれば、 これと命題 5.1 によって ⊢󱁑B{A:=A󰎘} が得られる。