构造性逻辑

数理逻辑的一个分支，是各种构造性数学用的一种非经典逻辑。不同的构造性数学派别采用的逻辑系统稍有不同。但对纯逻辑系统(命题演算、谓词演算)，术语“构造性的”和“直觉主义的”常被看作是同义的，直觉主义逻辑是构造性逻辑的典型系统，别的构造性数学派别没有建立像直觉主义逻辑这样的逻辑系统，只是在他们的数学中不采用直觉主义的某个原则(如E．毕肖普的《构造分析基础》不用直觉主义的选择序列)，或应用某个其它的原则(如前苏联的构造性递归分析学派的马尔科夫原则)。构造性数学与经典数学的一个明显区别表现在对存在命题的证明的态度上。xA(x)的一个证明是构造性的，如果从这证明能找到一个特定的客体x(系统中的项)满足A。下面这个定理的证明则是非构造性的。

定理 存在两个无理数a和b，使得a是有理数。

证明 或者是有理数或者是无理数。如果是有理数，取a=b=即满足定理。如果是无理数，取a=，b=，=2即满足定理。

上述证明在经典数学中完全成立，构造性数学则不承认这已证明定理。因为证明中没有证明(或给出一个方法能判明)是有理数还是无理数。在上述证明中，排中律起重要作用。构造性逻辑不承认排中律是普遍有效的逻辑规律。在构造性逻辑中没有排中律p∨p，和双重否定律p→p。构造性逻辑与经典逻辑不同的另一重要特点是对联结词∨(或者)的解释。根据对∨的构造性解释，如果┝p∨q，则┝p或者┝q。这在经典逻辑中不成立。

大多数构造性逻辑系统，相对于不同的可实现概念，包括克里尼的可实现和哥德尔解释，是正确的；一切可证的公式在构造性语义中可实现。另一方面，构造性逻辑的形式系统相对于自然的构造性语义常常是不完全的。对于包括算术在内的系统，这可从哥德尔不完全性定理得出。对直觉主义逻辑已证明了完全性定理：相对贝思模型和克里普克模型是完全的，相对于代数模型和拓扑模型也是完全的。

经典逻辑形式系统往往借助印相片式的翻译，即在一切子公式前面加上双重否定而嵌入相应的构造性逻辑系统(保持从假设可推演性关系)。因此建立在经典逻辑基础上算术系统同构地嵌入建立在构造性逻辑基础上的系统中。因此可得出经典算术系统的相对协调性。在有的构造性逻辑系统中正确的命题，如排中律的否定，在经典的解释下是假的。这样的系统S可借助适当的可实现性概念p归结到经典的系统S。证明，如果S┝A，则存在t，S┝tpA；并且如果A是数字等式，则S┝A→tpA。由此得出S相对于S的协调性。构造性逻辑系统S可以在无量词的系统S中得到解释：公式xyR(x，y)，其中R无量词，在S中可证，则对初始函数φ，公式R(x，φ(x))在S中可证。如果S是无归纳原则的算术，则S是原始递归算术；如果S是海廷算术，则S是哥德尔原始归泛函系统。