「開いた式」

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

言語，構造を固定した上で，伝統的（？）なのは，変数への個体割り当てを用いて

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

立場２　割り当て毎には充足性（＝立場１での真偽）を与え，任意の割り当てが充足する式に真を与える（ただし，偽は否定した式が真のこととするので，その式も否定も真とならないことがある）

というものです．

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

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

のが簡明です．

というわけで，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))

から始まります．

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

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

という，自由変数への割り当てを構造の定数の解釈で賄うものもあり，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）を導入，代入して，その任意のインスタンスが真となることを恒真としていますが．．．