数式処理の専門家の人はよく知っているのが、そうでない人は全く知らない、そんな技術の一つが量限定子除去と呼ばれる技術です。英語ではQuantifier Elimination, 略してQ.E.とも言われます。
具体的には実数の世界に限定して、多項式を項とする、等号や不等号を述語とする１階述語論理の世界を考えます。例えば、
$$ x^2\geq 0$$
は不等号を述語とし、多項式を項とする式です。これに全称量限定子を付けてみます。
$$ \forall x,\, x^2\geq 0$$
この式は確かに成り立ちます。
$$ \mathbf{true}$$
となります。Q.E.の用語で言えば、(2)に量限定子除去を適用すると(3)が得られる、という訳です。
別の例題を考えてみます。
これは \( y=x^3-6\,x \) という関数のグラフです。このグラフを見ると大体ですが、\( -\frac{5}{2}\leq x \)の範囲では \( y > -6 \) が成り立ちそうです。論理式で書いてみると、
$$\forall x\, \left(x\geq -\frac{5}{2}\right) \implies \left(x^3-6\,x>-6\right)$$
この(4)もQ.E.を適用すると\( \mathbf{true} \)が得られるはずです。でも\( x>-3 \) の範囲では成り立ちそうにありません。つまり、
$$\forall x\, \left(x\geq -3 \right) \implies \left(x^3-6\,x>-6\right)$$
にQ.E.を適用すると \( \mathbf{false} \) が得られるでしょう。
このように真偽値が決まる文に対してQ.E.を適用すると、その文の真偽を決定することになります。
