构造性数学（三）

在其经典的反证形式中，FTD 被称为 König 引理：如果对于每个 n 都存在一条长度为 n 且错过 B 的路径，则存在一条错过 B 的无限路径（参见 Dummett 1977 [2000], 49–53）。 （当然，传统上可分离性条件是多余的。）构建柯尼希引理的布劳威尔反例很简单。

布劳威尔实际上在没有杆可拆卸性限制的情况下提出了扇形定理。试图证明更一般的扇形定理建设性地依赖于对我们如何知道子集是条形的分析，并导致布劳威尔提出条形归纳的概念；这在数学哲学中直觉主义条目的第 3.6 节中进行了讨论； van Atten (2004) 是关于棒感应的另一个很好的参考。我们将回到第 4 节中的扇形定理。

在布劳威尔原理的众多应用中，最著名的是他的一致连续性定理（它是从 CC1-2 的点连续性结果得出的，是一种比 FTD 更普遍的扇形定理形式）：

从紧凑（即完整、完全有界）度量空间到度量空间的每个映射都是一致连续的。

再次警告读者在布劳威尔的直觉主义框架内仔细解释这一点，不要跳到直觉主义与经典数学相矛盾的错误结论。更明智的做法是认为这两种数学没有可比性。有关进一步的讨论，请参阅直觉逻辑条目。

不幸的是——也许不可避免的是，面对像希尔伯特这样的数学家的反对——布劳威尔的数学和哲学直觉主义学派越来越多地参与到至少对古典数学家来说似乎是关于自然的准神秘的推测中。建设性思想的影响，损害了建设性数学本身的实践。布劳威尔派和希尔伯特派之间的这种不幸的两极分化在 20 年代臭名昭著的 Grundlagenstreit 中达到了顶峰，其详细信息可以在 van Dalen [1999, 2005] 和 van Stigt [1990] 的 Brouwer 传记中找到。

3.2 递归构造数学

20 世纪 40 年代末，俄罗斯数学家 A.A.马尔可夫开始发展另一种形式的构造性数学，即 RUSS，它本质上是具有直觉逻辑的递归函数理论（Markov [1954]，Kushner [1985]）。在这种类型中，对象是通过哥德尔编号来定义的，并且过程都是递归的； RUSS 与图灵、丘奇等人在 1936 年澄清可计算过程的本质后发展起来的经典递归分析之间的主要区别在于，RUSS 中使用的逻辑是直觉性的。

试图掌握 RUSS 的数学家面临的一个障碍是，用递归理论的语言表达它并不容易阅读；事实上，当打开库什纳精彩演讲[1985]的一页时，人们可能会想知道这是分析还是逻辑。 （这一评论应该参考 Aberth [1980, 2001] 的两本相对可读的关于经典递归分析的书来缓和。）幸运的是，由于 Richman [1983]，人们可以通过一种公理化方法来了解 RUSS 的核心（另请参阅Bridges & Richman [1987] 第 3 章）。

首先，如果存在从 N 的可分离子集到 S 的映射，我们定义集合 S 是可数的。用直觉逻辑，我们无法证明 N 的每个子集都是可分离的（邀请读者提供一个布劳威尔式的例子来证明这一点） ）。 Richman 公理化方法中 N 的可数子集与 RUSS 正常开发中的递归可枚举集相对应。

N 上的偏函数是指其定义域是 N 的子集的映射；如果域是 N 本身，那么我们将该函数称为 N 上的总函数。Richman 的 RUSS 方法基于直觉逻辑和可计算偏函数 (CPF) 的单个公理：

从N到N具有可数域的所有部分函数的集合都有一个ϕ0，ϕ1。

使用该原则可以清洁，快速推导的内容是显着的。例如，我们可以证明以下结果，几乎立即表明LLPO及其LPO在递归环境中是错误的。

有一个总功能f：n×n→{0,1}，这样

对于每个m，最多存在一个n，使得f（m，n）= 1;和

对于每个总函数f：n→{0,1}，n中存在m，k，使得f（m，2k+f（m））= 1。

然而，更感兴趣的是诸如Russ内的以下结果。

Specker的定理（Specker [1949]）：在闭合间隔[0,1]中存在严格增加的序列（R1，R2，…）[0,1]，因此对于每个x∈R，存在n∈N和Δ＞0这样所有n≥n的| x -rn |≥δ。

对于每个ε＞0，存在一个序列（i1，i2，…）的序列的开放间隔，以使r⊆⋃

无穷大

n = 1

在和∑

氮

n = 1

| in | ＜ε为每个N。（这样的间隔序列称为R的ε-sIngular覆盖物。）

存在一个连续的连续函数f：[0,1]→r，并不统一连续。

存在一个正值统一的连续函数f：[0,1]→r，其幼体为0。

从经典的角度来看，当人们意识到诸如“函数”和“实际数字”之类的单词分别解释为“递归函数”和“递归实数”时，这些结果适合到位。请注意，以上四个递归定理中的第二个是对（递归）真实线的开放式紧凑性特性的强递归反例。第四个是对经典定理的递归反例，即每个紧凑型套件的每个均匀连续映射均达到其量。

3.3主教的建设性数学

在接下来的十年半中，各种建设性数学的进展相对较慢。在数学中提高建构主义的概况所需的是，是一位最高的古典数学家，以表明在没有承诺布鲁威尔的非古典原理或递归功能理论的机制的情况下，可以进行深入的深入分析的彻底建设性发展。这项需求是在1967年满足的，以埃雷特·毕晓普（Errett Bishop）的建设性分析基础的出现[1967]（另请参见Bishop＆Bridges [1985]），这是一个令人惊讶的几年的产物，其中以非正式但严格的风格工作BiShop由普通分析师使用，为二十世纪分析的大部分分析提供了建设性的发展，包括Stone-Weierstrass定理，Hahn-Banach和Shipation定理，Hilbert Space上自偶会操作员的频谱定理，Lebesgue，Lebesgue抽象积分，HAAR测量和抽象傅立叶变换，千古定理以及Banach代数理论的要素的收敛定理。因此，他的谎言在希尔伯特（Hilbert）如此有力地表达的普遍看法：

例如，从数学家中被排除的原则将是相同的，因为将望远镜的望远镜或拳击手的使用方式相同。 （Hilbert [1928]）

Bishop的数学Bish不仅具有可读性的优势 - 如果您在任何页面上打开Bishop的书，您认为的内容显然可以识别为分析，即使，即使，即使不时，他在证明过程中的举动可能会出现对于一个被排除的中间定律而受过教育的人很奇怪 - 但是，与直觉或递归数学不同，它承认了许多不同的解释。直觉的数学，递归的建设性数学甚至经典的数学都提供了比什的模型。实际上，在任何合理的可计算数学模型中，都可以解释比什中的结果和证据，例如Weihrauch的第二型有效性理论（Weihrauch [2000]； Bauer [2005]）。

这种多重解释性如何实现？至少在某种程度上，Bishop拒绝固定其原始的“算法”概念，或者用他的话说“有限的例行”。这种拒绝引起了批评，即他的方法缺乏逻辑学家通常会期望基础系统的精确度。但是，可以通过更仔细地研究比什（Bish）证明定理的实际做法来克服这种批评：实际上，他们正在使用直觉逻辑进行数学。经验表明，对直觉逻辑的限制总是迫使数学家以至少非正式地描述为算法的方式工作。因此，算法数学似乎等同于仅使用直觉逻辑的数学。如果是这种情况，那么我们可以在任何合理定义的数学对象上使用直觉逻辑练习建设性数学，而不仅仅是某些类别的“建设性对象”。

这种观点或多或少是由Richman [1990，1996]提出的。以逻辑为建设性数学的主要特征，它并不能反映数学在逻辑上的首要地位，而逻辑是Brouwer，Heyting，Markov，Bishop和其他建构主义的先驱者的信念的一部分。另一方面，它确实捕获了实践中建设性数学的本质。

因此，人们可能会通过相信数学对象是精神创造的信念，以及Richman的认识论建构主义和那些将建设性数学视为其方法的特征，而基于其方法的特征，将Brouwer的本体论建构主义与其他被导致建设性数学的建构主义和其他人区分开来。直觉逻辑。当然，以前的建构主义方法不可避免地会导致后者。后者肯定与布鲁维尔本体论不一致。

要进行实际数学，我们不仅需要直观的逻辑。对于主教而言，数学的基础是积极的整数（请参阅Bishop [1967]的第3.1节中的引用）。 Bish早期的正式系统包括Myhill的[1975]公理基础，基于原始数量，集合和功能的原始概念； Feferman的[1975]显式数学系统；和弗里德曼（Friedman）的[1977]直觉ZF集理论。在此阶段，Bish的两个最受欢迎的正式基础是Aczel and Rathjen [2010年，在其他互联网资源中]的建设性Zermelo-Fraenkel Set理论（CZF），以及Martin-Löf[1975，1984]中的直觉理论。

3.4 Martin-Löf的建设性理论

在结束我们的现代建设性数学品种之旅之前，我们根据Martin-Löf的直觉类型理论访问了第四种ML。 Martin-Löf根据他在1966 - 68年在欧洲发表的讲座发表了有关建设性数学的笔记[1968]；因此，他参与建构主义在数学中的参与至少可以追溯到主教撰写建设性分析基础的时期。马丁·洛夫（Martin-Löf）的书是本着拉斯（Russ）的精神，而不是比什（Bish）。确实，在他自己的手稿完成之前，它的作者才可以访问Bishop的书。马丁·洛夫（Martin-Löf）随后将注意力转向了他的类型理论，作为主教式数学的基础。

用他自己的话说，这里是对ML基础思想的非正式解释：

我们将想到数学对象或构造。每个数学对象都是某种类型或类型的类型，并且始终与其类型一起给出。 …一种类型是通过描述我们为构建该类型的对象所需要做的事情来定义的。 …换句话说，如果我们理解的话，一种类型是明确的……成为该类型的对象意味着什么。因此，例如n→n [从n到n的函数]是一种类型，不是因为我们知道特定的数字理论函数，例如原始递归函数，而是因为我们认为我们一般理解了数字理论函数的概念。 （Martin-Löf[975]）

特别是，在此系统中，每个命题都可以表示为一种类型：即命题的证明类型。相反，每种类型都决定了一个命题：即，所讨论的类型居住的命题。因此，当我们将某个类型T视为命题时，我们会解释公式

x∈T

因为“ X是命题t的证明”。

Martin-Löf继续构建新型类型，例如笛卡尔产品和脱节工会。例如，笛卡尔产品

（πx∈A）b（x）

是将A类型A类型X的任意对象X变成B（X）对象的函数类型。在“命题”解释中，b（x）代表一个命题，上述笛卡尔产品对应于普遍命题

（∀x∈A）b（x）。

马丁·洛夫（Martin-Löf）仔细区分了证据和派生：证明对象是证明某些命题的事实；而派生是构造证明对象的记录。此外，他在判断中行使两种基本形式（一种不敢说“类型”）。第一个是证明对象和命题之间的关系，第二个命题的属性。在第一种情况下，判决是证明对象A是命题A的证人，或者是两个证明对象A和B是平等的，并且两者都证明A已被证明。第二种形式的第一种案例指出，命题A形成良好，第二个记录表明两个命题A和B是平等的。

有一套正式化ML的仔细，高度详细的规则。我们不会在这里参与其中，而是将读者参考其他来源，例如Sambin＆Smith [1998]。

当实际上在类型理论中进行建设性数学时，通常需要配备具有等效关系的完全呈现的集合（类型），该组合称为setoid。然后，映射是尊重那些等价关系的函数。这与主教介绍其非正式集合理论的方式非常吻合。 Martin-Löf的依赖类型对于构建子集很有用。例如，可以使用σ型构建实数（参见Martin-Löf[1984]）：

（σx∈N+→Q）（πm∈N+）（πn∈N+）[| xm -xn |≤（

1

米

+

1

n

），，，

因此，这种类型B的元素是由理性的收敛序列X组成的一对，以及它是收敛的证明P。通过将（x，p）〜（y，q）取为平均值，可以定义合适的等效关系。

∀M∈N+（| xm -ym |≤

2

米

）。

实数的结果固定为r =（r，〜）。我们可以很容易地证明

∀x∈R∃n∈Z（n＜x＜n+2）

然后，使用选择的类型理论公理（请参见下面的第4节），找到一个函数f：r→z，使得f（x）＜x＜x＜f（x）+2。但是，没有理由相信函数F尊重等效关系，也就是说，f（x）= f（y）如果x〜y，则f（x）= f（y）。

每个建设性的证明都体现了一种原则上可以提取并作为计算机程序重新铸造的算法；此外，建设性的证明本身就是算法正确的验证，即符合其规范。马丁·兰夫（Martin-Löf）正式建设性数学方法的主要优点是，它极大地促进了从证据中提取程序。这导致了在各个地方实施建设性数学的认真工作（参见Martin-Löf[1980]，Constable [1986]，Hayashi＆Nakano [1988]，Schwichtenberg [2009]）。用于证明提取的类型理论的一些最新实现是COQ和AGDA（请参阅其他Internet资源中的链接）。

4。选择的公理和连续假设

选择的完整公理可以说如下：

如果a，b是居住的集合，则是a×b的子集

∀X∈A∃Y∈B（（x，y）∈S），

然后存在一个选择函数f：a→b，使得

∀x∈A（（x，f（x））∈S）。

现在，如果要在建设性的解释下保存，那么对于给定的x∈A，选择函数的值f（x）不仅取决于x，而且还取决于x，证明x属于A。 ，我们不能指望产生这种选择功能。但是，公理中假设的BHK解释是有一种算法A，该算法应用于任何给定的x∈A，产生一个元素y∈B，因此（x，y）∈S。如果A是一个完全呈现的集合，则需要一个超出集合中每个元素的构造的工作来证明该元素确实属于A，那么我们可能会合理地期望该算法A是选择功能。在Martin-Löf的类型理论中，每个集合都是完全呈现的，并且与BHK的解释保持一致，选择的公理是可衍生的。

另一方面，在主教式的数学中，完全呈现了 - 或在他的术语中，基本的 - 套装很少见，一个例子是n；因此，我们可能期望选择的公理将无法衍生。实际上，正如Diaconescu [1975]和Goodman＆Myhill [1978]所示，由Bishop本人预先在1967年Bishop第58页的问题2中预先建立，选择的公理意味着不包括中间的定律。显然，Dioconescu-Goodman-Myhill定理仅适用于并非每个集合都完全呈现的假设。

不用在ML工作的建设性数学家通常会拒绝全部选择的公理，但要接受可数选择的公理，其中选择的域是n，而依赖的选择。但是，有些人宁愿甚至不可数的选择工作，理由是说出无限的选择而没有给出规则的难度，这是无限的难度，无论无穷大是否可以贬低。有趣的是，勒贝格在给博雷尔的一封信中确切地提出了这一点（请参阅摩尔[2013]，第316页）：

我完全同意哈哈达姆（Hadamard）的说法，当时他说，不给出规则的无限选择，这是一个难度，无论无穷大是否可以贬低，这也一样。

放弃甚至可数选择的效果是排除许多定理，这些定理使用基于选择的基于选择的参数证明了这些定理。但是那些主张避免选择的人会认为避免选择会迫使您更好地制定事物。

数学联邦政治世界观提示您：看后求收藏（笔尖小说网http://www.bjxsw.cc），接着再看更方便。