| 甘岑 Gerhard Gentzen1909—1945 德国数学家、逻辑学家。希尔伯特学派的重要成员。毕业于格廷根大学。在1934年所作并在1935年发表的就职演说论文《关于逻辑推论的研究》中，提出了第一个自然演绎系统N，该系统共有十二条用图式表达的关于逻辑联结词和量词引进、消去的推理规则。还提出了和N相关的L系统，并证明：L系统中的任一证明，都可变为一个相应的范式，这种范式需要一种称之为“切割”(Schnitt)的运算。这就是他所谓的“主定理”(Hauptsatz)。认为，虽然“断”的运算在表明L与N系统等价时是决定性的，但它能在L系统的任何证明中删去。“主定理”使正确公式的证明结构简单化，产生了L系统部分命题的判定程序，这一理论大大推进了自足演算中证明的确立。还进一步把“主定理”用于算术系统的一致性证明。1936年证明借助超穷归纳法，可以证明自然数算术形式系统的一致性。其后几年，与其他人又给出了别的证明。他的研究成果代表了第二次世界大战结束前证明论的最高成就。主要著作还有《层次逻辑的无矛盾性》(1936)、《纯数论的无矛盾性》(1936)等。 |