谓词逻辑分一阶逻辑和高阶逻辑,当年罗素悖论刚被提出时,数学家们为了解决悖论给出两套方案,一套方案是采取公理化集合论,不让量词作高阶使用,即一阶逻辑;另一套方案是采取罗素本人提出的类型论,即高阶逻辑。多数数学理论采取的第一种理论作为数学基础,主要是因为部分重要的元定理对高阶逻辑不成立,加上高阶逻辑没有一个普适的演绎系统,1940年代高阶逻辑即集合论这一事实也逐渐被人认识到,而集合论的公理系统又是一阶的,最终确立了一阶逻辑的优势地位。高阶逻辑选这本书可以初步了解——
一阶逻辑使用的演绎系统,分自然演绎系统和公理系统,前者多见于哲学系本科教材和计算机系离散数学教材,后者多见于数理逻辑教材。自然演绎系统最初由格哈德·根岑在1934年提出,是在公理系统的基础上发展而来的,因为自然演绎系统的18项基本推理规则都可以在公理系统中得到证明,后续又加入了量词规则形成量化自然演绎。量化自然演绎分为不带标记的和带标记的系统,上面提到的那本书用的是不带标记的系统,而下面这本讲的是带标记的系统,相对上面那本简单一些——
公理系统相对自然演绎系统规则较少,但推理起来难度更大,哲学系教材多采用命题系统P扩张后形成的一阶系统G,而计算机系教材多采取命题系统L扩张形成的系统K,相比之下前者在证明一些内定理上更方便,而且哲学系的教材更通俗易懂一些。