ヘンキン性
授業では「ヘンキン理論」と呼んでたもの
存在の主張$ \exist x\psiが証明できるなら、その存在の証拠となる$ tが見つかる
定義
言語$ Lの閉論理式の集合$ \Gammaが次の性質を満たすとき、$ \Gammaは$ Lのヘンキン理論であるという
$ Lの論理式の$ \psiについて、$ \mathrm{FVar}(\psi)=\{x_i\}ならば、
$ \Gamma\vdash(\exist x_i\psi\rightarrow\psi[t/x_i]) をみたす$ Lの閉項$ tが存在する
どういうこっちゃmrsekut.icon
上の定義と同値なもうちょい理解しやすいものは以下
$ \Gamma\vdash\exist x\psi\Rightarrow\Gamma\vdash\psi[t/x]
参考