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 になってもかまいません.