4.6 全称記号

次に述語命題にはいっていきます．for x holds p[x] & q[x] の証明をします．なお p[x] とは x を含んだ述語という意味で，かぎかっこが許されているわけではありません．



  for x holds P[x] & Q[x]



   proof



    let x;



     ......



     ......



    thus P[x];



     ......



     ......



    thus Q[x];  (thesis)



   end;

全称記号 for に対する言葉として let があります． let x としておいて，thus P[x] で， P を証明します．さらに thus Q[x] で Q を証明します．

それから混乱しなければ，これは文字が変わってもかまいません．例えば y になってもかまいません．

4.6.1 変数が2つある場合

それから次の様に変数が2つある場合ですが，



  for x,y st P[x,y] holds Q[x,y]



   proof



    let x,y;



    assume P[x,y];



     ......



     ......



    thus Q[x,y];   (thesis)



   end;

このように変数を2つ書きます．直接的には，( ∀x )( ∀y )( P(x,y) ⇒ Q(x,y) ) を証明したことになります．assume ..... は１つの論理式になっています．

4.6.2 such thatを使った書き方

それから，もう1つの書き方として次のようなものがあります．



  for x,y st P[x,y] holds Q[x,y]



   proof



    let x,y such that L:P[x,y];



     ......



     ......



     ......



    thus Q[x,y];



   end;

なお，such that のあとに，ふつうはラベルを入れますが（この例の場合 L），入れなくてもかまいません．そして，最初の行のは st で，3行目は such thatです．

4.6.3 文の分割

こういうスケルトンがあります．



  for x,y st P[x,y] & Q[x,y] holds R[x,y]



   proof



    let x,y such that L1:P[x,y] and L2:Q[x,y];



    ......



    ......



    thus R[x,y];



   end;

これを次のように書き換えることもできます．注意しなければならないのは & と and の違いです．

3行目の，



      let x,y such that L1:P[x,y] and L2:Q[x,y];

は，



      let x,y such that L:P[x,y] & Q[x,y];

というふうに，書くこともできます．前の書き方と後の書き方は原理的には同じです．前の書き方の and は，別のラベルをたてるために2つの文に分けるためのものです．これは，A & B という１つの文を，A という文と，B とういう文とに分けたということです．それに対して，後の書き方はあくまで１つの文で，論理演算子でつながったものです．このように，and を使って1つの文を2つの文に分けたり，逆に & を使って2つの文を1つの文にすることもできます．

4.6.4 文の分割 assumeでの場合

such that 後の書き方の違いですが，これと似たことは assume の場合にも起こります．例えば，assume の例に，& S[x,y]を加えて，



  for x,y st P[x,y] & S[x,y] holds Q[x,y]



   proof



    let x,y;



    assume P[x,y] & S[x,y];



    ......



    ......



    thus Q[x,y];



   end;

と，なったとします．

このとき，



       assume P[x,y] & S[x,y];

は，



       assume that L1:P[x,y] and L2:S[x,y];

と書くこともできます．後の書き方に限って，P[x,y] と S[x,y] の両方にそれぞれにラベルを書くことができます．この例では L1，L2 というラベルです．

4.6.5 thatの後の注意

thatの使い方についていいますと，that の後には then を使うことができません．どうしてかというと，such that の後に2つ以上の文があるかもしれないと考えるからです．2つ以上の文がある場合は，直前の文というのがはっきりしません．ですから，



  assume that A and B;



  then C;

こういう書き方はできません．必ずラベルを使って，



  assume that L1:A and L2:B;



  C by L1,L2;

こういうふうに書かないといけません．あるいは，B だけ使うときは，



  C by L2;

これだけ書きます．引用が１つの場合にも then は使えません．then でなく by L2 と書かなければいけません．ですから that が来たらラベルが来なければこの文は使えません．つまり，後で引用することができません．したがって，that の後には必ずラベルが来ると考えられます．

that をつけなければ then を使えます．ですから，最初の書き方，

assume P[x,y] & Q[x,y] の場合は，



  assume P[x,y] & Q[x,y];



  then ......

と使うことができます．that がなくて，1つの文しかないわけです．assume のときは then を使います．