「開いた式」

「開いた式」とは「変数の自由出現(あるいは自由変数)を含む論理式」のことで,その真理値の定め方には幾つかの立場があります.

言語,構造を固定した上で,伝統的(?)なのは,変数への個体割り当てを用いて

立場1 割り当て毎に真偽を与える

立場2 割り当て毎には充足性(=立場1での真偽)を与え,任意の割り当てが充足する式に真を与える(ただし,偽は否定した式が真のこととするので,その式も否定も真とならないことがある)

というものです.

恒真性の定義では,構造,割り当てともに動くので(証明可能性が全称閉包をとっても変わらないことに対応),どちらの立場でも構いませんし,閉じた式(変数の自由出現を含まない論理式,いわゆる文)なら尚更ですから,変数への個体割り当てを用いずに,最初から

立場3 全称閉包を評価する

のが簡明です.

というわけで,pvs に

x,y:var real
f1:lemma x=y => (x=y or x<y)

と入力すると,黙って

f1 :  

  |-------
{1}   FORALL (x, y: real): x = y => (x = y OR x < y)

から始まりますし,高階なので

p,q:var [[real,real]->bool]
f2:lemma p(x, y) => (p(x, y) or q(x, y))

でも

f2 :  

  |-------
{1}   FORALL (p, q: [[real, real] -> bool], x, y: real):
        p(x, y) => (p(x, y) OR q(x, y))

から始まります.

また,立場3と同じく,変数への個体割り当てを用いない方法として,言語を拡張し

立場4 新たな定数を導入,変数に代入して,閉じさせる

という,自由変数への割り当てを構造の定数の解釈で賄うものもあり,pvs のスコーレム定数はそれと見做すこともできます.

f1 :  

  |-------
{1}   FORALL (x, y: real): x = y => (x = y OR x < y)

Rule? (skolem!)
Skolemizing,
this simplifies to: 
f1 :  

  |-------
{1}   x!1 = y!1 => (x!1 = y!1 OR x!1 < y!1)
f2 :  

  |-------
{1}   FORALL (p, q: [[real, real] -> bool], x, y: real):
        p(x, y) => (p(x, y) OR q(x, y))

Rule? (skolem!)
Skolemizing,
this simplifies to: 
f2 :  

  |-------
{1}   p!1(x!1, y!1) => (p!1(x!1, y!1) OR q!1(x!1, y!1))

なお,Shoenfield辺りでは,解釈が各個体となる新たな定数(いわゆる名前name)を導入,代入して,その任意のインスタンスが真となることを恒真としていますが...