數學證明
在數學上,數學證明(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).