QEPCAD B の量化子

　ブログを読み返してみて，QEPACD B の特徴の一つである量化子の拡張について殆ど述べていないことに気付きました．
　QEPCAD B には，特称量化子 E，全称量化子 A の他に

F = "for infinitely many"
G = "for all but finitely many"
C = "for a connected subset"
X k = "for exactly k distinct values" （ただし，kは正の整数）

という量化子があり，E，A を含め，これらの量化子は

束縛変数の条件が定める集合 S の性質を規定するもの

であり，それぞれ

E は S が空集合でない
A は S が実数全体の集合
F は S が無限集合
G は S の補集合が有限集合
C は S が連結集合
X k は S の濃度（要素の数）が k
（空集合は有限集合，連結集合であることに注意．また，QEPCAD B（というかRCF）の表現力の制限により「Sが無限集合⇔Sが内点をもつ」である．）

という性質に対応しています．例えば，コマンドプロンプトに

echo -e " \n (a,b,x) \n 2 \n (Ex)[x^2>a]. \n finish" | qepcad
echo -e " \n (a,b,x) \n 2 \n (Ax)[x^2>a]. \n finish" | qepcad
echo -e " \n (a,b,x) \n 2 \n (Fx)[x^2>a]. \n finish" | qepcad
echo -e " \n (a,b,x) \n 2 \n (Gx)[x^2>a]. \n finish" | qepcad
echo -e "[] \n (a,b,x) \n 2 \n (Cx)[x^2>a]. \n finish" | qepcad

と入力すれば，各結果は

TRUE
a < 0
TRUE
a <= 0
a < 0

となり

echo -e " \n (a,b,x) \n 2 \n (X1x)[x^2=a]. \n finish" | qepcad
echo -e " \n (a,b,x) \n 2 \n (X2x)[x^2=a]. \n finish" | qepcad
echo -e "[] \n (a,b,x) \n 2 \n (X3x)[x^2=a]. \n finish" | qepcad

と入力すれば，各結果は

a = 0
a > 0
FALSE

となります．
　これらのうち，A，F，G について

(Ax)[…] ならば (Gx)[…] ならば (Fx)[…]

が成り立ちますが，F，G では代数的数のコストの高いある種の計算を避けられることから，それが可能であれば A の代わりに F，G を用いることが推奨されています（ http://www.usna.edu/Users/cs/qepcad/B/user/EnterForm.html ）．
　なお，この「〜を除いて」という立場の一つである「殆ど至る所」すなわち，補集合の測度が 0 という性質を自由変数の条件が定める集合に適用するコマンドが measure-zero-error です．例えば

echo -e "[] \n (a,b,c,x) \n 3 \n (Ex)[a x^2+b x+c=0]. \n finish" | qepcad

と入力すると

4 a c - b^2 <= 0 /\ [ c = 0 \/ a /= 0 \/ 4 a c - b^2 < 0 ]

のように出力されますが

echo -e "[] \n (a,b,c,x) \n 3 \n (Ex)[a x^2+b x+c=0]. \n measure-zero-error \n finish" | qepcad

とすれば

4 a c - b^2 <= 0

のように薄っぺらな部分（零集合）にしかならない条件を考慮しない実務向き？の出力となります．

　また，F，Gについては，pが式のとき

　(Fx)[p] ⇔ {x|p}は無限集合 ⇔ ~({x|p}は有限集合)

そして

　(Gx)[p] ⇔ {x|~p}は有限集合

なので，A，Eと同様に

　(Gx)[ ~p ] ⇔ ~[ (Fx)[p] ]
　(Fx)[ ~p ] ⇔ ~[ (Gx)[p] ]

となります（ただし，QEPCAD Bでは最後の右辺のような式は作れません）．