海廷，A．

【生卒】：1898～1980

【介绍】：

荷兰数学家、逻辑学家。毕业于阿姆斯特丹大学。数理逻辑和数学基础中直觉主义学派创始人L．E．J．布劳维尔的学生，直觉主义数学和逻辑的积极倡导者和传播者。1930年，发表《直觉主义逻辑的形式规则》和《直觉主义数学的形式规则》两篇论文，详细论述了布劳维尔的直觉主义数学，并建立了第一个完整的直觉主义逻辑系统。海廷的系统被公认为正确地形式化了布劳维尔的想法，也为布劳维尔本人所接受，因此作为对现时用于直觉主义数学中的逻辑原理的正确纲要，这一系统值得我们仔细研究。海廷系统由下列公理模式和推理规则组成：

A→(B→A)，

(A→B)→((A→(B→C))→(A→C))，

A∧B→A，A∧B→B，A→(B→A∧B)，

A→A∨B，B→A∨B，

(A→C)→((B→C)→(A∨B→C))，

(A→B)→((A→B)→A)

A(t)→xA(x)

xA(x)→A(t)｝这里，t对x可代入；

从A和A→B可推出B；

从A(x)→B可推出xA(x)→B；

从B→A(x)可推出B→xA(x)；

后面两个规则中的x都不得在B中自由出现。从这系统中除去有关量词的公理模式和推理规则，就得海廷的命题逻辑系统。附加排中律A∨A或者双重否定律A→A到海廷的系统中，就可得到古典逻辑系统。海廷系统中的4个联结词和2个量词都是初始概念，是相互独立的。关于它们的意义，海廷于1931年提出了一种解释——证明解释，有力地推动了直觉主义逻辑的发展。他的主要论著还有《直觉主义导论》(1956)等。