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

直觉主义数学的形式化不仅仅包括算术。分析的很大一部分已经从构造的角度被公理化了（Kleene 1965, Troelstra 1973）。这些系统的建构性可以用函数、类型理论或可实现性解释来建立，其中大多数是基于哥德尔的辩证法解释(Gödel 1958, Kreisel 1959)、Kleene可实现性(Kleene 1965)或类型理论(Martin-Löf 1984)或其延伸。在这些解释中，构造性语句所依据的函数，例如将y分配给∀x∃yA(x,y)中的每个x的函数，以各种方式被明确化。

在(Scott 1968 and 1970)中，提出了一个二阶直觉分析理论的拓扑学模型，其中的实数被解释为从Baire空间到经典实数的连续函数。在这个模型中，克里普克的模式以及某些连续性公理是成立的。在(Moschovakis 1973)中，这种方法被改编为以选择序列的方式构造直觉分析理论的模型。在这个模型中，克里普克的模式和某些连续性公理也是成立的。在(Van Dalen 1978)中，Beth模型被用来提供一个满足选择模式、弱连续性实例和Kripke模式的算术和选择序列的模型。在这个模型中，每个节点的域都是自然数，因此人们不必像克里普克模型那样使用非标准模型。此外，创建主体的公理CS1-3可以在其中得到解释，从而表明这个理论是一致的。

5.3 无规律序列（Lawless sequences）

存在着无规律序列的公理化，它们都包含连续性公理的扩展（Kreisel 1968, Troelstra 1977）。特别是以开放数据公理的形式，说明对于 A (α) 不包含除此之外的其他非法学参数α：

A(α)→∃n∀β∈α(¯¯¯n)A(β)

在(Troelstra 1977)中，无规律序列的理论在直觉分析的背景下被发展(并被证明)。除了基本分析的公理之外，对于无规律序列，它还包含了开放数据、连续性、可决断性和密度(密度表示每个有限序列都是无规律序列的初始段)等公理的强化形式。特别有趣的是，在这些理论中，无规律序列上的量词可以被消除，这一结果也可以看作是为这类理论提供了一个有规律序列的模型。无规律序列理论的其他经典模型已经在范畴理论中以模型束的形式被构造出来（van der Hoeven and Moerdijk 1984）。在(Moschovakis 1986)中，引入了一个相对于一定的类定律元素集合的选择序列的理论，以及一个经典模型，在这个模型中，无规律序列正好是通用的。

5.4 创造主体的形式化（Formalization of the Creating Subject）

第2.2节介绍的创造主体可以产生选择序列，这是布劳威尔直觉主义中最重要和最复杂的数学实体。一些哲学家和数学家试图从数学和哲学的角度进一步发展创造主体的理论。

在创建主体概念的形式化中，它的时间方面是用符号形式化的 □ n A 表示创造主体在时间n有一个A的证明（在其他一些表述中：经历了A的真理性 A 在时间 n ). Georg Kreisel (1967)为“创造主体”引入了以下三个公理，它们一起用CS表示：

CS1：□nA∨¬□nA(在时间n，可以决定创建主体是否有A的证明。)

CS2：□mA→□m+nA(创造主体永远不会忘记它所证明的东西)

CS3：(∃n□nA→A)∧(A→¬¬∃n□nA)(创造主体只证明真实的东西，对创造主体来说，没有真实的陈述是无法证明的。)

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