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 の特徴の一つである量化子の拡張について殆ど述べていないことに気付きました． QEPCAD B には，特称量化子 E，全称量化子 A の他に F = "for infinitely many" G = "for all but finitely many" C = "for a connected sub…