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

15-01-04 banq
                   

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

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

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

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

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

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

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

                   

2
banq
2015-01-05 08:31

2015-01-04 13:59 "@banq"的内容
排中律则是从一个旁观者角度观察和俯瞰数学的柏拉图王国(从数学外部观看) ...

当我们看到有人喜欢轻易下结论时,大概可以推测他是使用排中律,他只是从旁观者角度看待领域内的事物,如果是真正领域专家,从来不轻易下结论,因为了解实际情况后,事情远非要么真要么假那么简单。

“凡是敌人反对的,我们坚决拥护”等也是一种排中律,只要是敌人反对的肯定是我们支持拥护的,这里面隐含了武端的真假设定在其中。

构造逻辑与构造定律提供了我们构造世界的两个支撑,当我们使用基于构造逻辑的类型系统开始编程第一步以后,构造定律(加法规则)开始显露,两种构造方式交织在我们创建软件世界的过程中。