数学证明
在数学上,数学证明(mathematical proof)是在一个特定的公理系统中,根据一定的规则或标准,由公理和定理推导出某些命题的过程。比起证据,数学证明一般依靠演绎推理,而不是依靠自然归纳和经验性的理据。这样推导出来的命题也叫做该系统中的定理。
数学证明建立在逻辑之上,但通常会包含若干程度的自然语言,因此可能会产生一些含糊的部分。
实际上,用文字形式写成的数学证明,在大多数情况都可以视为非形式逻辑的应用。在证明论的范畴内,则考虑那些用纯形式化的语言写出的证明。这个区别导致了对过往到现在的数学实践、数学上的拟经验论和民俗数学的大部分检验。
数学哲学就关注语言和逻辑在数学证明中的角色,和作为语言的数学。
定义
[编辑]数学上的证明包括两个不同的概念。
首先是非形式化的证明:一种以自然语言写成的严密论证,用来说服听众或读者去接受某个定理或论断的真确性。由于这种证明使用了自然语言,因此对于非形式化证明在严谨性上的标准,将取决于听众或读者对课题的理解程度。非形式化证明出现在大多数的应用场合中,例如科普讲座、口头辩论、初等教育或高等教育的某些部分。有时候非形式化的证明被称作“正式的”,但这只是强调其中论证的严谨性。
而当逻辑学家使用“正式证明”一词时,指的是另一种完全不同的证明——形式化证明。
形式化证明
[编辑]在数理逻辑中,形式化证明并不是以自然语言书写,而是以形式化的语言书写:这种语言包含了由一个给定的字母表中的字符所构成的字符串。而证明则是一种由该些字符串组成的有限长度的序列。这种定义使得人们可以谈论严格意义上的“证明”,而不涉及任何逻辑上的模糊之处。
研究证明的形式化和公理化的理论称为证明论。
尽管理论上来说,每个非形式化的证明都可以转化为形式化证明,但实际中很少会这样做。对形式化证明的研究主要应用在探讨关于可证明性的一般性质,或说明某些命题的不可证明性等等。
常见的证明技巧
[编辑]直接证明
[编辑]直接证明也称为逻辑演绎,是指从公认的事实或者公理出发,运用逻辑推演而导出需要证明的命题的真伪的方法。直接证明法一般使用谓词逻辑,运用存在量词或全称量词。主要的证明方式有肯定前件论式、否定后件论式、假言三段论式以及选言三段论式等等。比如说要证明命题:“任何奇数乘以另一个奇数仍然是奇数”,可以直接证明如下:
- 任何奇数都可以写成的形式,其中是整数。任取两个奇数,它们分别可以写作和,其中和是整数。它们的乘积为。所有能写成整数的两倍加1的数都是奇数。是整数,所以是奇数。证明完毕。
构造法
[编辑]构造法一般用于证明存在性定理,运用构造法的证明称为构造性证明。具体做法是构造一个带有命题里所要求的特定性质的实例,以显示具有该性质的物体或概念的存在性。也可以构造一个反例,来证明命题是错误的[2]。例如证明命题“2的素数次幂减一后不总是素数”,便可用构造法:
- 只需证明存在某个素数,使得2的次幂减一后不是素数。为此,考察素数11。2的次幂减一等于。不是素数。因此命题得证。
有些构造法证明中并不直接构造满足命题要求的例子,而是构造某些辅助性的工具或对象,使得问题更容易解决。一个典型的例子是常微分方程稳定性理论中的李亚普诺夫函数的构造[3]。又如许多几何证明题中常常用到的添加辅助线或辅助图形的办法。
非构造性证明
[编辑]与构造法证明相对的是非构造性证明,即不给出具体的构造而证明命题所要求对象的存在性的证明方法。比如下面例子:
在这个证明里并没有给出使得是有理数的两个具体的无理数[2]。
穷举法
[编辑]穷举法是一种列举出命题所包含的所有情况从而证明命题的方法[4]。例如证明“所有两位数中只有25和76的平方是以自己作为尾数”,只需计算所有两位数:10至99的平方,一一验证即可。显然,使用穷举法的条件是命题所包含的可能情况为有限种,否则无法一一罗列。
换质位法
[编辑]在谓词逻辑里,若同时否定一个命题的主词和谓词,则其结果称为原命题的换质。若交换主词和谓词的位置,则其结果被称作换位。先换质再换位则被称为换质位,同理先换位再换质则被称为换位质。例如“所有的S是P”的换质位是“所有的不是P的不是S”。换质位法是指利用换质及换位,将一个命题改为一个与其逻辑等价的命题,因此只要证明了后者就证明了原来的命题[5]。例如,要证明鸽笼原理:“如果n个鸽笼里装有多于n只鸽子,那么至少有一个笼子里有两只或者两只以上鸽子”,可以转证与其等价的逆否命题:“如果n个鸽笼的每一个中至多装有一只鸽子,那么n个鸽笼里至多装有n只鸽子”。而后者是明显的。
个案分析
[编辑]个案分析或分类讨论,是指将结论分成有限的个案,然后逐个证明的方法。
算两次
[编辑]算两次是一种对同一个量进行两种虽不同但都正确的分析,得到两个虽不同但相等的表达式的方法,常用于证明恒等式[6]。
反证法
[编辑]反证法是一种古老的证明方法,其思想为:欲证明某命题是假命题,则反过来假设该命题为真。在这种情况下,若能通过正确有效的推理导致逻辑上的矛盾(如导出该命题自身为假,于是陷入命题既真且假的矛盾),则能证明原来的命题为假。[7]无矛盾律和排中律是反证法的逻辑基础。反证法的好处是在反过来假设该命题为真的同时,等于多了一个已知条件,这样对题目的证明常有帮助[8]。
例子:证明命题“不是有理数”。
- 命题:不是有理数。
- 证明:假设是有理数,那么存在正整数使得为整数。不妨设为其中最小的(根据良序原理,必然存在最小的)。考虑。是一个比小的正整数,但也是整数。这与的最小性矛盾。所以根号2不是有理数[9]。
数学归纳法
[编辑]数学归纳法是一种证明可数无穷个命题的技巧。欲证明以自然数编号的一串命题,先证明命题1成立,并证明当命题成立时命题也成立,则对所有的命题都成立[5]。在皮亚诺公理系统中,自然数集合的公理化定义就包括了数学归纳法。数学归纳法有不少变体,比如从0以外的自然数开始归纳,证明当命题对小于等于n的自然数成立时命题也成立,反向归纳法,递降归纳法等等。广义上的数学归纳法也可以用于证明一般良基结构,例如集合论中的树。另外,超限归纳法提供了一种处理不可数无穷个命题的技巧,是数学归纳法的推广[10]。
例子:证明对所有自然数,命题
当,左边=1,右边=
假设对某个自然数,命题成立:,以下证明成立,即::
- 左边
- 右边
所以,对任意自然数,都有
其他证明方式
[编辑]直观证明
[编辑]直观证明或可视化证明是指用图像或表格等直观的手段证明命题的方法。这类证明可以达到不借助语言而证明的效果。如右图是勾股定理的一个图示证明。
计算机辅助证明
[编辑]电脑协助证明是二十世纪出现的证明方式。直到二十世纪中,人们一直认为任何的数学证明都应当能够被一个水平足够的数学家检验,以证实其正确性。然而,今天的数学家已经能够运用计算机来证明定理,并且完成人类难以做到的计算[11]。1976年四色定理的证明是计算机辅助证明的经典例子[12]。证明的方法是将地图上的无限种可能情况减少为1936种状态,并由计算机对每个可能的情况进行验证。有不少数学家对于计算机证明持谨慎态度,因为很多证明太长,不能由人手直接验证。此外,算法上的错误,输入时的失误甚至计算机运行期间出现的错误都有可能导致错误的结果。
证明的结尾
[编辑]有时在证明的结尾会加上Q.E.D.三个字母,这是拉丁文Quod Erat Demonstrandum的缩写,意思是“证明完毕”。现在的证明完毕符号,通常是■(实心黑色正方形),称之为“墓碑”或“哈尔莫斯(Halmos symbol)”(因保罗·哈尔莫斯最先采用此做法)。墓碑有时是空心的□。另一个简单方法是写“proven”、“shown”或“证毕”之类的文字。
参见
[编辑]参考资料
[编辑]- ^ Bill Casselman. One of the Oldest Extant Diagrams from Euclid. University of British Columbia. [2008-09-26]. (原始内容存档于2012-06-04).
- ^ 2.0 2.1 余红兵; 严镇军. 《构造法解题》. 中国科学技术大学出版社. 2009 [2014-01-11]. ISBN 7312024831. (原始内容存档于2019-05-03).
- ^ 王高雄; 周之铭; 朱思铭; 王寿松. 《常微分方程》(第三版). 高等教育出版社. [2014-01-11]. ISBN 9787040193664. (原始内容存档于2019-05-03).
- ^ Reid, D. A. & Knipping, C. (2010).Proof in Mathematics Education: Research, Learning, and Teaching (页面存档备份,存于互联网档案馆) Sense Publishers, p. 133.
- ^ 5.0 5.1 金岳霖; 杨宝星. 《形式逻辑》. 辽宁人民出版社. 1979 [2014-01-11]. ISBN 7010002037. (原始内容存档于2014-01-11).
- ^ 单壿. 《算两次》. 中国科学技术大学出版社. 2009 [2014-01-11]. ISBN 7312024823. (原始内容存档于2014-01-11).
- ^ 类似地,有更一般的归谬法:若然假设该命题为真,在通过正确有效的推理后会得出逻辑上的矛盾、与某个事实或公理相悖的结论、或荒谬难以接受的结果,亦可以证明原来的命题为假。反证法是归谬法的其中一种形式。
- ^ Vinciane CAMBRÉSY-TANT,Dominique CAMBRÉSY,Stéphane CARPENTIER,''Autour du raisonnement par l'absurde'',IUFM Nord - Pas de Calais (PDF). [2014-01-11]. (原始内容 (PDF)存档于2013-12-28).
- ^ THEODOR ESTERMANN,1975 (PDF). Blms.oxfordjournals.org. 2013-12-06 [2014-01-11].
- ^ 苏淳. 《漫话数学归纳法》. 中国科学技术大学出版社. 2009 [2014-01-11]. ISBN 7312024866. (原始内容存档于2019-05-03).
- ^ The History and Concept of Mathematical Proof, Steven G. Krantz. 1. February 5, 2007 (PDF). [2014-01-11]. (原始内容存档 (PDF)于2007-02-21).
- ^ 相信數學,或相信電腦. 中国科普博览. 2004-04-29 [2014-01-14]. (原始内容存档于2017-03-05).