一阶逻辑 -- 来自 Wolfram MathWorld

一阶逻辑（也称为一阶谓词演算）的项的集合由以下规则定义

1. 变量是一个项。

2. 如果是一个元函数符号（其中），且 , ..., 是项，则是一个项。

如果是一个元谓词符号（同样，其中），且 , ..., 是项，则是一个原子语句。

考虑语句公式和，其中是一个语句公式，是全称量词（“对于所有”），而是存在量词（“存在存在”）。称为相应量词的作用域，并且变量在量词作用域内的任何出现都由最接近的或约束。变量在公式中是自由的，如果在中的至少一次出现没有被内的任何量词约束。

一阶谓词演算的语句公式的集合由以下规则定义

2. 如果和是语句公式，则（非），（与），（或），以及（蕴含）是语句公式（参见命题演算）。

3. 如果是一个语句公式，其中是一个自由变量，则和是语句公式。

在一阶谓词演算的公式中，所有变量都是对象变量，充当函数和谓词的参数。（在二阶谓词演算中，变量可以表示谓词，并且量词可以应用于表示谓词的变量。）一阶谓词演算的公理模式的集合由命题演算的公理模式以及以下两个公理模式组成

	(1)
	(2)

其中是任何语句公式，其中自由出现，是一个项，是用替换语句公式中的自由出现的结果，并且中所有变量的所有出现都在中自由。

一阶谓词演算中的推理规则是肯定前件和以下两个规则

	(3)
	(4)

其中是任何语句公式，其中以自由变量的形式出现，不以自由变量的形式出现在公式中，并且该符号表示如果线上方的公式是通过应用推理规则从公理中正式推导出的定理，则线下方的语句公式也是一个正式定理。

与命题演算类似，和的引入和消除规则可以在一阶谓词演算中导出。例如，以下规则成立，前提是是用变量替换语句公式中的自由出现的结果，并且由此替换产生的的所有出现都在中自由，

(5)

哥德尔完备性定理确立了一阶谓词演算的有效公式与一阶谓词演算的形式定理之间的等价性。与命题演算相比，真值表的使用不适用于在一阶谓词演算中查找有效的语句公式，因为它的真值表是无限的。然而，哥德尔完备性定理为确定有效性开辟了一条道路，即通过证明。

一阶逻辑