Chapter 4

証明の方法

4.1　基本的な証明方法

　証明の方法について説明します．証明の方法としては，さきほど説明したように，

　　　　証明したい式
　　　　proof
      · · ·
      · · ·
　　　　　thus (hence) ...;
　　　　　end;

　証明したい式をまず書き， proof (証明)， end; (証明終り)の間に証明を書きます．証明の最後の行は必ずthus　. . . またはhence . . . で終わります．
　p implies qという命題を証明したいとします．

　　　　p implies q
　　　　 proof
　　　　 assume p;　　　　　　p を仮定する
      · · ·
      · · ·
　　　　 thus q;　　　　　　　　q が示せた
　　　　end;

　まず証明したい式　p implies q を書き， proof , end; と書きます． proof にはセミコロンをつけなくて， end にはセミコロンをつけます． p であるならばqということを証明すれば良いのですが， p というのはこれも1つの論理式になっているのです．まず，assume p と書き p を仮定し，それから q が示せたら thus q で証明終りです．　次に，a=c が仮定されいて，b=c implies a=b を証明したいしますと，次のようになります．仮定の a=c には A: というラベルをつけておきます．

　　　　A:a=c;
　　　　　　b=c implies a=b
　　　　　　proof
　　　　　　　assume B:b=c
　　　　　　　hence thesis by A;
　　　　　　end;

　assume . . . で . . . を仮定するということになります．仮定部であることを示すわけです．また， hence . . . は hence の直前の式と hence の式の理由部からこの証明の最後の式がいえたということを示します． thesis とは,示すべき式ということです．
　thus と hence をもう少し詳しく説明しましょう．
　thus と hence は証明中で使いましたが，証明すべき式が thus と hence があらわるたびに証明済の部分が & でつながった式よりそぎ落とされて簡単になっていきます.例えば，

　　　　theorem　3-1=2　&　5-2=3　&　6-3=3
　　　　proof　2+1=3;
　　　　 hence　3-1=2 by REAL_2:17;
　　　　 3+2=5;
　　　　 hence　5-2=3　by REAL_2:17;
　　　　 3+3=6;
　　　　 hence thesis by REAL_2:17;
　　　　end;


は and でつながった3つの式の証明です．最初の hence で 3-1=2 が証明されましたので，5-2=3 & 6-3=3 が証明すべき式となります．次の hence で 5-2=3 が証明されましたので，6-3=3 が最終的に証明すべき式となります．最初に hence thesis で，残りの部分 (6-3=3) が全て証明されたことになります．
　なお，hence は前述したように then と thus を組み合わせたものです．例えば，

　　　　A1: A=B;
　　　　A2: B=C;
　　　　thus A=C by A1,A2;
　　というのを,
　　　　A1: A=B;
　　　　B=C;
　　　　hence A=C by A1;


と書けます.