在KS中,A的范围是公式,α的范围是选择序列,选择序列是由创造性主体产生的自然数序列,创造性主体逐一选择其元素。选择序列和克里普克模式将在第3.4节进一步讨论。
在大多数数学哲学中,例如柏拉图主义,数学陈述是无时态的。但直觉主义中的真假有一个时间面向:即既定事实将保持不变,但在某个时刻才得到证实的陈述在该时刻之前不具有真值。在“创造性主体”概念的形式化中,直觉主义的时间面向明显存在,而这一概念并非由布劳威尔提出,而是后来才由其他人提出。
尽管使用创造性主体概念的论证对于进一步理解作为数学哲学的直觉主义可能很重要,但它在该领域的发展中的作用不如直觉主义的两个规定的影响大,后者直接导向了布劳威尔和他以后的人愿意接受的数学真理。
3. 数学
尽管布劳威尔对直觉主义的发展在20世纪初数学家们的基础性争论中发挥了重要作用,但他的哲学对数学的深远影响在多年研究后才显现出来。直觉主义最典型的两个特性是它在证明中允许的逻辑推理原则和对直觉连续体的全面构想。只有在后者中,直觉主义才变得与经典数学不可比拟。在本条目中,重点是那些使直觉主义有别于其他数学学科的原则,因此,它的其他构造性方面将得到较少地处理。
3.1 BHK解释
在直觉主义中,知道一个陈述A是真的意味着有对它的证明。1934年,曾是布劳威尔学生的海廷(Arend Heyting)提出了一种后来被称为Brouwer-Heyting-Kolmogorov解释的说明形式,它抓住了直觉主义以及一般建构主义中逻辑符号的意义,通过指出连接词和量词应该如何解释,以一种非正式的方式定义了直觉主义的证明应该包括哪些内容:
• ⊥是不可证明的;
• A∧B 的证明由 A 的证明和 B 的证明组成;
• A∨B 的证明由一个 A 的证明或一个 B 的证明组成;
• A→B 的证明是一个将任何对 A 的证明转换为对 B 的证明的结构;
• ∃xA(x)的证明是通过提出该域的一个元素 d 以及 A(d)的证明来实现的;
• ∀xA(x)的证明是一种结构,它将每个证明d属于该域的证明转化为A(d)的证明。
一旦证明不可能存在A的证明,即提供一个结构,从A的任何可能的证明中导出错误,那么公式A的否定¬A就被证明了。因此,¬A与A→⊥等价。BHK解释并不是一个正式的定义,其构造的概念没有被定义,因此可以有不同的解释。不过,在这个非正式的层面上,人们已经被迫拒绝了经典逻辑中一直存在的一个逻辑原则:排中律(A∨¬A)。根据BHK解释,如果创造性主体知道A的证明或者A不能被证明的证明,那么这个陈述在直觉上就成立。如果既不知道 A 的证明,也不知道 A 的否定的证明,则(A∨¬A)不成立。开放性问题的存在,如哥德巴赫猜想或黎曼假设,都说明了这个事实。但是一旦找到了 A 的证明或者其否定的证明,情况就改变了,对这个特定的 A 来说,原则(A∨¬A)从那一刻起就是真的。
3.2 直觉主义逻辑
布劳威尔在他的哲学基础上拒斥了排中律,但阿伦德·海廷是第一个从直觉主义的角度提出一个可以接受的全面的逻辑原则的人。直觉主义逻辑,也是大多数其他形式的建构主义的逻辑,通常被称为“没有排中律的古典逻辑”。它用IQC来表示,IQC代表直觉主义量词逻辑,但文献中也有其他名称。一个可能的希尔伯特式的公理化由以下原则组成:
数学联邦政治世界观提示您:看后求收藏(同人小说网http://tongren.me),接着再看更方便。