关于高阶逻辑介绍

[拼音]：gaojie luoji

[外文]：higher order logic

通常的逻辑演算是一阶谓词演算，也叫一阶逻辑。在其中除命题联结词外，所讨论的函词及谓词都只以个体为变目，而量词及摹状词只以个体变元为指导变元(约束变元)。一阶逻辑是很重要的。但它也有不足，它不是自封闭的。虽然一阶逻辑中含有量词符号“凬”、“扽”，又含有谓词、函词变元符A、ƒ，但却没有以谓词变元、函词变元为指导变元的量词。例如当A、B是谓词变元符时，A(x)→B(x)是一阶逻辑的公式，但扽A扽B(A(x)→B(x))却不再是一阶逻辑的公式了。

可以从多方面来推广一阶逻辑。首先是允许量词、摹状词的指导变元既可以为个体变元，又可以为谓词变元及函词变元。这样推广后就得到了通常所说的二阶逻辑。例如，扽A扽B(A(x)→B(x))便是二阶逻辑的公式。

在一阶逻辑中无法定义出“等于”这个谓词。在二阶逻辑中，对于公式“x=y”则可以定义为凬A(A(x)呏A(y))。该式表示:对于任何性质A，A(x)与A(y)或同时成立或同时不成立。由于当且仅当x与y相等时凬A(A(x)呏A(y)成立，所以就可以用凬A(A(x)呏A(y))作为x=y的定义。但是如果省略“凬A”而写成A(x)呏A(y)，那么意思就完全改变了。它只表示：对于所给的性质 A， A(x)与A(y)或同时成立或同时不成立。这就表明用A(x)呏A(y)绝不能定义x=y。所以，二阶逻辑的确强于一阶逻辑。

对于二阶逻辑所使用的公理系统通常与一阶逻辑使用的公理系统相仿。不过有关量词的公理推广到了以谓词变元及函词变元（不再限于仅是个体变元）作为指导变元。但是，这种公理系统是不能够推出二阶逻辑中的一切永真公式（所谓主要永真公式）的，而只能推出其中的一部分（所谓次要永真公式）。已经证明了，主要永真公式是不能公理化的，即不能够做出一个公理系统，使得凡是主要永真公式均可在该系统中推出并且该系统可推出的公式仅为主要永真公式。在二阶逻辑中所讨论的常常是主要永真公式。既然它不能公理化，因此上面所说的二阶逻辑公理系统也就没有一阶逻辑公理系统那么优越了。

如果对含有自由谓词变元，函词变元的公式利用概括原则抽象出一个新谓词。那么这个新谓词就是一个以谓词、函词为变目的二阶谓词。例如，对于含二元谓词R 的公式凬x凬y(R(x，y)→R(y，x)根据概括原则可抽象出一个表示对称性的谓词Sym，即

。

同样，根据公式由概括原则也可抽象出一个表示可传性的谓词tr，可见Sym及tr都是以二元谓词R为变目的二阶谓词。一般地，由含有至高为 n阶的自由谓词变元、函词变元的公式根据概括原则抽象出来的谓词、函词便是 n+1阶谓词、函词。这样可以逐步得到更高阶的谓词及函词，再添入以各阶谓词变元、函词变元为指导变元的量词及摹状词，更高阶的逻辑便也逐步得到了。但要注意，二阶逻辑中只是含有一阶谓词、函词(自由的及约束的)，含二阶谓词、函词的便是更高阶的逻辑了。依照A.丘奇的划分，如果在系统中最高阶的谓词及函词（设为n阶）均是自由的，便叫做2n-1阶逻辑，最高阶（设为n阶）的谓词及函词有为约束的，便叫做2n阶逻辑。

在高阶逻辑中，每个谓词或函词的空位，究竟应该填以什么东西这完全是由谓词或函词本身决定的，由一个谓词（函词）空位中可以填入的东西的全体组成的集合叫做该谓词（函词）的定义域。一阶谓词（函词）的定义域必须是某个个体域，而高阶谓词（函词）的定义域就必须是由较低阶谓词，函词及个体组成的集合。对于一个高阶谓词（譬如n+1阶谓词），哪个空位必须填以n阶谓词、函词，哪个空位必须填以较低阶谓词、函词甚至是个体，都有着明确的规定。因此就不会出现高阶谓词。函词填入较低阶谓词的空位中的现象。所以，在高阶逻辑中就可以无条件地使用概括原则而不致产生悖论。反之，如果把各阶谓词、函词不加区别，组成一个共通的域（无类型的集合域），这便是集合论。在集合论中对概括原则必须加适当的限制，否则就会产生悖论。人们宁肯对概括原则加以一定的限制，而使用无类型的集合论作为数学的基础。因此高阶逻辑就被人们忽略了。

对于高阶谓词及高阶函词的本质还可有另一解释，例如前面提到的 Sym、tr，可以不把它们看成是以谓词为变元的高阶谓词，而把它们看成是具有两个指导变元的约束词。即对于Sym(R)及tr(R)，写成Symx，yR(x，y)，trx，yR(x，y)，其中x、y是Sym及tr的指导变元，R(x，y)是Sym及tr的作用域。Symx，yR(x，y)与trx，yR(x，y)的意思就是说:作为x，y的二元谓词而言，R(x，y)是对称的和可传的。在这里，Sym及tr的作用完全和量词凬，扽的作用一样，其所以具有两个指导变元，只因 R是二元谓词罢了。在这种解释之下，所谓的高阶谓词无非是一些类似于量词的约束词，所谓的高阶函词无非是一些类似于摹状词的约束词，在高阶逻辑中，只是研究由概括原则抽象出的各种约束词的公共特性。鉴于约束词的使用日益频繁，所引进的约束词日益增多，作为研究各种约束词公共特性的高阶逻辑就将会日益显示其重要性。