Homeにもどる

QEの計算例: 関数定義を伴う解法

例題

$a$, $b$ は実数とする。3次方程式 $x^3-3ax^2+a+b=0$が3個の相異なる実数解をもち、そのうち1個だけが負となるための$a$, $b$の満たす条件を求めよ。

（出典： チャート式 基礎からの数学 I + A （青チャート） (2011), Ex. 141）

解法

1階述語論理式の構成

まず、$x^3-3ax^2+a+b$ を関数$f(x)$として定義します。

f[x_] := x^3 - 3 a x^2 + a + b

関数の定義を行う式の書き方は以下の通りです。

• 関数の引数のカッコには大カッコ [] を使います。
• 関数の引数の後ろに _ （アンダースコア）をつけます。
• 等号は := を使います。

次に、問題では「3次方程式 $f(x)=0$ が3つの相異なる実数解をもつ」とされていますので、これらの解を x1, x2, x3 で表します。

そして、問題から、x1, x2, x3 が満たすべき条件を以下の通り得ます。

• ある実数$x1,x2,x3$が存在して、$f(x1)=0$, $f(x2)=0$, $f(x3)=0$を満たす。
• x1, x2, x3 のうち1個は負なので、$x1<0$ とする。
• x2, x3 は非負で、かつ $x2\ne x3$である。

以上より、この問題から、次の1階述語論理式を得ます。

$$\exists x1 \exists x2 \exists x3 (f(x1)=0 \wedge f(x2)=0 \wedge f(x3)=0 \wedge x1<0 \wedge x2\ge 0 \wedge x3 \ge 0 \wedge x2\ne x3)$$

この論理式に対してQEを行うと、変数$x1,x2,x3$が消去され、変数$a,b$のみを含む論理式が出力されるはずです。

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

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

f4 = Exists[{x1, x2, x3}, f[x1] == 0 && f[x2] == 0 && f[x3] == 0 && x1 < 0 && x2 >= 0 && x3 >= 0 && x2 != x3]

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

Reduce[f4, Reals]

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

a > 0 && -a < b < -a + 4 a^3

出力として、問題の答え $a > 0 \wedge -a < b < -a + 4 a^3$ が直ちに導かれます。