构造逻辑

　　构造逻辑（constructive logic），一种非经典的逻辑系统。它主要由对数学持直觉主义、构造主义或致力于构造性数学研究和发展的数学家和逻辑学家建立和使用。在数理逻辑和数学基础中，“构造性”一词有几种不同的理解并在几种不同的意义下使用，其共同之处在于它们都满足下列构造性要求：①对存在命题ƎxAx的一个证明是构造性的，如果从这个证明能找到（构造出）一个特殊的对象x，它满足A。②不能无条件地使用排中律。按照构造性观点，对于p∨p，只有在有一个方法能判明p与p中哪一个是真的情况下，才能承认它是真的，而不承认任一命题非真即假。按照这些构造性观点建立的逻辑就是构造逻辑。

　　在构造逻辑中，对于逻辑联结词(非）、∧(并且）、∨(或者)、→(如果，则，)和量词Ǝx(存在一个x，有一个x)、"x(所有x）的理解如下：①对A∧B的一个证明由A的一个证明和B的一个证明一起构成。②对A∨B的一个证明由特别指定的A的一个证明或者由特别指定的B的一个证明构成。③对A→B的一个证明由一个构造c构成，构造c可把A的任一证明转换成B的一个证明，即构造c具有如果d是A的一个证明，把c与d结合起来就产生B的一个证明这种性质。④以符号⊥表示一个不可证的命题，对A的一个证明由一个构造c构成，构造c把对A的任一证明转换成对⊥的一个证明。⑤如果个体变元x取值于某个基本的个体域D，则对"xA(x)的一个证明由一个构造c组成，当把构造c应用于域D中的任一个体d时，就产生对A(d）的一个证明c(d)。⑥如果个体变元x取值于某个基本的个体域D，则对ƎxA(x）的一个证明由一个构造c和域D中的一个个体d构成，并且构造c是对A(d）的一个证明。

　　在构造逻辑中，各个联结词和量词都是彼此独立、不能相互定义的。