Empty domain
古典的(?)な一階の古典論理の意味論では,ドメインAは空でないとされ,その理由として,Aが空では,∀x.p(x),つまり「任意のxについて,x∈Aならばp(x)」が真,∃x.p(x)つまり「あるxについて,x∈Aかつp(x)」が偽,したがって,定理式
∀x.p(x)→∃x.p(x)
が偽となることが挙げられます.
一方,PVSでのドメインの宣言には
A:TYPE
と
A:TYPE+ 略さないなら A:NONEMPTY_TYPE
とがあり前者はAが空でも構いません.その場合,健全性を破棄しない以上,上記の含意は証明できない筈であり,実際
A:TYPE x,y:var A p:[A->bool]
としても
f01 : |------- {1} (FORALL (x): p(x)) => (EXISTS (x): p(x)) Rule? (flatten) Applying disjunctive simplification to flatten sequent, this simplifies to: f01 : {-1} (FORALL (x): p(x)) |------- {1} (EXISTS (x): p(x)) Rule? (inst - "y" ) The supplied terms should not contain free variables. The following irrelevant free variables occur in the terms: (y) No change on: (inst - "y")
のように弾かれます.つまり,instantiate できるのは,宣言済みのドメインに属する定数,または,例えば
q:[A->bool]
とした上での
f02 : |------- {1} ((EXISTS (x): q(x)) AND (FORALL (x): p(x))) => (EXISTS (x): p(x)) Rule? (flatten) Applying disjunctive simplification to flatten sequent, this simplifies to: f02 : {-1} (EXISTS (x): q(x)) {-2} (FORALL (x): p(x)) |------- {1} (EXISTS (x): p(x)) Rule? (skosimp*) Repeatedly Skolemizing and flattening, this simplifies to: f02 : {-1} q(x!1) [-2] (FORALL (x): p(x)) |------- [1] (EXISTS (x): p(x)) Rule? (inst - "x!1" ) Instantiating the top quantifier in - with the terms: x!1, this simplifies to: f02 : [-1] q(x!1) {-2} p(x!1) |------- [1] (EXISTS (x): p(x)) Rule? (inst + "x!1" ) Instantiating the top quantifier in + with the terms: x!1, Q.E.D.
のようなスコーレム定数から構成された,いわゆる「閉項」のみという訳です.これは,代入する項に既に式内で量化されている変数が含まれている可能性を排したもので,例えば「∀x. ∃y. p(x, y) の x を y に inst して,∃y. p(y, y) を得る」といった事態を回避できます.
HOL Light だと,この辺りは,普通に
# g `(!x:A. ?y:A. p x y) ==> q` ;; Warning: Free variables in goal: p, q val it : goalstack = 1 subgoal (1 total) `(!x. ?y. p x y) ==> q` # e( STRIP_TAC );; val it : goalstack = 1 subgoal (1 total) 0 [`!x. ?y. p x y`] `q` # e( FIRST_X_ASSUM (ASSUME_TAC o (SPEC `y:A`) ) );; val it : goalstack = 1 subgoal (1 total) 0 [`?y'. p y y'`] `q`
と束縛変数が逃げてくれます(α変換ではなく,最初から,束縛変数と自由変数を使い分けるのが穏健ですが).