higher-order prover のこと（１）

「高階論理の定理証明システム」という言葉がよく用いられ，実際，主なプルーフ・アシスタントでは高階論理の定理式が扱えます．しかし，それは関数や述語を変数のまま使えるということであり，高階の decision procedure を備えているという意味ではありません．全称はフリーのままにすれば，所謂，スコーレム化として処理してくれますが，特称やユニファイはビルトインのfirst-order proverには荷が重く，例えば

MESON[]`!y:Y. ?x:X. f x = y ==> ?g. !y. f (g y) = y`;;

lemma "(∀a::real. ∀b::real. f a = f b --> a = b) --> (∃g::real => real. ∀x. g (f x) = x)";
by metis;

などは行ったきりです．