Cookie Policy Terms and Conditions >
一阶逻辑的公式是Skolem 范式的,如果它的前束范式只有全称量词。一个公式可以被Skolem 化,就是说消除它的存在量词并生成最初的公式的等价可满足的公式。Skolem 化是如下(二阶的)等价的应用
Skolem 化的本质是对如下形式的公式的观察
它在某个模型中是可满足的,在这个模型必定有某些点对于所有的
使得
为真,并且必定存在某个函数(选择函数)
使得公式
为真。函数 f 叫做 Skolem 函数。
页面分类: 逻辑学小作品 | 模型论