甘岑后继式演算系统与其自然演绎系统的比较

董文媛



甘岑后继式演算系统与其自然演绎系统的比较

董文媛

（山西农业大学信息学院创意写作中心，山西 太谷030800）

《逻辑演绎研究》“（Untersuchungen über das Logische Schliessen”）是甘岑提交哥廷根大学的就职论文，文中甘岑提出了两种逻辑演算系统，即“自然演绎”和“后继式演算”系统。从自然演绎开始甘岑尝试构造一个接近数学实际推理的逻辑演算，而后针对自然演绎系统的不足进行了转化和改进，构造了后继式演算系统，并证明了该逻辑演算系统的合理性。甘岑的逻辑演绎思想在逻辑史上具有十分重要的地位，对现代逻辑和证明论的发展具有深远的影响。

自然演绎；后继式演算；逻辑演算系统

1　甘岑后继式演算系统

1.1从“自然演绎”到“后继式演算”

继希尔伯特和阿克曼的《数理逻辑基础》之后，甘岑（Gerhard Gentzen 1909-1945）于1934-1935年分两部分发表的论文《逻辑演绎研究》（“Untersuchungen über das Logische Schliessen”英译为“Investigations into logical deduction”）中提出了“自然演绎”（Natural deduction）的概念。哥德尔在不完全定理证明之后，进一步提出了数论一致性的不可证问题，甘岑则以构造数论的一致性证明为目标，将逻辑演绎的形式化作为出发点进行尝试。他认为弗雷格、罗素和希尔伯特的形式系统远离了数学证明中实际使用的演绎形式，因此为了使形式证明尽可能地接近自然的、实际的推理，使结论独立于假设成为“纯逻辑”的证明，并且达到可观的形式上的优越性，构造了自然演绎系统。［1］288自然演绎是一种证明演算，在这种逻辑演算中，不同于公理系统演算包含公理和推理规则，自然演绎系统是只包含推理规则，更加接近自然的实际推理。……