4.7 存在記号

さらにいろいろなスケルトンがあります．存在記号を含んだ述語論理式 ex x st P[x] の証明のしかたですか，この場合 take というものを使います．

takeを使って，



　ex x st P[x]



   proof



    L:P[a];



    take x=a;



    then P[x] by L;



    thus thesis;



   end;

と書きます．P[x] を満たす x が存在することを証明するときに，P[a] が証明されたとします．すると take x=a として， 存在する x として, a を取ってくれば， L よる証明されたことになります．

4.7.1 considerの使い方

take と逆の言葉として consider があります．



  (ex x st P[x]) implies for y st Q[y] holds R[y]



   proof



    assume ex x st P[x];



    then consider a such that L:P[a]



    ......



    ......



    let y such that Q[y];



    ......



    ......



    thus R[y];



   end;

と，なります．まず，assume します． assume ex x st P[x]; として，ここで consider を使って， then consider a such that L:P[a] ，とします．この場合も such that がきますから，ラベルがないといけません．そして，こうしておいて，次に for y st...... を言うために let y such that Q[y] として， thus Q[y] が言えればいいわけです．

consider とは，P[x] を満たすような x が存在するとき，その存在する x に，なにか固有名詞を与えるという意味です．だから存在する x をいま１つ話題にしましょうということです．ですから，x でなくてもかまいません．a でもいいです．

存在する a として，ここでは a が固有名詞のように使えるわけです．どこかに存在するとして使われているわけです．ですから consider は take の逆になります． take は固有名詞で何かにおけることに，存在記号をもって来ることに使います．

4.7.2 givenの使い方

それから，ちょっと変わったスケルトンがあります．



  (ex x st P[x]) implies for y st Q[y] holds R[y]



   proof



    given x such that P[x];



    ......



    ......



    let y



    assume Q[y];



    ......



    ......



    thus R[y];



   end;

この中で2行目の given x such that P[x] ; の given は assume と consider を合わせた働きがあるわけです．

と覚えてください．こちらの方が簡単です．