3.4.11 発展：限定子

x^4 + x^2 > 0のような命題で，Mathematicaは変数xを特定はされていないが限定的な値を持つものとして扱う．しかし，場合によってはxが取りうる可能な値の集合についての陳述を行うことができると便利である．そのような場合には「限定子」を使うとよい．

量限定子の構造

Mathematicaでは方程式，不等式，論理結合等と同じように量限定子も扱うことができる．ほとんどの場合，量限定子は評価によってすぐに変化はしない．しかし，FullSimplifyやReduceのような関数を使って量限定子を簡約することができる．

これは，この不等式が成立する値xが存在することを宣言している．ここでの出力は入力を別の形にフォーマットしたものに過ぎない．

In[1]:= Exists[x, x^4 + x^2 > 0]

Out[1]=

FullSimplifyによって宣言が真であることが確認される．

In[2]:= FullSimplify[%]

Out[2]=

xがゼロのときは不等式が成立しないので，この場合はFalseが返される．

In[3]:= FullSimplify[ForAll[x, x^4 + x^2 > 0]]

Out[3]=

Mathematicaは述語論理と純粋数学で使われている量限定子の標準的な表記によるバージョンをサポートしている．は\[ForAll]あるいは faとして入力できる．また，は\[Exists]あるいは exとして入力できる．表記を厳密にするために，Mathematicaは限定子のとついた変数を下付き文字にする．変数の条件もまたコンマで区切った下付き文字にする．

量限定子の表記法

量限定子を含む命題を，量限定子を除去した等価の命題に変換できる場合がある．量限定子の除去は，すべてのxあるいは特定のxについて真であるという黙示的な宣言を，これが成立する条件に関する明示的な宣言に変換する点で，方程式を解くのに似ている．

量限定子の除去

これはこの方程式を真にするxが存在することを示している．

In[4]:= Resolve[Exists[x, x^2 == x^3]]

Out[4]=

これは，cが特定の条件に従った場合にのみこの方程式が満たされることを示している．

In[5]:= Resolve[Exists[x, x^2 == c && x^3 == c + 1]]

Out[5]=

Resolveは，複素領域と実数領域の任意の整方程式と不等式から常に量限定子を除去することができる．また論理式からも量限定子が除去できる．

これは実数領域の2次方程式の制約条件が正であることを示している．

In[6]:= Resolve[ForAll[x, a x^2 + b x + c > 0], Reals]

Out[6]=

これはこの式が真になるようにpとqに真値を割り当てる方法があることを示している．

In[7]:= Resolve[Exists[{p, q}, p || q && ! q], Booleans]

Out[7]=

Reduceでも量限定子を使うことができる．Reduceに方程式あるいは不等式の集合を与えると，Reduceは完全な解の集合の詳細に渡る表現を作成しようとする．しかし，ときには解がxのすべての値を網羅している，あるいはこの値を全くカバーしていないといった，より大局的な問いに対する答えが欲しい場合もあるだろう．量限定子は，このような問いを指定する便利な方法を提供している．

これは解の集合の完全な構造を与える．

In[8]:= Reduce[x^2 + x + c == 0, {c, x}, Reals]

Out[8]=

一方これは解が存在するための条件だけを与える．

In[9]:= Reduce[Exists[x, x^2 + x + c == 0], {c}, Reals]

Out[9]=

量限定子を使って多くの数学的な問題を形成することができる．

これは円を任意の円錐曲線内に入れる条件を求める．

In[10]:= Reduce[ForAll[{x, y}, x^2 + y^2 < 1, a x^2 + b y^2 < c],
{a, b, c}, Reals]

Out[10]=

これは線が円を横切る条件を求める．

In[11]:= Reduce[Exists[{x, y}, x^2 + y^2 < 1, r x + s y == 1],
{r, s}, Reals]

Out[11]=

これはqが主係数が1の一般的な4次方程式であると定義する．

In[12]:= q[x_] := x^4 + b x^3 + c x^2 + d x + e

これで，4次方程式のすべての根のペアについての条件が等しいことが分かる．

In[13]:= Reduce[ForAll[{x, y}, q[x] == 0 && q[y] == 0, x == y],
{b, c, d, e}]

Out[13]=

整数について量限定子を除去するのは一般的に，計算上不可能な問題であるが，Mathematicaは特別な場合に限ってこれを行うことができる．

これはが有理数ではあり得ないことを示している．

In[14]:= Resolve[Exists[{x, y}, x^2 == 2 y^2 && y > 0], Integers]

Out[14]=

は有理数である．

In[15]:= Resolve[Exists[{x, y}, 4 x^2 == 9 y^2 && y > 0], Integers]

Out[15]=