QE で独立

　今回は線形代数のお話です．係数，数ベクトルの成分は実数とします．
　まず，線形独立な 2 個の 2 項数ベクトルが存在することを見ましょう．数ベクトル(a,b),(c,d)が線形独立であるとは

∀s ∀t ( s(a,b) + t(c,d) = (0,0) → s=t=0 )

ということでしたから

Reduce[
　Exists[{a, b, c, d},
　　ForAll[{s, t}, s*a + t*c == s*b + t*d == 0, s == t == 0]
　],
　Reals
]

のように QE すれば

True

と出力されます．では，どのようなベクトルが線形独立なのか？ということで

Reduce[
　ForAll[{s, t}, s*a + t*c == s*b + t*d == 0, s == t == 0]
]

と問えば，Mathematica は

(a == 0 && b c != 0) || a (-b c + a d) != 0

のように a で場合を分けてしまうので

rlqepcad all ( {s,t}, s*a + t*c = s*b + t*d = 0 impl s = t = 0 );

と問えば，QEPCAD B は

a*d - b*c <> 0

と答えてくれます．
　次に，任意の 3 個の 2 項数ベクトルが線形従属であることを確かめます．数ベクトル(x1,y1),(x2,y2),(x3,y3)が線形従属であるとは

∃c1 ∃c2 ∃c3( c1(x1,y1) + c2(x2,y2) + c3(x3,y3) = (0,0) ∧ ¬(c1=c2=c3=0) )

ということでしたから

Reduce[ForAll[{x[1], y[1], x[2], y[2], x[3], y[3]},
Exists[{c[1], c[2], c[3]},
Sum[c[k]*{x[k], y[k]}, {k, 1, 3}] == {0, 0},
Not[c[1] == c[2] == c[3] == 0]]], Reals]

のように QE すれば

True

と出力されます．これで，2 項数ベクトル全体からなる空間 R^2 の次元は 2 であることが判りました．