为什么使用构造逻辑而不是排中律？

基于类型的逻辑让我们使用构造逻辑constructive logic而不是经典逻辑，而且以这样一种奇怪扭曲的方式否定排中律，为什么我们要这么做？

有一些理由，首先，构造逻辑其实不奇怪，只要你以它的方式思考，在经典逻辑中，排中律是“对于任何语句P，要么P是真，要么是假”，听起来很显然，但是在构造逻辑中，最好将这个法则叙述为：“对于任何语句P，要么我具备P的证明，要么我具备P的反证”，现在哪个是明显错误的呢？

我并不是无所不知，即使我是，我们也知道应该有一个语句，既不能可被证明，也不能被反证。

但是我们是要谈论的是可证明而不是真理，有很多理由，其中一个主要是：真理对于计算是无用的，而证明则不是，构成主义思想比经典逻辑更加严密，一个构成的证明比非构成的经典逻辑会包含很多可用来分析的信息，在计算科学中，我们都是构成逻辑的特别粉丝，因为一些规定实现对于构成证明来说是这样：存在一段程序满足那条规定约束。

通常，你也会通过构造证明来很多解决头脑中哪些是"可用的可实现的"想法，但是如果你有一个证明是经典逻辑范围内有效，而不是构造逻辑，那么它不能告诉你任何是否可用可实现的判断。所以，构造性证明是更靠近实践。(banq注：实践是检验真理唯一标准 这句话已经不重要，重要的是我们的真理要更靠近实践，否则无用，也无需等待实践检验，也肯定等不到检验，只能蒙混下去)。

构造逻辑对于我们知识如何工作是很好的模型，一个命题可以是真或假，但是我们不会知道它是真，除非我们有一个证明，排中律则是从一个旁观者角度观察和俯瞰数学的柏拉图王国(从数学外部观看)，而从里面我们不能看到任何纯洁如水晶的真理，一个语句“要么是真，要么是假”对于我们很少有用。(banq注：实际中没有如排中律那么明显真假，常常似是而非，排中律武端认为要么是真要么是假的黑背分明思维对实践毫无用处)

[该贴被banq于2015-01-05 08:25修改过]