Xk 量化子のネスト

　RedLog や Mathematica の量化子は変数のリストを束縛することが可能で，これまでも

ex ( {x,y} , x^2+y^2=2 and x+y=a );

のような例を数多く扱ってきましたが，実際に入力すれば，直ちに

ex(x,ex(y,a - x - y = 0 and x**2 + y**2 - 2 = 0))$

となることからも明らかなように，それは量化子のネストによって実現され，その換言はロジックとしても正しいものです．
　一方，QEPACD B にはリストの束縛機能はありませんので，最初から

echo -e "[] \n (a,x,y) \n 1 \n (Ex)(Ey)[ x^2+y^2=2 /\ x+y=a]. \n finish" | qepcad

のように入力するわけですが，量化子として前回述べた Xk を用いる際には，以下の注意が必要です．
　それは，一般に P を満たす X が丁度 1 個存在することを ∃!X ( P ) で表すとき，∃!(x,y) ( p ) と ∃!x ( ∃!y ( p ) ) とは同値とは限らないという事実です．例えば

∃!(x,y) ( x≦0 ∧ y≦0 ∧ a≦x+y )

は a=0 と同値ですが

E!y ( y≦0 ∧ a≦x+y )

は x=a と同値なので

∃!x ( E!y ( x≦0 ∧ y≦0 ∧ a≦x+y ) )

は a≦0 と同値になります．従って，例えば

echo -e "[] \n (a,x,y) \n 1 \n (X1x)(X1y)[ x^2+y^2=2 /\ x+y=a]. \n finish" | qepcad

と入力して

a + 2 >= 0 /\ a - 2 <= 0 /\ [ a - 2 = 0 \/ a + 2 = 0 ]

を得ても，それが円周と直線との共有点の個数が 1 となる条件だというのはロジックとして早計なのです．