1 历史渊源
1.1 古代逻辑的先声
1.1.1 亚里士多德的三段论
亚里士多德在《前分析篇》中首次系统表述了三段论。三段论是由两个前提推出一个结论的演绎形式，例如著名的“所有人都会死，苏格拉底是人，因此苏格拉底会死”。亚里士多德区分了每个命题的全称、特称、肯定、否定四种形式，并分辨出有效的格与式。虽然他用的是自然语言，但其推理规则已经隐含了形式化的思路。这段工作被视为逻辑学的起点，也为日后数理逻辑的符号化处理提供了范本。
1.1.2 斯多葛学派的命题逻辑萌芽
斯多葛学派在命题逻辑层面作出了重要贡献。他们系统研究了条件句（蕴含关系），讨论了“如果……那么……”真值条件的各种可能性。与亚里士多德关注范畴词不同，斯多葛更关注句子本身作为逻辑单元，并提出了类似于现代命题逻辑中析取与合取推理的规则。这种以句子为基本单位的思路，为后来将逻辑完全符号化埋下了伏笔。
1.2 近代符号化浪潮
1.2.1 莱布尼茨的“普遍语言”设想
莱布尼茨梦想创造一种“普遍语言”（characteristica universalis），使所有知识都可以用精确的符号表达，并配合一套“推理演算”进行无歧义的推演。他认为，一旦建立这样的系统，哲学争论就可以像数学计算那样迎刃而解。虽然他的设想在技术上未能实现，但这一方向激励了其后布尔、弗雷格等人将逻辑彻底数学化。
1.2.2 布尔代数与逻辑代数
乔治·布尔在《思维规律的研究》中将逻辑推理转化为代数运算。他用符号表示类或命题，用“与”“或”“非”对应乘法和加法，从而构建了布尔代数。例如，X·Y 表示 X 和 Y 同时为真，X+Y 表示 X 或 Y 为真。布尔的工作第一次赋予逻辑精确的代数结构，是符号逻辑的里程碑。他的代数后来成为数字电路的基础——所以每一个开关晶圆的故事里都有布尔。
1.3 二十世纪的大爆发
1.3.1 弗雷格的概念文字
戈特洛布·弗雷格于1879年出版《概念文字》，引入了一套二维符号系统来表示逻辑推理，第一次系统处理了量词和谓词。他定义了函数与自变元的区分，并将数学中的等式视为逻辑关系。弗雷格的系统是现代一阶逻辑的直接祖先，只不过他那套符号排版太像化学式了，以至于同时代的人觉得难以接受。
1.3.2 罗素与怀特海的《数学原理》
伯特兰·罗素与阿尔弗雷德·诺思·怀特海共同撰写了三卷巨著《数学原理》（1910–1913），试图从逻辑公理推导出全部数学。他们详细构建了类型论以避免悖论，并花费数百页推导出“1+1=2”。这部书因符号繁复、论证冗长而恶名远扬——但它的确证明了逻辑主义纲领的可行性，也为数理逻辑奠定了庞大的形式基础。据说该书出版后，罗素感叹“那几百页推导1+1=2，足够让数学家们闭嘴了”。
1.3.3 希尔伯特的形式主义计划
大卫·希尔伯特在20世纪初提出了形式主义纲领：将数学完全形式化为无歧义的符号系统，然后用有限的方法证明该系统不会产生矛盾（一致性），并且每一个真命题都可以被证明（完备性）。他相信“一切数学问题都可以被解决”。然而，哥德尔的不完备定理直接将这个梦想击碎：形式系统如果足够强大，就无法证明自己的一致性，也必然存在不可判定的命题。不过希尔伯特的劲头带来了证明论、元数学等重要研究方向。
2 基础逻辑系统
2.1 命题逻辑
2.1.1 语法：命题符号与联结词
命题逻辑的语法指定了什么是合法的公式。基本元素是命题符号（如 p, q, r），通常代表一个可以为真或假的句子。联结词包括否定（¬）、合取（∧）、析取（∨）、蕴含（→）和等价（↔）。由这些联结词和括号构造的复合公式递归定义：如果 φ 和 ψ 是公式，那么 ¬φ、φ∧ψ、φ∨ψ、φ→ψ、φ↔ψ 都是公式。
2.1.2 语义：真值表与重言式
命题逻辑的语义通过真值表给出：每个命题符号可被赋值为真（1）或假（0），联结词的真值由基本真值规则决定。例如，p→q 仅在 p 真而 q 假时为假，其余情况均为真。一个公式被称为重言式（永真式），如果它在所有可能赋值下都为真，如 p ∨ ¬p。重言式是逻辑真理的核心。
2.1.3 推理系统：自然演绎与公理化
自然演绎模仿人类自然的推理方式，以引入和消去规则（如 ∧-引入、→-消去）操作公式，可以从一组前提推演出结论。公理化系统则用少数公理和分离规则进行推导。两种系统在表达能力上等价，只是风格不同：自然演绎更亲民，公理化更适合元理论分析。
2.1.4 元性质：可靠性与完备性
可靠性是说：所有可证明的都是逻辑真（重言式）。完备性是说：所有逻辑真（重言式）都是可证明的。对于命题逻辑，这两个性质均已得证：任何合理的推理系统都满足可靠性，而完备性则需要证明对任意重言式存在一个证明。这确保了语法推导与语义真值之间的完美对齐。
2.2 一阶谓词逻辑
2.2.1 语法：个体词、谓词、量词
一阶逻辑在命题逻辑基础上增加了个体变元（如 x, y）、个体常元（如 0）、函数符号（如 f(x)）和谓词符号（如 P(x)）。量词包括全称量词 ∀ 和存在量词 ∃。公式由原子公式（如 P(x)）通过联结词和量词迭代构成。一阶逻辑的“一阶”含义是量词只能作用于个体变元，而不能作用于谓词或函数。
2.2.2 语义：模型与真值赋值
语义通过模型定义。模型是一个结构，包含一个非空论域和各个符号的解释。公式的真假由在模型中对变元的指定来判定。例如，∀x P(x) 在模型 M 中为真，当且仅当论域中的每一个元素都在 P 的解释中。一阶逻辑的语义使得我们可以谈论“在所有模型中均真”的逻辑真理。
2.2.3 自由变元与约束变元
量词的出现决定了变元的角色。在 ∀x P(x) 中，x 是约束变元，其意义由量词限定。若一个变元不在任何量词的辖域内，则为自由变元。例如在 P(x) ∧ ∀y Q(y) 中，x 是自由的，y 是约束的。只有闭合公式（无自由变元）才具有绝对的逻辑真值。自由变元使得公式像属性描述而非具体断言。
2.2.4 前束范式与斯科伦化
所有一阶公式都可以通过量化前移转换成前束范式：所有量词出现在公式最前面，后接一个无量词矩阵。进一步，通过斯科伦化可以消去存在量词：引入新的函数符号（斯科伦函数）来表示对于每个 ∃x，存在某个依赖全称变元的实例。斯科伦化在自动定理证明中非常有用——它把一阶公式转换成等可满足的仅含全称量词的公式。
2.2.5 哥德尔完备性定理
哥德尔在1929年证明了：一阶逻辑在标准推理系统中是完备的。即，任何一个一阶逻辑的普遍有效公式（在每个模型中都为真）都可以在公理化系统中推导出来。这意味着语法和语义再次完美匹配。不过，不要与哥德尔不完备定理混淆：完备性话说的是逻辑本身，而不是包含算术的公理系统。
2.3 高阶逻辑与类型论
2.3.1 二阶逻辑的强度与局限
二阶逻辑允许量化谓词和函数（即变量可以代表集合或关系）。这使得它可以非常简洁地表达数学概念——比如可以用一个二阶公式刻画自然数结构的唯一性（而一阶逻辑做不到）。但代价是：二阶逻辑没有完备的推理系统（紧致性和完备性均失效），且其元理论比一阶逻辑复杂得多。所以大多数数学公理系统宁愿用一阶逻辑作为基础框架。
2.3.2 简单类型论与范畴逻辑
简单类型论由罗素为避开悖论而提出，后经丘奇发展为λ演算的一种形式。它将个体、集合、集合的集合等分成不同“类型”，函数和谓词应用必须遵循类型规则。这一思想直接影响了函数式编程语言（如Haskell）。范畴逻辑则用范畴论的语言统一逻辑与数学结构，将类型视为对象，证明视为态射，实现了抽象层面的逻辑统一。
3 模型论
3.1 基本概念
3.1.1 结构、解释与满足
模型论研究语言在具体结构中的解释。一个结构包含一个论域和一组对谓词、函数、常元的赋值。给定公式 φ 和一个赋值（将变元映射到论域），如果在该结构下 φ 为真，则称该结构满足 φ。所有满足公式集 Γ 的结构构成的类，称为 Γ 的模型类。
3.1.2 同构、初等等价与紧致性
如果两个结构之间存在一一对应且保持所有函数与谓词解释，则称它们同构。如果两个结构满足完全相同的所有一阶句子，则称它们初等等价——同构蕴含初等等价，但反之不真（例如有理数序结构与实数序结构是初等等价的，但它们不同构紧致性定理是模型论的核心定理：如果一个公式集的所有有限子集都有模型，那么该公式集整体也有模型。这一定理在构造非标准模型时至关重要。
3.2 经典模型构造
3.2.1 昂西-瓦尔定理与类型省略
昂西定理（由昂西等人证明）给出了一个理论有无限模型的充分必要条件。瓦尔定理则关于类型省略：给定一个类型（一组公式，其中变元自由），如果它在某结构中不实现，则可以通过技术手段构造一个省略了该类型的新结构。类型省略是模型论构造特定性质结构的有力工具。
3.2.2 超积与超幂构造
超积是模型论中最著名的构造之一。选取一族结构，在它们的积上利用一个超滤子（一种“几乎处处”的概念）取商，就得到一个新结构。超积可以“放大”原结构的性质，并常用于证明紧致性定理。超幂则是取同一结构的超积——它会生成一个通常不同构于原结构的“放大版本”，比如非标准自然数模型。
3.3 应用与趣闻
3.3.1 模型论与代数（如代数闭域理论）
代数闭域的一阶理论是一个重要的例子。所有特征0的代数闭域（如复数域）共享完全相同的一阶性质。利用模型论，可以证明代数闭域理论具有量词消去性质（每个公式等价于一个无边界的公式），从而可以高效地判断代数命题的真假。模型论还为超积在代数几何中的应用提供了途径。
3.3.2 模型论中的“非标准模型”梗（比如非标准自然数）
紧致性定理的一个著名推论是：自然数算术 (ℕ, +, ×) 存在非标准模型，里面包含“无穷大自然数”（严格大于所有标准自然数的元素）。这些模型仍然满足一切一阶算术公理。想象一下：你明明在写自然数，却悄悄藏着像“∞+1”这样的大家伙，而且它们还要满足结合律和交换律。这个事实也说明一阶公理无法唯一刻画标准自然数，成为模型论人拿来坑朋友的常见段子。
4 证明论
4.1 形式化证明系统
4.1.1 希尔伯特风格演算
希尔伯特演算（又称希尔伯特系统）以尽可能少的公理和推理规则为核心。通常只有一条推理规则（分离规则，modus ponens），公理则是一组选定的重言式。这种系统虽然推导冗长，但元理论分析往往更简洁。充分多的公理保证了完备性，但需要高度技巧才能进行简单推理。
4.1.2 根岑的序列演算与自然演绎
格哈德·根岑在20世纪30年代提出了自然演绎和序列演算。自然演绎更接近日常思考：每个逻辑联结词都有引入规则和消去规则，比如“如果从 φ 推出 ψ，则你可以引入 φ→ψ”。序列演算则更结构化：每个推导涉及一个序列 Γ ⊢ Δ（Γ 为前提集，Δ 为结论集），并对称地包含左右推广规则。序列演算的明显优势是切消定理。
4.1.3 切消定理（Hauptsatz）
根岑的切消定理是证明论的核心成果：如果一个公式在序列演算中有证明，那么存在一个不含“切规则”的证明。切规则本质上是演绎链的传递性（从 Γ ⊢ Δ, A 和 A, Σ ⊢ Π 推出 Γ, Σ ⊢ Δ, Π）。去掉切意味着证明变得更直接、更局部。切消定理在一致性证明中扮演关键角色。
4.2 一致性证明
4.2.1 算术的一致性：哥德尔不完备定理的阴影
哥德尔第二不完备性定理说：如果一个形式系统足够强大（能表达皮亚诺算术），且一致，则它无法证明自身的一致性。这意味着任何在系统内部证明一致性的尝试都会失败。证明论只好退而求其次，使用更强的元理论来证明较弱理论的一致性。于是，你不小心在证明一个理论一致性时，会发现自己已经使用了比该理论更强大的方法——这就像抓着鞋带把自己拎起来。
4.2.2 序数分析与皮亚诺算术的再证
为了绕过不完备定理，证明论引入了序数分析。方法的思路是：将理论的证明递归证明论序数（一个超穷序数），证明递归深度小于该序数的推导不会引出矛盾。例如，皮亚诺算术的证明论序数是 ε₀（第一个满足 ω^ε = ε 的序数）。通过超穷归纳，可以在更强的元理论下给出皮亚诺算术的一致性子证明。这一领域至今仍有活跃研究。
4.3 证明复杂性
4.3.1 证明长度与计算资源
证明复杂性关心一个逻辑命题的最短证明有多长，与证明系统本身有关。不同证明系统在最短证明长度上可能相差很大——例如某些命题在弗雷格系统中短短几行，在希尔伯特系统中可能需要天文数字的行数。这一点与计算机科学中的计算复杂性直接呼应。
4.3.2 多项式有界证明与可行证伪性
如果一个证明系统使得所有真命题都存在长度受限于某个多项式的证明，则称该系统为多项式有界的。但研究表明，许多自然系统（如扩展弗雷格系统）是否多项式有界是开放问题。这与NP与co-NP问题相关：如果一个系统有界，则co-NP=NP。所以证明复杂性中经常埋着“如果证明了那个，你就顺便解决了P vs NP”的彩蛋。
5 递归论与可计算性
5.1 图灵机与可计算函数
5.1.1 图灵机的标准模型
图灵机由艾伦·图灵于1936年提出，是计算的最基本抽象。一台图灵机有有限数量的状态、一个无限长的纸带和读写头。每一步根据当前状态和读到的符号执行一个动作（写符号、移头、改状态）。尽管结构极简，图灵机可以模拟任何已知的计算过程。一台万能图灵机可以模拟任意图灵机——这也是现代计算机的雏形。
5.1.2 丘奇-图灵论题
丘奇-图灵论题断言：任何在直觉上可计算（或“有效可计算”）的函数都可以被图灵机计算。这不是一个可证明的定理，而是一个被广泛接受的定论——因为许多替代形式化（λ演算、递归函数、图灵机）都被证明等价，且从未发现反例。它设定了一个边界：算法能做什么、不能做什么。
5.2 不可判定问题
5.2.1 停机问题与对角线论证
停机问题问：是否存在一个算法，能够判定任意图灵机在任意输入上是否会最终停机？图灵通过对角线论证证明这样的算法不存在。假设存在一个判定停机问题的算法 H，则构造一台新机器：如果 H 说输入会停机，则它进入死循环；否则停机。然后对这台机器输入它自己的描述，立即产生矛盾。所以停机问题不可判定。
5.2.2 波斯特对应问题与不可判定的“段子”
波斯特对应问题（PCP）是另一个著名的不可判定问题：给定若干对字符串，问能否将若干对拼接成两个相同的长字符串。这听起来像拼字游戏，却是一个不可判定的问题。这段子是递归论课上拿来敲打新生的：看看这些该死的瓷砖，你永远无法确保能拼出来。
5.3 递归分层与度结构
5.3.1 算术分层与图灵度
算术分层将可判定性划分为不同层次：Σₙ₀ 和 Πₙ₀ 分别表示含有 n 层量词交替的公式，而 Δₙ₀ 同时属于两者。可计算性的更深层次是图灵度：将自然数上的函数按照相对可计算性分类，形成的偏序结构极其丰富。所有可计算函数处于0度，而停机问题的度（0'）是第一个非递归的图灵度。
5.3.2 优先方法与非递归结构
优先方法是递归论中构造特定图灵度的标准技术：通过逐步近似并满足无穷的“需求”，同时在冲突时安排优先级。它被用来证明许多关于图灵度的结构性质——比如存在不可比较的度（无信息的两个集合互相不可计算）。这些构造精致复杂，常被描述为“算法上的博弈”。
6 集合论
6.1 朴素集合论的悖论
6.1.1 罗素悖论与理发师梗
罗素悖论指出：考虑“所有不包含自身的集合的集合” R——R 包含 R 当且仅当 R 不包含 R，直接产生矛盾。这击穿了朴素集合论“任意性质都能构造集合”的想法。罗素搞了个通俗版：村里有一个理发师，只给那些不自己刮胡子的人刮胡子——那么理发师自己刮不刮胡子？答案是：他既不能刮，也不能不刮。这个悖论催生了公理集合论的严格化。
6.1.2 康托尔的朴素集合与对角线论证
格奥尔格·康托尔用对角线论证证明了实数集不可数——任何自然数到实数的映射都会漏掉一个实数。对角线法也成了递归论、模型论中反复使用的工具。康托尔的工作在当时被很多数学家视为“疯狂”，但后来成为集合论的基石。
6.2 ZFC公理化集合论
6.2.1 外延公理、并集公理、幂集公理等
ZFC（Zermelo-Fraenkel 集合论加选择公理）是一组公理，规避了罗素悖论。外延公理断言：集合由它的元素唯一确定。对空集、配对集、并集、幂集、无限集等均有公理。替换公理允许通过函数关系替换集合的元素来构造新集合。正则公理禁止“集合包含自身”的降序链，从而排除不自然的结构。
6.2.2 选择公理与连续统假设
选择公理（AC）说：对任意一个由非空集合组成的族，存在一个集合恰好从每个族内选择诸元素。它在数学中有广泛应用（例如每个向量空间有基底），但也导致一些反直觉结论（如巴拿赫-塔斯基悖论）。连续统假设（CH）断言不存在大小严格介于自然数集和实数集之间的集合。二者在ZFC中独立（既不可证也不可证伪），哥德尔和科恩分别证明了它们的相对一致性。
6.3 大基数与力迫法
6.3.1 不可达基数、可测基数
大基数公理断言存在某些很大的基数，以至于普通ZFC无法证明其存在。不可达基数是正则且不可数的强极限基数，超限的“墙”第一次出现。可测基数比不可达基数更大：存在一个非平凡的超滤子可以“测算”可测基数上的子集。大基数公理层次上无穷丰富，从弱到强构成一条“大基数链条”。
6.3.2 科恩力迫与独立性证明
保罗·科恩发明力迫法，通过构造新的集合论模型来证明给守恒独立性。例如，他证明ZFC无法证明或否定CH：在力迫扩张中，他可以任意调整实数的个数，而保持ZFC公理成立。力迫法是数学中最强大的独立性工具之一，也被用于解决许多其他问题（如选择公理的独立性）。
6.4 集合论中的“有趣”宇宙
6.4.1 可构造宇宙L
库尔特·哥德尔定义了可构造宇宙 L：从空集开始，在每一步递归地添加所有可以用一阶公式定义出来的子集。L满足ZFC和连续统假设，并且是一个极小模型。在任何外力迫扩张中，L都是“内层模型”。大基数在L中的存在性会减弱，但L是研究集合论相对一致性的标准工具。
6.4.2 大基数与武丁基数
武丁基数是更强大的一种大基数，它关于可测性具有极高的闭包性质。武丁基数在描述集合论和确定公理（AD）的研究中是关键对象。一些数学家认为，通过引入大基数作为公理，可以为实数投影集的行为提供非常丰富的结构，甚至可以解决CH以外的许多经典问题。
7 数理逻辑的跨界应用
7.1 计算机科学
7.1.1 自动定理证明与逻辑编程（Prolog）
自动定理证明使用命题逻辑和谓词逻辑的推理算法来自动导出一个命题的证明或反例。例如分辨率法是基于一阶逻辑的机器证明引擎。Prolog 是一种基于霍恩子句的逻辑编程语言：程序员只需描述事实和规则，由引擎通过回溯和合一完成推理。Prolog 经常被用来解数独、处理自然语言，甚至实现专家系统。
7.1.2 类型系统与程序验证
类型系统源于逻辑中的类型论，确保程序的正确性。例如强类型语言在编译时就拦截了类型错误。更高级的依赖类型语言（如 Coq、Agda 或 Lean）允许用逻辑公式作为类型，程序员写出程序的证据性证明，证明其行为符合规范。这就是“Curry-Howard 对应”——程序与证明本为一体。
7.2 哲学与语言学
7.2.1 模态逻辑与可能世界语义
模态逻辑研究必然与可能：公式 □φ 意思为“φ是必然的”，◇φ 意为“φ是可能的”。克里普克提出的可能世界语义学为模态逻辑提供了严格的模型论：每个世界是一个可能状态，全称/存在量词类似地穿越世界。这一框架被广泛用于哲学形而上学和认知科学。
7.2.2 动态逻辑与认知逻辑
动态逻辑将程序行为形式化：[α]φ 表示“执行程序 α 后 φ 成立”；⟨α⟩φ 表示“存在一个 α 的合法执行使 φ 成立”。它用于描述和推理指程序。认知逻辑则引入“知道”算子 Ka φ（代理人 a 知道 φ），处理知识和信念的逻辑结构，在人工智能、博弈论、密码协议分析中至关重要。
7.3 跨界“梗”与逸闻
7.3.1 布尔逻辑在键盘上的狂欢
布尔代数在数字电路里无处不在。每个逻辑门的真值表都可以对应一个简单的物理实现。于是，键盘上每一个键按下实际上是一场布尔运算的狂欢：按键产生一个二进制信号，与门、或门、非门在微处理器里迅速过一遍，最终将你的字母显示在屏幕上。所以说没接触过数理逻辑的人，其实每天也在给布尔打工。
7.3.2 哥德巴赫不睡觉：不完备性的幽默解读
哥德尔不完备定理常常被拉出来开玩笑：“世界上有两种系统，不一致的和不完整的。哦，还有第三种——那些自称完整的，其实只是不自洽。”或者：“如果一个形式系统证明了它的自洽性，那么它其实是不自洽的（根据哥德尔第二不完备定理）。”所以每个公理系统最后的命运都是——要么漏东西，要么炸掉。
8 当前前沿与开放问题
8.1 极限消去与逆数学
逆数学是证明论的一个分支：它试图确定数学定理所需的公理强度。不再是“从公理推导定理”，而是“已知定理，需要多强的公理才能证它”。例如一些基本定理等价于算术公理的某个片段，而一些较高阶定理等价于更强的存在公理。极限消去则研究了在超限归纳法中如何消去高序数假设，从而揭示定理真实逻辑力量。
8.2 可计算模型论与结构复杂性
可计算模型论研究可计算结构及其模型的可计算性特征。例如，能否在算法上判定一个结构是否包含同构子结构？结构复杂性的层次如何与计算复杂性对应？该领域现在依旧活跃，尤其是关于随机图、代数闭域的可计算模型的构造。其中许多问题仍然悬而未决，比如是否存在一个可计算的代数闭域，其中每个可计算子域都是可计算的？
8.3 同伦类型论与数学新基础
同伦类型论（HoTT）将类型论与同伦论结合，引入“路径空间”概念，将等式视为一个结构——命题的证明可以不是唯一的，而是像连续变形那样形成一个高阶结构。这种观点为实现新型数学基础（Univalent Foundations，单值性基础）提供了可能，它许诺更自然的计算机证明辅助。这一理论仍在飞速发展，能否真正取代传统集合论的基础地位还未知——但至少它在证明辅助系统中的应用已经很热闹了。