Hilbertのε計算
$ \varepsilon x. F\lbrack x \rbrackとは「$ F\lbrack x \rbrackを満たす対象」を指す
ない場合は適当な対象を指す
$ Q \lbrack \varepsilon x. F \lbrack x \rbrack \rbrackは「$ P\lbrack x \rbrackを満たす対象はQを満たす」ことを主張している
1. $ \exists x. F\lbrack x \rbrack \iff F \lbrack \varepsilon x. F \lbrack x \rbrack
$ \Leftarrowは存在汎化
2. $ \forall x. F\lbrack x \rbrack \iff F \lbrack \varepsilon x. \lnot F \lbrack x \rbrack
$ \Rightarrowはε計算の公理:主要論理式 任意の項$ tに対して$ F\lbrack t \rbrack \to F \lbrack \varepsilon x. F \lbrack x \rbrack