数学基礎論講義をこっそり読む（その２）
引き続きこっそり読んでいます。もうちょっとでPartA 第三講が終わります。
いくつか、コメントというかメモっぽいものを。
p.31 定理3.2（演繹定理）の証明は読者に任されていますが、その証明中で唯一問題になりそうなのは
の導出だと思います。ちょこちょこ参考に見ている 前原昭二著『数学基礎論入門』では、は公理であり、導出規則
の代わりに
となっており、これらから上の式は次のように証明できます。
は推論規則から、
公理より
は、
(公理）の形なので定理であり、
が得られ、全部つなげると証明完了。
『数学基礎論講義』の公理系は『数学基礎論入門』のものに等価なので、実のところテクニカルには同値関係（ここではAを仮定してB、Bを仮定してAが導出できるとき A⇔Bとする）
が成立しており、これを認めればすぐに証明できるのですが、テキスト中では論理記号についての説明をすっとばしているのでいかんとも…そこでこれと等価な、
を直接示します。ショートカットのため、少しゲンツェン流の入った証明図です。矛盾から前提のどれか一つの否定が導出できるのはp.19補題2.5からです。この論法により、
から
という導出が可能です。また
等も黙って定理として使っています。ただし、Aを仮定してBが証明できたとき、Aの仮定なしにA→Bが証明できるという仮定の消去のルールを無反省には使えません。これは証明したい演繹定理そのものだからです。ただし、下の証明のように証明が命題論理の証明図と同じ構造のものは、命題論理の演繹定理よりその使用が正当化されます。
の証明図：
の証明図：
