科学网

 找回密码
  注册

tag 标签: 公理系统

相关帖子

版块 作者 回复/查看 最后发表

没有相关内容

相关日志

量词消去——为了没有存在和任意
热度 1 dongmingwang 2018-5-27 22:01
数学中有两个非常特别的符号∃和∀,它们分别代表存在和任意。这两个符号与其限定变量一起,如∃x和∀y,称为存在量词和全称量词。存在和全称量词在数学中必不可少,但在很多时候我们都不希望它们出现,因为含有量词的数学问题往往都非常棘手、难以处理。量词符号∃和∀源自英文单词Exist和All的缩写E和A的镜像。这种镜像表示不仅简明对称,而且将两个特殊符号和常用变量区分开来。 譬如,含量词的公式(∃y) 的意思是:存在实数y,使得x 2 +y 2 -3=0和x+y0同时成立。如果将量词从公式中消去,那么可以得到一个等价的无量词公式x 2 -3≤0∧ 。这个公式比原来的公式简单而且明确很多。又譬如,哥德巴赫猜想断言:对任意大于2的偶数,存在两个奇素数,其和为给定正偶数。这个断言也可以用含有量词的公式来加以表述。几年前刚刚证明的Fermat大定理指出:对任意大于2的整数n,不存在正整数x,y,z,使得等式x n +y n =z n 成立。这个命题同样可以用含量词的公式加以表示。如果能消去上述两个命题中的全称和存在量词,即可得到等价的永真命题,因而也就给出了命题的证明。 量词消去理论是一阶逻辑理论的重要组成部分。在可判定性理论中,为判断含量词命题的真假,人们往往需要消去其中的量词得到一个等价的不含量词的命题,通过对后者真值的判断来获知原命题的真假。然而,量词消去并非平凡的问题,这可以从数学家们证明上述费马大定理的艰辛历程中得到印证。 量词消去问题也没有统一的求解方法。目前主要是根据变量所在环/域的结构和命题中所涉及的运算将量词消去问题分为不同的类型,然后针对每种类型设计特定的量词消去算法。如果一阶逻辑中的任意命题都可以经过有限步运算得出该命题是否为真,则称该一阶逻辑理论是可判定的。带+、*、=和运算的实闭域以及带+、*和=运算的代数闭域都是一阶逻辑可判定理论的典型范例。在这两种一阶逻辑理论中,多项式扮演着非常重要的角色,可以通过多项式理论将量词消去问题转化为多项式方程(组)的可解性问题,如实闭域上的一阶逻辑判定问题可以转化为求多项式方程(组)的实解问题,而代数闭域上的一阶逻辑判定问题可以转化为求多项式方程(组)的复解问题。 图1 David Hilbert(1862—1943) 判定问题由D. Hilbert首先提出。根据他的设想,可将数学知识全部纳入严密的公理体系之中,在此基础上寻找一般的机械化方法来判定命题是否成立。但是1931年,在Hilbert的设想提出还不到3年之后,K. Gödel发现的不完备定理就否定了Hilbert的设想。Gödel证明了任何一个形式系统,只要包括了简单的初等数论描述,而且是自洽的,那么它必定包含某些系统内所允许的方法既不能证其为真也不能证其为伪的命题。这一定理对现今十分热门的人工智能领域也产生了重要影响。Gödel不完备定理不仅使数学基础研究发生了划时代的变化,更是现代逻辑史上最重要的一座里程碑。该定理与A. Tarski的形式语言真理论、图灵机和判定问题,是现代逻辑科学在哲学方面的三个标志性成果。 图2 Kurt Gödel(1906—1978) Gödel不完备定理让人们有些失望,但并不是任何有意义的公理系统都是不完备的。Gödel定理成立的前提是要假设所考虑的公理系统可以用来“定义”自然数。那么是否所有系统都能用来 定 义自然数呢?回答是否定的,也就是说,完备的公理系统是存在的。Tarski证明了实数和复数理论都是完备的一阶公理化系统,并且于1930年提出了针对实闭域上初等代数和初等几何中命题的判定方法。该方法分为变换和判定两步,变换即是对任意给定的公式进行量词消去,判定则是对所得的无量词公式进行真值判断。Tarski将关于两个多项式实根的Sylvester定理推广到了任意多变元方程和不等式情形,利用方程求根的思想处理量词消去和命题判定问题,从而将命题的判定转化为能在有限步内完成的代数运算和命题演算。然而,Tarski方法的复杂度是超指数的,因此它只是一种理论化的方法,无法被广泛应用到具体问题。尽管如此,Tarski的方法还是为判定问题的研究指明了新方向,也开启了针对特定系统寻求判定方法的研究先河。 图3 Alfred Tarski(1901—1983) 柱形代数分解(简称CAD)是第一个实用的量词消去算法,由G. E. Collins于1975年提出,因此又被称为Collins算法。该算法可以将n维实空间中的任一半代数集通过投影和提升分解为有限多个互不相交的半代数集,所得半代数集都由同一组多项式定义,而在每个半代数集上定义多项式的符号不变。对含量词的命题进行量词消去即等价于寻找符合量词约束条件的参数胞腔,并将胞腔用多项式方程和不等式表示出来。CAD方法还可以用于半代数系统的实解隔离和实解分类。它和吴文俊的特征列方法、B. Buchberger的Gröbner基方法都是计算机代数系统的基石;后者也可以用于解决代数闭域上的量词消去问题。有关柱形代数分解有大量后续工作,学者从理论复杂度、实际计算效率、实施策略等方向针对量词消去问题对分解方法进行了研究、改进和发展。基于CAD的量词消去算法的复杂度虽然仍是双指数的,但较Tarski的超指数复杂度有了很大的改善,因此可以用于解决适当规模的量词消去问题。 图4 George E. Collins(1928—2017) 由于量词消去问题在一般情形的复杂度是变元个数的双指数,因此量词消去的研究重点是将量词消去问题进行分类,然后针对各类具体问题设计更优化的算法。 (本文经王东明教授审阅,图片均来源于网络) (杨静) 来源: 阿狗数学AlgoMath
个人分类: 阿狗数学|20195 次阅读|1 个评论
数学证明的长度:与公理系统能力负相关
热度 18 zlyang 2013-10-4 10:00
数学证明的长度:与公理系统能力负相关 杨正瓴 ( 天津大学电气与自动化工程学院,天津市 300072 ) 1 基本含义 “工欲善其事,必先利其器”(《论语·卫灵公》),以及“故以身观身,以家观家,以乡观乡,以邦观邦,以天下观天下。吾何以知天下然哉?以此。”(老子《道德经》第五十四章),早就说明“工具越强,劳动量越低”这样一个朴素的道理。 这个道理在数学证明中的具体体现,就是特定定理(命题)证明过程的长度问题。可能 B. Russell 在 1906 年, D. Hilbert 等人在 1928 年就考虑了这类问题。看上去 1936 年 K. Gdel 的 ber die Lnge von Beweisen ( On the length of proofs )是最早的专门文献。 1966-1974 年 Gregory J. Chaitin 提出的定理,被认为是哥德尔第一不完全性定理( Gdel's first incompleteness theorem )的信息论形式下的具体化。 Chaitin 定理的第三条说: Unfortunately, any formal system in which it is possible to determine each string of complexity less than n has either one grave problem or another. Either it has few bits of axioms and needs incredibly long proofs, or it has short proofs but an incredibly great number of bits of axioms. We say “incredibly” because these quantities increase more quickly than any computable function of n . Chaitin 定理的第三条的基本意思是: 对特定命题,如果在一个信息量小的公理系统( few bits of axioms )里证明,则证明的过程或长度是很大的。反过来,想要得到短的证明( short proofs ),则必须在一个信息量很大的公理系统( an incredibly great number of bits of axioms )里。 这和 “工欲善其事,必先利其器”的道理是一致的。 目前的数学命题证明(过程),往往是数百页的长度。如 Andrew Wiles 对费马大定理的证明。以及对四色定理计算机证明的批评: “一个好的数学证明应当像一首诗——而这纯粹是一本电话簿!( A good mathematical proof is like a poem - this is a telephone directory! )”这种长的数学证明,除了数学问题的难度本身引起之外,另一种可能的原因是:证明所采用的数学理论的信息量太小。 Grigori Perelman 对 Poincaré conjecture 证明的核心,大约十页。这说明合适的理论,是可以缩短数学证明长度的。 采用信息量大的数学理论进行证明,是缩短证明长度的主要策略之一。 2 两个例子 2.1 矩阵乘法 以 n 阶有理数方阵为例,由于矩阵乘法定义中的加法会引起 lg n 的进位位,所以对于两个“独立因素”的方阵,定义包含的必须信息量为 O ( n 3 × lg n ) 。换言之,不存在比 O ( n 3 ) 更小的时间复杂性。 以 Strassen 算法为代表的 O ( n 2+ ε ) 类方法,核心是“把多个乘法合并在一起 ” 计算。在数字计算机上,这几乎必然导致计算结果误差的增大。其极限是 1990 年陈道琦、谢友才、应文隆在科学通报发表的《关于矩阵乘法的一个最佳算法》。该方法只用一次乘法,但需要 W ( n 3 × lg n ) 的有效数字位数。 2.2 “P对NP” “ P 对 NP ”( P versus NP, P vs NP )问题当前研究与证明的主流方法主要有三大类:对角化 diagonalization 、电路复杂性 circuit complexity 、证明复杂性 proof complexity 。它们都是比较弱小的数学理论,所以在里面证明“对确定型图灵机 P ≠ NP ”的难度极大( incredibly long proofs )。 换成信息量大的 ZF ( Zermelo–Fraenkel set theory ),则不难发现:幂集公理( Axiom of power set )直接引起康托定理( Cantor theorem )。由于“非确定型图灵机的状态数”可以是“它对应的确定型图灵机的幂集”,所以 P ≠ NP 。准确地说,“ P 对 NP ”是个相对性的问题,不存在抽象的确定答案。接受 ZF ,则有“对确定型图灵机 P ≠ NP ”;反过来,不接受 ZF ,“ P 对 NP ”的答案则是需要进一步的具体考虑。 参考文献: B. Russell The theory of implication, American Journal of Mathematics , 28, pp. 159-202. D. Hilbert and W. Ackermann Grundzüge der theoretischen Logik , Springer-Verlag, Berlin. K. Gdel ber die Lnge von Beweisen, Ergebnisse eines Mathematischen Kolloquiums, pp. 23-24. English translation in Kurt Gdel: Collected Works, Volume 1 , pages 396-399, Oxford University Press, 1986. Pavel Pudlák The lengths of proofs, in Handbook of Proof Theory , S.R. Buss ed., Elsevier, pp.547-637. Gdel incompleteness theorem, Encyclopedia of Mathematics , http://www.encyclopediaofmath.org/index.php/G%c3%b6del_incompleteness_theorem . Gregory J. Chaitin Information-theoretic computational complexity. IEEE Transactions on Information Theory , IT-20, pp. 10-15. 杨东屏 哥德尔不完全性定理剖析 , 曲阜师范大学学报:自然科学版 , 19(1): 31-36. Andrew Wiles Modular elliptic curves and Fermat's Last Theorem, Annals of Mathematics ( Annals of Mathematics ), 141(3): 443-551. 杨正瓴 “ P 对 NP ”难题研究的形转换新思路 , 科学智慧火花 , http://idea.cas.cn/viewdoc.action?docid=9402 . 杨正瓴 第二类计算机构想 . 中国电子科学研究院学报 , 6(4): 368-374. YANG Zhengling ( 杨正瓴 ) A non-canonical example to support that P is not equal to NP. Transactions of Tianjin University , 17(6): 446-449. Cantor theorem, Encyclopedia of Mathematics , http://www.encyclopediaofmath.org/index.php/Cantor_theorem . ZFC (Zermelo–Fraenkel set theory with the axiom of choice), Encyclopedia of Mathematics , http://www.encyclopediaofmath.org/index.php/ZFC . 相关链接: 俗解Chaitin定理 http://bbs.sciencenet.cn/home.php?mod=spaceuid=107667do=blogid=478066 矩阵乘法需要O(n^3)的时间,不能再减少 http://bbs.sciencenet.cn/blog-107667-725846.html
个人分类: 基础数学-逻辑-物理|24514 次阅读|73 个评论

Archiver|手机版|科学网 ( 京ICP备07017567号-12 )

GMT+8, 2024-4-27 01:01

Powered by ScienceNet.cn

Copyright © 2007- 中国科学报社

返回顶部