高阶逻辑

一阶逻辑的推广系统，又称广义谓词逻辑。在一阶逻辑中，量词只能加于个体变元上，即只有个体约束变元，并且只有个体词能作谓词的变目。这样就限制了一阶逻辑的语言表达能力。一阶逻辑的表达能力还有其它方面的限制。为了提高逻辑系统的表达能力，就提出了对一阶逻辑予以推广的要求。

可以从不同方面、沿不同方向推广一阶逻辑。一阶逻辑的一个很自然而又简单的推广是二阶逻辑。这就是取消量词只约束个体变元的限制。修改一阶逻辑中与量词有关的形成规则：如果A是合式公式，α是自由变元(个体变元、命题变元或谓词变元)，则αA和aA是合式公式；同时确定适当的公理和推演规则(与一阶逻辑中的相仿，不过有关量词的公理推广为以谓词变元作约束变元)，所得到的系统就是一个二阶逻辑(二阶谓词演算)。例如，x(F(x)∨F(x))是一阶逻辑的合式公式，Fx(F(x)∨F(x))就是二阶逻辑的合式公式，它表示x(F(x)∨F(x))对一切性质F成立，是二阶逻辑的一个定理。二阶逻辑具有更强的表达能力。在一阶逻辑中无法定义“等于”这个谓词。在二阶逻辑中，就可以用公式F(F(x)F(y))来定义x=y。公式xy(x=yF(F(x)F(y)))是二阶逻辑的定理，它表示，对于所有x，y，x=y当且仅当F(F(x)F(y))，所以就可用F(F(x)F(y))作为x=y的定义。又如，用一阶语言，不能用一公式表达数学归纳原则：如果数0有某一性质，并且如果某个数有此性质则该数的后继也有此性质，那么就所有自然数都有这个性质。在二阶逻辑中，由于有谓词量词，就能用一个公式表达数学归纳原则：F(F(0)∧x(F(x)→F(x+1))→xF(x))。

进一步推广二阶逻辑，就可以得到更高阶的逻辑。在一阶逻辑中有公式xy(R(x，y)→R(y，x))，它表示关系R是对称的。公式xyz(R(x，y)∧R(y，z)→R(x，z))表示关系R是传递的。对称性、传递性等都是关于关系的性质，是以谓词为主目的谓词。用sym(R)、tr(R)表示R是对称的和R是传递的，sym和tr都是以谓词为主目的谓词。以个体词为主目的谓词称为一阶的，以一阶谓词为主目的谓词称为二阶的。sym和tr都是以一阶二元谓词为主目的二阶谓词。在二阶逻辑中增加二阶谓词后，就是三阶逻辑。如果再允许以二阶谓词变元作约束变元，就是四阶逻辑。一般地，以n阶谓词为主目的谓词便是n+1阶谓词。应用概括原则，从含有至多为n阶的自由谓词变元的公式便可抽象出来n+1阶谓词。这样便可以逐步构造出更高阶的逻辑。依照A．丘奇的划分，如果一个系统中的最高阶谓词为n阶，而n阶谓词都是自由的，便是2n1阶逻辑；最高阶的n阶谓词有约束的，便是2n阶逻辑。所有有穷阶逻辑的并便叫做ω阶逻辑。在构造高阶逻辑时，不仅需要区分谓词的阶，还要区分谓词的型。个体词的型为i，一阶一元谓词F(x)的型为(i)，二元谓词G(x，y)的型为(i，i)；二阶谓词sym(R)，其主目R的型为(i，i)，sym的型为((i，i))，二阶谓词H(G(x，y)，F(x))的型为((i，i)，(i))，等等。这样，一个谓词的空位究竟应该填以什么东西，就由它的型决定，填以不符合它的型的东西，就不是合式公式。如sym(x)不是合式公式。由一个谓词的空位中可以填入的东西的全体组成的集合叫做该谓词的定义域。一阶谓词的定义域必须是某个个体域，而n阶谓词的定义域必须是由较低阶谓词(必须包括n－1阶的)及个体组成的集合。一个高阶谓词(譬如n+1阶谓词)，哪个空位必须填以n阶谓词，哪个空位必须填以较低阶谓词甚至个体词都有明确规定。所以在高阶逻辑中可以无条件地使用概括原则而不会产生逻辑悖论。

ω阶逻辑称为简单类型论。它的关于量词的公理，和一阶逻辑的形式类似，如关于全称量词有公理模式：GF(G)→F(H)，其中若G，H为n阶的，F便为n+1阶的。此外，还有无穷公理、外延公理和选择公理。类型论是罗素为消除悖论而又要从它推出数学而建立的系统，因此包括无穷公理和选择公理这两个非逻辑公理。

二阶逻辑是协调的，但不是完全的。二阶逻辑的常真公式分为主要常真公式和次要常真公式。只有次要常真公式都是在二阶逻辑中可证的，但是没有一切主要常真公式都在其中可证的二阶逻辑公理系统。不包括无穷公理的简单类型论的协调性是可证明的。对于包括无穷公理的简单类型论，假设它是协调的，那么它的协调性在系统自身之中是不可证明的。

一阶逻辑具有完全性、紧致性和勒文海姆－司寇伦性质，高阶逻辑都不具备这些性质。也就是说，在高阶逻辑中，完全性定理、紧致性定理和勒文海姆-司寇伦定理不成立。有一个定理刻划了一阶逻辑区别于其它逻辑(不仅高阶逻辑，还包括沿其它方向推广一阶逻辑而得的系统)的特征：一阶逻辑是在运算，∧，∨下封闭的唯一能够满足紧致性定理和勒文海姆－司寇伦定理的逻辑。一阶逻辑是很重要也是最基本的逻辑，具有完全性，紧致性这样重要的性质；特别是，虽然它的表达能力受限制，但有了公理集合论后，用一阶语言可以陈述当今各个数学分支。因此，有的逻辑学家持一种可以称为一阶论题的主张：逻辑就是一阶逻辑。按照他们的主张，高阶逻辑不算是逻辑。但是，高阶逻辑虽没有完全性等重要性质，可它除了比一阶逻辑表达能力强外，还有其它的优点。用一阶逻辑来陈述许多相当简单的定义和证明，显得十分复杂，而用高阶逻辑陈述就要简单得多，并且在n+1阶逻辑中可以证明原来在n阶逻辑中不能证出的定理，因此研究高阶逻辑是有意义的，高阶逻辑是有生命力的。