记录一下防止遗忘，不一定精准。

可判定性

可判定性用于描述某个问题是否能在有限的时间内被某个算法解决。图灵停机问题被证明为不可判定的，命题逻辑的可满足性问题是可判定的，而一阶逻辑公式的有效性、可满足性和蕴含问题是半可判定的。

一阶逻辑相关概念

模型

模型是语义相关的概念，模型可简单理解为赋予一阶逻辑公式中谓词、函数和常量含义。脱离模型这个概念去谈一阶谓词公式的真值是没有意义的。这一点与命题逻辑不同，因为命题逻辑中没有谓词。

可满足性和有效性

命题逻辑的可满足性问题是指判断是否存在一组赋值使得命题逻辑公式为真。一阶逻辑的可满足性问题是指判断是否存在一个模型使得一阶谓词逻辑公式为真。
在命题逻辑中，如果所有赋值均使公式为真，那么称该公式是有效的。在一阶逻辑中，如果一个公式在所有的模型下均为真，称该公式是有效的。

一阶逻辑的可靠性和完备性

可靠性和完备性保证了一阶逻辑语法和语义等价，即通过推理（语法层面）得到新的公式一定在给定模型下是真的（语义层面）。
在一阶逻辑中，通过利用推理规则去得到新的公式是相对简单的，但是通过推理规则去证明某个公式不被语法蕴含是困难的。但是语义层面正好相反，证明一个公式不被语义蕴含是相对简单的（找到一个模型即可），但是证明一个公式被语义蕴含则是困难的（要验证所有的模型）。
可靠性和完备性为我们提供了语法和语义的桥梁。

一阶逻辑的半可判定性

一阶逻辑的蕴含是半可判定的，即当某个公式bb被公式aa蕴含时，通过一系列的推理规则在有限的时间内一定能从aa得到bb；这是由于对于任意有效的公式P，P是可被证明的。然而，当某个公式bb不被公式aa蕴含时，这个过程可能永远无法中止。由前所述，证明某个公式不被另一个公式蕴含从语义层面上证明是相对容易的，由于可靠性和完备性，我们可以从语法层面转化到语义层面来证明一个公式不被另一个公式蕴含。直观来讲这一过程很容易，只要找到一个模型就可以了，为什么程序可能永远不会停止呢？
思考偏序关系这个例子，它表述的是在偏序关系中对所有元素来说总存在一个“更大”的元素：

∀x∀y∀z(R(x,y)∧R(y,z)→R(x,z))∧∀x¬R(x,x)∧∀x∃yR(x,y)\forall x \forall y \forall z(R(x,y)\land R(y,z) \to R(x,z))\land \forall x \neg R(x,x) \land \forall x \exist y R(x,y)

其中RR代表偏序关系。离散数学的知识告诉我们这个公式是可满足的（考虑实数论域的情况），但是在论域有限的情况下我们找不到可以令该公式满足的模型。然而机器只能在有限的论域中进行搜索，因此虽然这个公式可满足，但是在有限时间内计算机却不能找到一个模型去证明其可满足性。考虑这个公式的否定，由于其是可满足的，因此其否定一定是非有效的，这也说明在公式非有效的情况下，计算机不一定能在有限的时间内判断它是否真的非有效。
当然，这并不意味着所有非有效的公式都不能在有限时间内被判断，如

∀xP(x)\forall x P(x)

计算机很容易在有限时间内找到一个模型从而证明其非有效。
综上，由一阶逻辑的完备性和可靠性，一阶逻辑中的有效性、可满足性和蕴含关系都是半可判定的。