Homeにもどる

QEの計算例: 全称量化子 $\forall$ を含む論理式の量化子消去

例題

方程式 $ax^2+bx+c=0$ が実根（実数解）をもたないための $a,b,c$ の条件を求めよ。

解法

1階述語論理式の構成

この問題で示すべき条件を書き出して変形すると

任意の実数 $x$ が方程式 $x^2+bx+c=0$ の根になることはない

$\Leftrightarrow$ 任意の実数 $x$ に対して関数 $x^2+bx+c=0$ が成り立つことはない

$\Leftrightarrow$ 任意の実数 $x$ に対して $x^2+bx+c\ne 0$ が成り立つ

となりますので、この問題を表す1階述語論理式は

$$\forall x (ax^2 + bx + c \ne 0)$$

となります。

Mathematica への論理式の入力とQEによる解法

Mathematica に入力する論理式を定義します。

f2 = ForAll[x, a x^2 + b x + c != 0]

Reduce関数に論理式を入力して量化子消去を実行します。

Reduce[f2, Reals]

すると、次の出力が得られます。

(c < 0 && ((b < 0 && a < b^2/(4 c)) || (b == 0 && a <= 0) || (b > 0 && a < b^2/(4 c)))) || (c > 0 && ((b < 0 && a > b^2/(4 c)) || (b == 0 && a >= 0) || (b > 0 && a > b^2/(4 c))))

出力の意味は次の論理式です:

$$( c<0 \wedge ( (b<0 \wedge a<\frac{b^2}{4c} ) \vee (b=0 \wedge a\le 0 ) \vee (b>0 \wedge \frac{b^2}{4c} ) ) \vee (c > 0 \wedge ((b<0 \wedge a < \frac{b^2}{4c}) \vee (b=0 \wedge a \ge 0) \vee (b>0 \wedge \frac{b^2}{4c} ))$$

ちょっと複雑ですね。

これも、先の例と同様に、変数を消去する順序を変えて、再計算してみましょう。

Reduce[f2, {a,b,c}, Reals]

すると、次の出力が得られます。

(a < 0 && c < b^2/(4 a)) || (a == 0 && b == 0 && (c < 0 || c > 0)) || (a > 0 && c > b^2/(4 a))

出力の意味は次の論理式です:

$$(a < 0 \wedge c < \frac{b^2}{4 a}) \vee (a = 0 \wedge b = 0 \wedge (c < 0 \vee c > 0)) \vee (a > 0 \wedge c > \frac{b^2}{4 a})$$

上の論理式は、一番外側に選言（または）がありますので、そこで論理式を分けましょう。同値な論理式は、次の「1. または 2. または 3.」となります（3つの論理式の並べ方を変えています）。

1. $$a < 0 \wedge c < \frac{b^2}{4 a}$$
2. $$a > 0 \wedge c > \frac{b^2}{4 a}$$
3. $$a = 0 \wedge b = 0 \wedge (c < 0 \vee c > 0)$$

論理式 3. の $(c < 0 \vee c > 0)$ は $c\ne 0$ と同値ですから、論理式 3. からは

$$a = 0 \wedge b = 0 \wedge c\ne 0$$

という条件が導かれます。

一方、論理式 1. と 2. に出てくる不等式については、$a$の正負に注意して分母を払うと、それぞれ

1. $a<0$より$c < \frac{b^2}{4 a} \Leftrightarrow 4ac>b^2 \Leftrightarrow b^2-4ac<0$
2. $a>0$より$c > \frac{b^2}{4 a} \Leftrightarrow 4ac>b^2 \Leftrightarrow b^2-4ac<0$

となり、$a$の正負にかかわらず、$b^2-4ac<0$（すなわち、判別式の値が負）という条件にまとめられます。ゆえに、論理式 1. と 2. からは

$$a\ne 0 \wedge b^2-4ac<0$$

という条件が導かれます。