[拼音]：gaojie luoji

[外文]：higher-order logic

又称广义谓词逻辑。它是一阶逻辑（见一阶理论及其元逻辑）的推广。在一阶逻辑中，量词只能用于个体变元，即只有个体约束变元，并且只有个体变元能作谓词变元的主目(见谓词逻辑)。这样就限制了一阶逻辑的语言的表达能力。如果去掉一阶逻辑中的上述限制，命题变元和谓词变元也能作约束变元，即受量词约束，并且作谓词变元的主目，以此构造起来的逻辑系统就是高阶逻辑。它包括二阶逻辑、三阶逻辑……以至无穷阶逻辑。

一阶逻辑的一个很自然的推广是二阶逻辑。修改一阶逻辑中与量词有关的形成规则：如果A(α)是合式公式，α是自由变元（个体变元、命题变元或谓词变元），则凬αA(α)和ヨαA(α)是合式公式；同时，确定适当的公理和变形规则，所得到的系统就是一个二阶逻辑（二阶谓词演算）。例如，凬X [F(x)∨塡F(x)]是一阶逻辑中的合式公式，凬F凬x[F(x)∨塡F(x)]就是一个二阶逻辑的合式公式，它表示凬x[F(x)∨塡F(x)]对一切性质 F都成立。二阶逻辑具有比一阶逻辑更强的表达能力。例如，对于数学归纳原则:“如果一公式对数0成立，并且如果它对某一个数成立则对该数的后继也成立，那末这个公式就对所有的（自然）数成立”，就不能在一阶逻辑陈述的算术理论中，用一个公式表达。而在二阶逻辑中，由于有了谓词量词，就可以用一个公式把该数学归纳原则表示为：

凬F[F(0)∧凬x(F(x)→F(x+1))→凬xF(x)]。

进一步推广二阶逻辑，可以构造出三阶逻辑、四阶逻辑等等，而对于每一自然数 n，可以构造 n阶逻辑。三阶逻辑是在二阶逻辑中引进谓词的谓词。在一阶和二阶逻辑中，谓词表示个体的性质或个体间的关系，以个体常元（个体的名字）或个体变元作主目。这样的谓词称为一层谓词；一阶和二阶逻辑中的谓词变元称为一层谓词变元。有的谓词不是表示个体的性质或个体间的关系，而是表示某个谓词的性质或关系。例如，对一个关系 R，我们说 R是对称的，即如果R(x，y)，则R(y，x);或者说是传递的，即如果R(x，y)且R(y，z)，则R(x，z)。而这种对称性、传递性等都是关于关系的性质。用sym(R)、tr(R)表示关系R是对称的、传递的，而sym和tr都以一层谓词作主目。主目中包括一层谓词（谓词变元）的谓词（谓词变元）称为二层的。一个包括二层谓词变元，但二层谓词变元只作为自由变元出现的逻辑系统，就是三阶逻辑。在三阶逻辑中，不但引进二层谓词变元，而且还要区别谓词变元（一层的、二层的）的不同的型。个体变元的型为i;一层谓词变元F(x)的型为(i)，G(x，y)的型为(i，i)；二层谓词sym(R)，其主目R的型为(i，i)，sym的型为［(i，i)］;二层谓词变元H［G(x，y)，i)］的型为［(i，i)，i)］，等等。对三阶逻辑的形成规则，不但要考虑到新增加的二层谓词变元，还要根据谓词变元的型的区分，对二阶逻辑的形成规则加以修改，并确定适当的公理和变形规则。如果修改三阶逻辑的形成规则，而且允许二层谓词变元也作约束变元，并且确定适当的公理和变形规则，就得到四阶逻辑。类似地，还可以引入三层谓词变元、四层谓词变元等，构造五阶逻辑、六阶逻辑，等等。这样，就可以构造出所有有穷阶逻辑。简单类型论就是ω阶逻辑，它是把所有有穷阶逻辑总汇在一起的系统。简单类型论的公理，除了有一阶逻辑、二阶逻辑等的公理外，还包括另外两条公理，即外延公理和选择公理。这两条公理与公理 论中的外延公理和选择公理相当。

一阶逻辑具有完全性，即系统中的普遍有效的公式都是系统中可证明的。这是一阶逻辑的一个重要特征。此外，一阶逻辑还有两个重要的定理，即紧致性定理和勒文海姆-司寇伦定理（见司寇伦定理）。一阶逻辑还有一个区别于高阶逻辑的重要性质，即一阶逻辑是在运算塡，∧，ョ下封闭的唯一能够满足紧致性定理和勒文海姆-司寇伦定理的逻辑。 虽然一阶逻辑的表达能力是受限制的，但也已很强了，特别是有了公理 论以后，用一阶逻辑的语言可以陈述当今数学的全部分支。因此，有许多逻辑学家认为，除一阶逻辑而外无需研讨高阶逻辑。然而，用一阶逻辑陈述许多相当简单的定义和证明显得十分复杂，而通过高阶逻辑陈述这些定义和证明则要简单得多。尽管通过 论可以把高阶逻辑归纳到一阶逻辑，但却造成定义和证明的大大复杂化。高阶逻辑的表达力和易推导性比一阶逻辑强有力得多。因此，在数理逻辑中高阶逻辑仍是有生命力的。

高阶逻辑的一个重大不足是没有完全性，它的任何公理系统，都不能证明系统中的全部普遍有效公式。

严正声明：本文由历史百科网注册或游客用户和韵自行上传发布关于» 高阶逻辑的内容，本站只提供存储，展示，不对用户发布信息内容的原创度和真实性等负责。请读者自行斟酌。同时如内容侵犯您的版权或其他权益，请留言并加以说明。站长审查之后若情况属实会及时为您删除。同时遵循 CC 4.0 BY-SA 版权协议，尊重和保护作者的劳动成果，转载请标明出处链接和本声明内容：作者：和韵；本文链接：https://www.freedefine.cn/wenzhan/38020.html