【SEP】数学与哲学直觉主义（二） (6-1)

4. 建构主义（Constructivism）

直觉主义与大多数其他形式的建构主义有一个核心部分。一般来说，建构主义关注的是建构的数学对象和推理。至少在原则上，人们可以从建构性证明中提取计算元素的算法，并模拟在证明中确定存在的建构。大多数形式的建构主义都与经典数学兼容，因为它们一般都是基于对量词和连接词以及允许的结构的更严格的解释，而不做额外的假设。几乎所有建构主义团体所接受的逻辑都是一样的，即直觉主义逻辑。

经典数学中的许多存在性定理都有一个建设性的类似物，其中存在性声明被一个关于近似的声明所取代。我们在上面关于弱反例的章节中看到了一个例子，即中值定理。数学的大部分内容都可以用类似的方式建设性地恢复。之所以在此不作进一步处理，是因为本条目的重点在于直觉主义的那些方面，这些方面使它与数学的其他建构主义分支不同。对于建构主义的彻底处理，读者可以参考本百科全书中的相应条目。

5. 元数学

尽管布劳威尔以精确和基本的方式发展了他的数学，但我们今天所知的形式化只是后来由其他人进行的。事实上，根据布劳威尔的观点，数学是在内部展开的，形式化虽然不是不可接受的，但也是不必要的。在他之后的其他人则不这么认为，直觉主义数学的形式化和对其元数学特性的研究，特别是对算术和分析的研究，吸引了许多研究者。所有形式化的基础是直觉主义逻辑的形式化，这一点上面已经讲过了。

5.1 算术

由Arend Heyting制定的Heyting算术HA是自然数直觉论的形式化（Heyting 1956）。它具有与Peano算术PA相同的非逻辑公理，但它是基于直觉主义逻辑的。因此，它是对经典算术的限制，而且它是几乎所有建构数学领域中公认的自然数理论。海廷算术有许多反映其建构性的属性，例如，对直觉逻辑也适用的分离属性。HA的另一个属性是数字存在属性，这是PA所不具备的：( ¯¯¯ n 是对应于自然数的数字 n )

(NEP) HA⊢∃xA(x)⇒∃n∈NHA⊢A(¯¯¯n).

这个属性在PA中不成立，这是因为PA证明了∃x(A(x)∨∀y¬A(y))的事实。例如，考虑A(x)是公式T（e,e,x）的情况，其中T是可解的Kleene谓词，表示x是编码为e的程序在输入e上的终止计算的代码。如果每一个e都存在一个数n，使得PA⊢T(e,e,n)∨∀y¬T(e,e,y)，那么通过检查T(e,e,n)是否成立，就可以决定一个程序e在输入e上是否终止。

马尔科夫规则是一个在经典上和直觉上都成立的原则，但只有对HA来说，这个事实的证明是不难的：

(MR)HA⊢∀x(A(x)∨¬A(x))∧¬¬∃xA(x)⇒HA⊢∃xA(x)

由于HA证明了每个原始递归谓词的排除中间律，因此，对于这样的A，HA中¬¬∃xA(x)的可推导性也意味着∃xA(x)的可推导性。由此可见，PA对HA是Π02保守的。也就是说，对于原始递归的A：

PA⊢∀x∃yA(x,y)⇒HA⊢∀x∃yA(x,y).

因此，HA的可证递归函数类与PA的可证递归函数类相吻合，根据建构主义和直觉主义的基础思想，这一属性可能并不令人惊讶。

5.2 分析

数学联邦政治世界观提示您：看后求收藏（同人小说网http://tongren.me），接着再看更方便。