补充资料：高阶逻辑

    　　又称广义谓词逻辑。它是一阶逻辑（见一阶理论及其元逻辑）的推广。在一阶逻辑中，量词只能用于个体变元，即只有个体约束变元，并且只有个体变元能作谓词变元的主目(见谓词逻辑)。这样就限制了一阶逻辑的语言的表达能力。如果去掉一阶逻辑中的上述限制，命题变元和谓词变元也能作约束变元，即受量词约束，并且作谓词变元的主目，以此构造起来的逻辑系统就是高阶逻辑。它包括二阶逻辑、三阶逻辑......以至无穷阶逻辑。
　　
　　二阶逻辑 　一阶逻辑的一个很自然的推广是二阶逻辑。修改一阶逻辑中与量词有关的形成规则：如果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)］,等等。对三阶逻辑的形成规则，不但要考虑到新增加的二层谓词变元，还要根据谓词变元的型的区分，对二阶逻辑的形成规则加以修改，并确定适当的公理和变形规则。如果修改三阶逻辑的形成规则，而且允许二层谓词变元也作约束变元，并且确定适当的公理和变形规则,就得到四阶逻辑。类似地,还可以引入三层谓词变元、四层谓词变元等，构造五阶逻辑、六阶逻辑，等等。这样，就可以构造出所有有穷阶逻辑。简单类型论就是ω阶逻辑，它是把所有有穷阶逻辑总汇在一起的系统。简单类型论的公理，除了有一阶逻辑、二阶逻辑等的公理外，还包括另外两条公理，即外延公理和选择公理。这两条公理与公理集合论中的外延公理和选择公理相当。
　　
　　一阶逻辑与高阶逻辑 　一阶逻辑具有完全性，即系统中的普遍有效的公式都是系统中可证明的。这是一阶逻辑的一个重要特征。此外，一阶逻辑还有两个重要的定理,即紧致性定理和勒文海姆-司寇伦定理（见司寇伦定理）。一阶逻辑还有一个区别于高阶逻辑的重要性质，即一阶逻辑是在运算塡,∧,ョ下封闭的唯一能够满足紧致性定理和勒文海姆-司寇伦定理的逻辑。 虽然一阶逻辑的表达能力是受限制的，但也已很强了，特别是有了公理集合论以后，用一阶逻辑的语言可以陈述当今数学的全部分支。因此，有许多逻辑学家认为，除一阶逻辑而外无需研讨高阶逻辑。然而，用一阶逻辑陈述许多相当简单的定义和证明显得十分复杂，而通过高阶逻辑陈述这些定义和证明则要简单得多。尽管通过集合论可以把高阶逻辑归纳到一阶逻辑，但却造成定义和证明的大大复杂化。高阶逻辑的表达力和易推导性比一阶逻辑强有力得多。因此，在数理逻辑中高阶逻辑仍是有生命力的。
　　
　　高阶逻辑的一个重大不足是没有完全性，它的任何公理系统，都不能证明系统中的全部普遍有效公式。
　　

说明：补充资料仅用于学习参考，请勿用于其它任何用途。