24小时热门版块排行榜    

查看: 730  |  回复: 0
当前主题已经存档。

formleaf

木虫 (正式写手)

[交流] 构造性数学的历史

构造性数学的历史
http://icl.pku.edu.cn/yujs/papers/html/constructism.htm
首先声明,构造主义更多的是方法论,举例说明:直觉主义者(坚持数学对象是精神的构造)都是构造主义者,但反之不成立。
构造性数学与古典的数学区别在于构造性的数学认为“存在就是被构造”。为了做到构造性,我们必须重新解释存在量词及其其他逻辑联结词和量词,以便用构造的观点解释包含这些逻辑表达式的命题的证明的含义。
尽管十九世纪的某些数学家---值得注意的是Kronecker(他的名言是“上帝创造了自然数,其他都是人的工作。”)---表示了不赞成当时数学中“唯心的”、非构造性的方法,直到L.E.J.Brouwer(1881-1966)的那篇具有挑战性的作品(源于Brouwer在阿姆斯特丹的博士论文(Brouwer[1907]))公布于世的四十七年后,构造性数学的一条精确、系统的研究方法的基础才被奠定。在Brouwer的哲学(即直觉主义)中,数学是人的意志的自由创造,并且,一个对象存在当且仅当它可被构造。不幸的是(也许是不可避免的),Brouwer及其直觉主义学派的数学和哲学面临Hilbert那样的地位的数学家的反对和构造性数学本身在自身实践方面的缺陷,至少在古典的数学家的眼中,Brouwer关于构造性的思维本质的推测带有半神秘的色彩。另一方面,19世纪30年代俄国数学家A.A Markov发展了一种递归的构造性的数学,特别是基于直觉逻辑的递归函数理论。Markov方法的缺点是递归函数理论上的语言的严格规则约束了它的推广使用。例如,在传统的分析学家看来Markov的分析显得不自然---可读性很差,于是构造主义在递归分析上的进展相对较缓慢并且难以与古典分析相比。
我们需要的是有一个一流的经典数学家去证明,构造性数学的发展离开了Brouwer怪癖哲学或递归函数理论的机械论调也是可行的。1967年,Errett Bishop的专著《构造性分析的基础》实现了这个愿望。Bishop提供了20世纪分析学的大部分结果的构造性实现,包括Stone-Weierstrass定理,Hahn-Banach分离定理,Hilbert空间上的自伴算子的谱定理,抽象积分的Lebesgue收敛定理,Haar测度和抽象Fourier变换,遍历定理,和Banach代数理论的基础。这样,他一次性地改变了传统的观点(Hilbert说过:“剥夺数学家的排中律,就如同剥夺天文学家的望远镜或拳击手拳头的使用一样。”)。
不仅Bishop的数学(BISH)有可读性的优点---你打开Bishop著作的任何一页,你看见的都是可被认可的分析。不同的直觉或递归的数学承认不同的解释。直觉数学、Markov的递归的构造性的数学,甚至古典的数学都提供了BISH的模型。事实上,BISH的结果和证明经过较小的修改,在可计算的数学的某个合理的模型中可以找到解释。例如,Weihrauch的TTE。这多重的解释能力是如何完成的呢?至少由于Bishop拒绝放弃他关于“算法”或“有限原则”的原始观点。他的拒绝导致了他的方法的基础遭受到一些批评,例如,缺乏逻辑学家通常视为系统基础的精密。然而,这批评可以被克服,只要我们仔细地看看BISH的创业者们实际上了什么,而不是Bishop认为自己想做什么。当他们证明定理时,实践上,他们正在做直觉逻辑基础上的数学。有限数学与只用直觉逻辑的数学是等价的。如果这是事实,我们能在任何合理定义的数学对象上实践使用直觉逻辑的构造性数学,而不仅仅是可构造的对象。这个观点或多或少被Richman所发展。拿逻辑作为构造性的数学的特征,当然没有反映Brouwer, Heyting, Markov, Bishop等构造主义先驱们关于逻辑基础上的数学的最初的想法。Richman的哲学是构造性的数学的实践之一,并且与数学中的更激进的构造性哲学相容兼容,例如,Brouwer的直觉主义认为数学的对象是精神的构造。它是认识论的哲学,而非本体论。
最近的发展:自从Bishop的著作出版以来的30年里,构造性分析理论和代数理论有了充足的发展。这些发展---值得注意的是在积分理论和Riemann映射---在1985年Bishop和Bridges的著作中有详细的阐述(尽管不是第一次);其它的散布在Richman和Bridges的原始文章中。
BISH的形式系统在计算机程序设计中有有趣的应用。这些应用的基本想法是:从BISH的每个证明都可以得到一个程序,这个程序的正确性由这个证明提供。这个领域的开创性的工作由Martin-Lof于1975年在他的类型理论中给出。在这个充满希望的领域,计算机科学家们正在着从事定理机器证明的研究工作。
回复此楼

» 收录本帖的淘帖专辑推荐

控制理论灌水大法

» 猜你喜欢

已阅   回复此楼   关注TA 给TA发消息 送TA红花 TA的回帖
相关版块跳转 我要订阅楼主 formleaf 的主题更新
普通表情 高级回复 (可上传附件)
信息提示
请填处理意见