MATHEMATICAチュートリアル

限定子

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

ForAll[x,expr]	x のすべての値で成り立つ expr
ForAll[{x₁,x₂,...},expr]	すべての x_i のすべての値で成り立つ expr
ForAll[{x₁,x₂,...},cond,expr]	cond を満たすすべての x_i で成り立つ expr
Exists[x,expr]	expr が成り立つ値 x が存在する
Exists[{x₁,x₂,...},expr]	expr が成り立つ複数の値が存在する
Exists[{x₁,...},cond,expr]	cond を満たす expr が成り立つ複数の値が存在する

量限定子の構造

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

これは，この不等式が成立する値

が存在することを宣言している．ここでの出力は入力を別の形にフォーマットしたものに過ぎない．

In[1]:=

Out[1]=

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

In[2]:=

Out[2]=

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

In[3]:=

Out[3]=

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

_xexpr	ForAll[x,expr]
_{{x₁,x₂,...}}expr	ForAll[{x₁,x₂,...},expr]
_x,condexpr	ForAll[x,cond,expr]
_xexpr	Exists[x,expr]
_{{x₁,x₂,...}}expr	Exists[{x₁,x₂,...},expr]
_x,condexpr	Exists[x,cond,expr]

量限定子の表記法

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

Resolve[expr]	expr から量限定子を除去しようとする
Resolve[expr,dom]	領域 dom 中にあると仮定されるすべての変数の量限定子を除去しようとする

量限定子の除去

これはこの方程式を真にする

が存在することを示している．

In[4]:=

Out[4]=

これは，

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

In[5]:=

Out[5]=

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

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

In[6]:=

Out[6]=

これはこの式が真になるように

と

に真値を割り当てる方法があることを示している．

In[7]:=

Out[7]=

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

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

In[8]:=