上帝所做的、勝過一切想象中的幸福行為，莫過于純粹的思考，而人的行為
中最接近這種幸福的東西，也許是與思考最密切的活動。
?
——亞里士多德
邏輯作為一種思維和認知方式，對現代人的學習和生活都是必不可少的。人們日常的交流討論需要邏輯；新知識、新技能的學習需要邏輯；保障人們有序生活、工作的各種規章制度、法律條文的表述也都基于邏輯。邏輯在人們學習、工作和生活中的重要作用已得到廣泛認可，許多家長都注重從小培養孩子的邏輯思維能力。那么，究竟什么是邏輯呢？
邏輯（英文logic）一詞來源于古希臘語（λογικ?），其最初的意思是“話語”，之后逐漸被用于描述思考或推理的過程和方式，即通過一些確定的思維“模式”建立起連接假設與結論的紐帶。這種樸素的思考和推理方式長期被古希臘學者用于演講和辯論。而后逐漸被人們用于哲學、數學以及各種自然科學的研究。
 |
圖1 邏輯方陣（15世紀）
邏輯含義的演化反映了人們對思維認識的深化。古希臘思想家認為，只有通過這種“邏輯”思考才能領悟物質世界的實質和精髓。柏拉圖認為，人可以通過對物質世界的觀察抽取基本真理，再通過理性的（邏輯）思考探究世界的規律。正是通過這種“思考”，人們能夠從正確的前提出發，獲得正確可靠的結論。更進一步，亞里士多德認為，邏輯是自然科學研究的基礎，因而需要將“理性的思考”與具體物質世界的真理相分離。為此，他提出了著名的三段論、反證法等邏輯推演法則。
亞里士多德所開創的邏輯也被稱為亞里士多德邏輯，在隨后近兩千年的歷史進程中廣為傳播，長期被人們視為哲學思考和研究的基本思維方式，促進了自然科學的發展。特別是對于數學的發展，它起到了至關重要的作用：指明了從公理和定義出發，由邏輯推理建立一套嚴格理論體系的途徑和方法。正是基于這種邏輯推理的方法，歐幾里得的《幾何原本》才成了構建數學知識大廈的不朽典范。
 |
圖2 1573年版《幾何原本》
十七世紀后期，德國數學家戈特弗里德·威廉·萊布尼茨首先提出，要建立一種“通用的形式語言”，用于描述數學推理。在這種語言中，每個概念都應該用一個符號表示；這樣，抽象的“思維過程”就可以通過機械的“符號演算”來處理。盡管萊布尼茨沒有明確給出現代邏輯的表示方式，但他提出的這種形式語言和符號演算的思想卻正是現代數理邏輯的主要特征。
到了十九世紀中葉，邏輯終于從“論證”的手段轉變為處理數學問題的系統方法。1854年，喬治·布爾出版了《The Laws of Thought》，首次從代數系統的角度闡述了邏輯推演方法。布爾接受了亞里士多德邏輯的主要觀念，并對傳統邏輯進行了系統化推進：擴展了命題的數量，提供了抽象的邏輯推演規則，加入了數學最基本的符號，等等。該代數系統就是著名的布爾代數，它是現代命題邏輯和計算機科學的基礎。
1879年，戈特洛布·弗雷格發表了《概念文字》（Begriffsschrift）。他在命題邏輯中引入量詞（“全部（任意）”、“一些（存在）”）符號，將原本簡單的命題符號擴充為帶有量詞的謂詞語句。這種擴展大大增強了邏輯的表達能力，使得許多數學分支都可以由該（一階）邏輯系統的形式語言去刻畫。例如，基于若干公理構建的自然數算數系統（皮亞諾算術）就可以通過一階邏輯完全刻畫（見圖4）。至此，“數理邏輯”的概念和理論逐步形成。
 |
圖3 皮亞諾算數公理的一階邏輯表示
數理邏輯是用數學方法研究邏輯的學問，它既包含數學推理的抽象規則，又為具體數學知識的描述提供形式語言，是現代數學必不可少的組成部分。
隨著數學知識的不斷擴充，要將所有數學結論列舉出來似乎并不可行。人們轉而期望能夠選擇有限多個不證自明的數學論斷作為初始公理，通過邏輯推理獲得所有其他數學結論。1900年，戴維·希爾伯特在巴黎國際數學家大會上作了題為《數學問題》的報告，提出了23個著名的數學問題。其中第二個問題就是希望能以嚴謹邏輯推理的方式證明任意公理系統內命題的相容性（一致性）。
1910年到1913年，伯特蘭·羅素和他的老師阿爾弗雷德·懷特海德合著了《數學原理》，期望根據有限的數學公理，通過與具體領域無關的邏輯推理獲得各個數學領域中的全部真理。這就要求數學公理系統具有兩個重要性質：可靠性（即所有可證的數學命題都是正確的）和完備性（即所有為真的數學命題都是可證的）。
1929年，庫爾特·哥德爾證明了一階邏輯系統自身的完備性，其可靠性也可以證明。看上去，一切似乎都十分順利。然而，在1931年他又證明了著名的哥德爾不完備定理，指出皮亞諾算數系統具有不完備性，從根本上否定了通過嚴格邏輯證明獲得全部數學定理的可能性；稍微復雜些的數學公理系統（如包含皮亞諾算術的公理系統）都會存在不能被證明的命題。這一結論擊碎了幾代數學家的夢想，同時也說明了形式化語言的局限性。
1936年和1937年，阿隆佐·邱奇和艾倫·麥席森·圖靈基于各自的計算模型——lambda演算和圖靈機，再次從可計算的角度分別獨立地給出了希爾伯特第二問題的否定答案，即，不存在一個通用的算法，它可以用于判定任何一個數學命題是否為真。
 |
圖4 不完備定理的經典對角線構造
盡管哥德爾、邱奇和圖靈對數學公理系統的完備性給出了否定答案。然而，他們的工作卻為數學研究打開了另外一扇大門——可以根據具體需要選擇恰當的斷言作為初始公理，使得數學向著更為廣闊的領域發展。目前，數理邏輯正在沿著四個相互獨立卻又內部關聯的方向——模型理論、證明理論、可計算性和集合論——不斷發展，繼續夯實現代數學和計算機科學的理論基礎。
隨著計算機和移動設備計算能力的不斷提升，數理邏輯在定理自動證明、程序驗證、知識管理、數學計算中的作用日益突顯，為數學機械化、算法數學、計算機應用、人工智能等學科之間的立體交叉提供了基石、架起了橋梁；同時，數學與計算機科學的交叉融合也在促使數理邏輯自身不斷地向前發展。
（文中圖片來自百度百科、維基百科等網上資料；感謝阿狗數學AlgoMath的老師和同學們對文章內容、措辭的修改和建議）
（北京林業大學信息學院 蔣東辰）
阿狗數學（AlgoMath）:
阿爾法狗（AlphaGo）多次擊敗世界頂級圍棋高手，彰顯了人工智能在圍棋領域的成功應用。阿爾法狗中的軟件程序（算法數學）就是阿狗數學。
阿狗數學，誕生于2017年11月11日。英文名是AlgoMath，取Algorithm（算法）與Mathematics（數學）兩詞的前四個字母構成。所謂算法，泛指解決特定類型問題的意義清晰的指令，此處特指可以解決具體問題的易于實現的計算機指令。數學則是泛指對數量、結構、空間與變化等概念進行研究的一門學科。而算法數學是計算機算法與數學研究的交叉領域，指數學理論與方法的算法化、機械化與自動化。
顧名思義，阿狗數學的特長不是下圍棋，而是計算機算法與數學理論的交叉與融合，是數學理論與方法的算法化。他的這個特長源自他的老祖宗──中國古代數學。正如數學泰斗吳文俊先生所言：“中國古代數學就是一部算法大全”，“中國古代數學的特點就是構造性和機械化”。誠然，中國古代的數學走著與西方公理體系不同的道路，發展出更相減損術（計算最大公因子）、盈虧術（線性差值法）、大衍術（解同余方程）等一系列構造性數學算法。
基于算法數學，1976年用計算機成功證明了四色定理，1980年前后用吳方法實現了計算機上自動證明幾何定理。隨著計算機計算能力的大幅增強以及代數幾何、數理邏輯等數學理論的不斷深入，算法數學得到了而快速發展、強化，阿狗數學就是其中在一個顯劇成果。
阿狗數學的興趣就在這構造性數學的理論與方法，包括相關算法的設計與實施、復雜性理論與實驗分析。他感興趣的研究領域包括符號計算、可信數值計算、統計計算與分析、自動推理、知識發現等當今最前沿的理論計算機科學與應用數學學科，所要涉及到的數學知識包括數理邏輯、離散數學、數值逼近、概率統計、組合優化、方程求解、代數計算、公式推導、定理證明、可靠性分析以及復雜性估計，等等。
阿狗數學既敬仰笛卡爾意欲將一切問題歸結為解決代數方程組的宏偉藍圖，又贊賞著名代數幾何學家S.Abhyankar《Polynomials and power series》（多項式與冪級數）一詩中的豪言壯語，但也深知構造性數學與存在性數學的依存與共榮關系。阿狗數學充滿豪情而又不失理智地誕生于這瞬息萬變、激昂豪邁的信息世界舞臺，我們期望他舞出更精彩的人生（狗生）大劇！
