次に述語命題にはいっていきます．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 ...は 1 つの論理式になっています．
4.6.2 such that を使った書き方
それから，もう 1 つの書き方として次のようなものがあります．
for x,y st P[x,y] holds Q[x,y]
proof
let xs,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 という1
つの文を，A という文と，B という文とに分けたということです．それに対して，後の書き方はあくまで
1
つの文で，論理演算子でつながったものです．このように，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;
これだけ書きます．引用が
1
つの場合にも 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を使います．