4.8　場合分け

　次に場合に分けて証明するときの話をします．証明したいのは A and B という命題で，この命題は場合分けすれば証明できるとします．例えばx=1 の場合と x=2 の場合と，x がその他の値を取る場合とに分けて証明したいとします．x=1, 2で特異点になっているということです．このときには次のような証明の構造をとります．

　　　　L:( x=1 or x=2　or not ( x=1 & x=2 ))
　　　　　 now per cases by L;
　　　　　　case LA:x=1;
　　　　　　 ······
　　　　　　thus A and B;

　　　　　　case LB:x=2;
　　　　　　 ······
　　　　　　thus A and B;

　　　　　　case LC:not (x=1 & x=2);
　　　　　　 ······
　　　　　　thus A and B;

　　　　　 end;


　now per cases　〜 endの中で，それぞれの場合について case を分けて証明します．
case x=1 から最初の thus A and B までで x=1 のときの証明をします．同様に，x=2 の時，その他の場合についても証明します．このとき，now から end までの文は全体で1つの A and B とみなします．例えば now 〜 end の後に then とすれば，then は now 〜 end 全体を受けるわけです．case でそれぞれの場合に分けられていますが，それぞれの場合の帰結の部分を最後に渡すわけです．ですから，これ全体を引用したときには case に分かれたということは忘れてしまって，結論だけが全部同じということがチェックされるわけです．だからこれは1つの式だということです．なお，Lのような式は論理的に明らかなので，now per cases by L の by L はなくてもいいのです．