Can you summarize the following document?
        
  數學上的證明包括兩個不同的概念。  首先是非形式化的證明:一種以自然語言寫成的嚴密論證,用來說服聽眾或讀者去接受某個定理或論斷的真確性。由於這種證明使用了自然語言,因此對於非形式化證明在嚴謹性上的標準,將取決於聽眾或讀者對課題的理解程度。非形式化證明出現在大多數的應用場合中,例如科普講座、口頭辯論、初等教育或高等教育的某些部分。有時候非形式化的證明被稱作“正式的”,但這只是強調其中論證的嚴謹性。  而當邏輯學家使用“正式證明”一詞時,指的是另一種完全不同的證明——形式化證明。

  在數理邏輯中,形式化證明並不是以自然語言書寫,而是以形式化的語言書寫:這種語言包含了由一個給定的字母表中的字元所構成的字串。而證明則是一種由該些字串組成的有限長度的序列。這種定義使得人們可以談論嚴格意義上的「證明」,而不涉及任何邏輯上的模糊之處。  研究證明的形式化和公理化的理論稱為證明論。  儘管理論上來說,每個非形式化的證明都可以轉化為形式化證明,但實際中很少會這樣做。對形式化證明的研究主要應用在探討關於可證明性的一般性質,或說明某些命題的不可證明性等等。

  

  直接證明也稱為邏輯演繹,是指從公認的事實或者公理出發,運用邏輯推演而匯出需要證明的命題的真偽的方法。直接證明法一般使用謂詞邏輯,運用存在量詞或全稱量詞。主要的證明方式有肯定前件論式、否定後件論式、假言三段論式以及選言三段論式等等。比如說要證明命題:“任何奇數乘以另一個奇數仍然是奇數”,可以直接證明如下:

  構造法一般用於證明存在性定理,運用構造法的證明稱為構造性證明。具體做法是構造一個帶有命題裡所要求的特定性質的例項,以顯示具有該性質的物體或概念的存在性。也可以構造一個反例,來證明命題是錯誤的。例如證明命題“2的質數次冪減一後不總是質數”,便可用構造法:  有些構造法證明中並不直接構造滿足命題要求的例子,而是構造某些輔助性的工具或物件,使得問題更容易解決。一個典型的例子是常微分方程穩定性理論中的李亞普諾夫函式的構造。又如許多幾何證明題中常常用到的新增輔助線或輔助圖形的辦法。

  與構造法證明相對的是非構造性證明,即不給出具體的構造而證明命題所要求物件的存在性的證明方法。比如下面例子:  在這個證明裡並沒有給出使得formula_17是有理數的兩個具體的無理數。

  窮舉法 (數學)是一種列舉出命題所包含的所有情況從而證明命題的方法。例如證明“所有兩位數中只有25和76的平方是以自己作為尾數”,只需計算所有兩位數:10至99的平方,一一驗證即可。顯然,使用窮舉法的條件是命題所包含的可能情況為有限種,否則無法一一羅列。

  在謂詞邏輯裡,若同時否定一個命題的主詞和謂詞,則其結果稱為原命題的換質。若交換主詞和謂詞的位置,則其結果被稱作換位。先換質再換位則被稱為換質位,同理先換位再換質則被稱為換位質。例如“所有的S是P”的換質位是“所有的不是P的不是S”。換質位法是指利用換質及換位,將一個命題改為一個與其邏輯等價的命題,因此只要證明了後者就證明了原來的命題。例如,要證明鴿籠原理:“如果n個鴿籠裡裝有多於n只鴿子,那麼至少有一個籠子裡有兩隻或者兩隻以上鴿子”,可以轉證與其等價的逆否命題:“如果n個鴿籠的每一箇中至多裝有一隻鴿子,那麼n個鴿籠裡至多裝有n只鴿子”。而後者是明顯的。

  個案分析或分類討論,是指將結論分成有限的個案,然後逐個證明的方法。

  算兩次是一種對同一個量進行兩種雖不同但都正確的分析,得到兩個雖不同但相等的表示式的方法,常用於證明恆等式。

  

  反證法是一種古老的證明方法,其思想為:欲證明某命題是假命題,則反過來假設該命題為真。在這種情況下,若能通過正確有效的推理導致邏輯上的矛盾(如匯出該命題自身為假,於是陷入命題既真且假的矛盾),則能證明原來的命題為假。無矛盾律和排中律是反證法的邏輯基礎。反證法的好處是在反過來假設該命題為真的同時,等於多了一個已知條件,這樣對題目的證明常有幫助。  例子:證明命題“formula_23不是有理數”。

  數學歸納法是一種證明可數無窮個命題的技巧。欲證明以自然數"n"編號的一串命題,先證明命題1成立,並證明當命題"n"成立時命題"n"+1也成立,則對所有的命題都成立。在皮亞諾公理系統中,自然數集合的公理化定義就包括了數學歸納法。數學歸納法有不少變體,比如從0以外的自然數開始歸納,證明當命題對小於等於"n"的自然數成立時命題"n"+1也成立,反向歸納法,遞降歸納法等等。廣義上的數學歸納法也可以用於證明一般良基結構,例如集合論中的樹。另外,超限歸納法提供了一種處理不可數無窮個命題的技巧,是數學歸納法的推廣。  例子:證明對所有自然數formula_35,命題formula_36  當formula_37,左邊=1,右邊=formula_38  假設對某個自然數formula_39,命題formula_40成立:formula_41,以下證明formula_42成立,即:formula_43:  所以,對任意自然數formula_35,都有formula_50

  

  直觀證明或視覺化證明是指用影象或表格等直觀的手段證明命題的方法。這類證明可以達到不借助語言而證明的效果。如右圖是勾股定理的一個圖示證明。

  電腦協助證明是二十世紀出現的證明方式。直到二十世紀中,人們一直認為任何的數學證明都應當能夠被一個水平足夠的數學家檢驗,以證實其正確性。然而,今天的數學家已經能夠運用計算機來證明定理,並且完成人類難以做到的計算。1976年四色定理的證明是計算機輔助證明的經典例子。證明的方法是將地圖上的無限種可能情況減少為1936種狀態,並由計算機對每個可能的情況進行驗證。有不少數學家對於計算機證明持謹慎態度,因為很多證明太長,不能由人手直接驗證。此外,演算法上的錯誤,輸入時的失誤甚至計算機執行期間出現的錯誤都有可能導致錯誤的結果。

  有時在證明的結尾會加上Q.E.D.三個字母,這是拉丁文Quod Erat Demonstrandum的縮寫,意思是「證明完畢」。現在的證明完畢符號,通常是(實心黑色正方形),稱之為「墓碑」或「哈爾莫斯(Halmos symbol)」(因保羅·哈爾莫斯最先採用此做法)。墓碑有時是空心的。另一個簡單方法是寫「proven」、「shown」或「證畢」之類的文字。
在數學上,證明是在一個特定的公理系統中,根據一定的規則或標準,由公理和定理推匯出某些命題的過程。比起證據,數學證明一般依靠演繹推理,而不是依靠自然歸納和經驗性的理據。這樣推匯出來的命題也叫做該系統中的定理。