Homeにもどる

QEの計算例: 複数個の束縛変数と、自由変数を含む論理式の量化子消去

例題

不等式 $ax^2+y^2+az^2-xy-yz-zx\ge 0$が任意の$x,y,z$に対して成り立つような定数$a$の値の範囲を求めよ。

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

解法

1階述語論理式の構成

この問題を表す1階述語論理式は

$$\forall x \forall y \forall z (ax^2+y^2+az^2-xy-yz-zx\ge 0)$$

となります。この論理式に対してQEを行うと、変数$x,y,z$が消去され、変数$a$のみを含む論理式が出力されるはずです。

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

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

f3 = ForAll[{x,y,z}, a x^2 + y^2 + a z^2 - x y - y z - z x >= 0]

この式を入力する際は、以下の点に注意します。

1. $\forall x \forall y \forall z$より、複数個の変数に量化子をつける場合は、{x,y,z}のようにリストの形で変数を与えます。
2. 変数と変数や、係数と変数の積を書く場合は、各変数や定数の間にスペースを入れます。そうしないと、たとえば xy という新しい記号（変数）と見なされることがあります。

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

Reduce[f3, Reals]

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

a >= 1

出力として、問題の答え $a\ge 1$ が直ちに導かれます。