数理逻辑（Mathematical Logic），又称符号逻辑（Symbolic Logic），是数学的一个分支，它将逻辑推理用数学符号和形式化方法表示和研究。数理逻辑是现代数学和计算机科学的理论基础，对人工智能、语言学、哲学等领域也有深远影响。
数理逻辑是使用形式化方法研究逻辑推理的学科。与传统的形式逻辑不同，数理逻辑使用精确的数学符号系统代替自然语言，使得推理过程可以被严格分析和机械化。其核心思想是：将推理转化为符号演算（calculus of reasoning），从而将哲学思辨转化为数学计算。
数理逻辑的主要特征包括：
数理逻辑在数学中的地位类似于"数学的基础工程"——它不是研究某个具体的数学对象（如数、函数、空间），而是研究数学推理本身的规则和极限。这种元层面的视角使得数理逻辑在20世纪初的数学基础危机中扮演了核心角色，并深刻影响了计算机科学的诞生。
数理逻辑的发展经历了几个关键阶段，每一个阶段都有标志性的人物和突破：
萌芽期（17-19世纪）：
莱布尼茨（Gottfried Wilhelm Leibniz, 1646-1716）最早提出"普遍语言"（Characteristica Universalis）和"推理演算"（Calculus Ratiocinator）的设想。他设想创造一种通用的符号语言——类似于二进制编码的前身——使得所有推理都能通过计算完成："Calculemus！"（让我们计算！）。这个被称为"莱布尼茨之梦"的设想，是数理逻辑和人工智能的思想源头，比他那个时代超前了两个多世纪。
乔治·布尔（George Boole, 1815-1864）创立了布尔代数（Boolean Algebra），将逻辑推理代数化。在他的代表作《思维定律的研究》（An Investigation of the Laws of Thought, 1854）中，布尔用代数系统表示命题的真假运算，将"且"、"或"、"非"分别对应为代数中的乘、加和补运算。布尔代数至今仍是数字电路设计、数据库查询优化和编程语言类型系统的基础。
德·摩根（Augustus De Morgan, 1806-1871）提出了著名的德·摩根定律（De Morgan's Laws）：¬(A ∧ B) ≡ ¬A ∨ ¬B 和 ¬(A ∨ B) ≡ ¬A ∧ ¬B，并系统研究了关系逻辑，为后来一阶逻辑中的关系演算奠定了基础。
奠基期（19世纪末-20世纪初）：
弗雷格（Gottlob Frege, 1848-1925）在《概念文字》（Begriffsschrift, 1879）中首次建立了完整的谓词逻辑系统，被广泛认为是现代数理逻辑的真正开端。他引入了量词和变元的概念，并设计了一套二维符号系统来表示逻辑关系。弗雷格还试图将算术还原为纯粹的逻辑（逻辑主义），这项工作成为罗素和怀特海《数学原理》的直接先导。
皮亚诺（Giuseppe Peano, 1858-1932）建立了自然数的公理系统（皮亚诺公理），并发明了许多现代逻辑符号，包括我们今天仍在使用的 ∈（属于）、⊃（蕴含）等符号。他的符号系统对后来的数学符号标准化产生了重要影响。
伯特兰·罗素（Bertrand Russell, 1872-1970）发现了罗素悖论（Russell's Paradox）——"所有不属于自身的集合的集合"是否属于自身？这一悖论撼动了朴素集合论的基础，直接推动了公理集合论的发展。罗素与怀特海合著的三卷本《数学原理》（Principia Mathematica, 1910-1913）试图将全部数学建立在逻辑基础上，以类型论（Theory of Types）避免悖论。这部巨著虽然在后来的发展中被视为并非完全成功，但作为形式化数学的极致尝试，至今仍是数理逻辑史上的里程碑。
成熟期（20世纪）：
大卫·希尔伯特（David Hilbert, 1862-1943）在20世纪20年代提出了著名的希尔伯特计划（Hilbert's Program），试图用有限的、有穷的数学方法证明整个数学系统的一致性和完备性。这一计划推动了证明论的诞生和发展。在1928年的国际数学家大会上，希尔伯特提出了一系列开放问题，其中包含判定问题（Entscheidungsproblem），直接推动了图灵和丘奇的工作。
库尔特·哥德尔（Kurt Gödel, 1906-1978）的不完备性定理（1931）彻底改变了数学基础的面貌。第一不完备性定理证明：任何包含皮亚诺算术的一致公理系统都是不完备的——存在数学真理不能在该系统中证明。第二不完备性定理证明：这样的系统不能证明自身的一致性。哥德尔的工作粉碎了希尔伯特计划的核心理想，但同时也开启了数理逻辑的新时代。
阿尔弗雷德·塔尔斯基（Alfred Tarski, 1901-1983）建立了模型论的基础，定义了真值的形式化概念（塔尔斯基可定义真值理论），并证明了著名的塔尔斯基不可定义性定理。他的工作为形式语义学树立了标准。
阿隆佐·丘奇（Alonzo Church, 1903-1995）和艾伦·图灵（Alan Turing, 1912-1954）分别提出了λ演算（Lambda Calculus）和图灵机（Turing Machine）模型，奠定了可计算性理论的基础。图灵的停机定理证明了判定问题的不可解性，丘奇则独立证明了类似结果（丘奇定理）。他们提出的计算模型等价（丘奇-图灵论题）是理论计算机科学的核心基石。
数理逻辑通常包括以下几个核心分支：
| 分支 | 研究对象 | 核心问题 | 创立者/先驱 |
|---|---|---|---|
| 命题逻辑 | 命题之间的逻辑关系 | 真值表、逻辑等价、范式 | 布尔、弗雷格 |
| 谓词逻辑 | 谓词、量词和个体变元 | 有效推理、前束范式 | 弗雷格（1879） |
| 证明论 | 数学证明的形式化 | 一致性、完备性 | 希尔伯特、根岑 |
| 模型论 | 形式语言与数学结构 | 可定义性、紧致性 | 塔尔斯基、罗宾逊 |
| 可计算性理论 | 可计算函数和判定问题 | 停机问题、不可判定性 | 图灵、丘奇、哥德尔 |
| 集合论 | 集合的公理化 | 连续统假设、选择公理 | 康托尔、策梅洛、弗兰克尔 |
这些分支并非彼此孤立，而是相互交织。例如，哥德尔完全性定理连接了模型论和证明论；不完备性定理则横跨所有分支，揭示了形式系统本身的极限。
命题逻辑（Propositional Logic），又称命题演算（Propositional Calculus），是数理逻辑中最基础的部分，研究由原子命题（atomic propositions）通过逻辑联结词（logical connectives）构成的复合命题之间的推理关系。命题逻辑不关心命题的内部结构，只关心命题之间的真假关系——这正是其名称中"命题"的含义。
与谓词逻辑不同，命题逻辑不包含量词和个体变元，这使得命题逻辑的表达能力有限，但正因如此，它拥有优良的元性质：可判定性、可靠性和完备性。
命题（Proposition）是一个可以判断真假的陈述句。命题的真假称为其真值（Truth Value），通常用 T（True, 真）和 F（False, 假）或 1 和 0 表示。
命题示例：
原子命题是不可再分解的最小命题单位，通常用 p, q, r, ... 表示。命题变量是形式化中的基本单元——类似代数中的 x, y, z。
逻辑联结词（Logical Connectives）将简单命题组合成复合命题。标准的五个联结词如下：
| 联结词 | 符号 | 名称 | 定义 |
|---|---|---|---|
| 否定 | ¬p / ~p / ┐p | 非 | p为假时¬p为真 |
| 合取 | p ∧ q | 与 | p和q都真时真 |
| 析取 | p ∨ q | 或 | p和q至少一个真时真 |
| 蕴含 | p → q / p ⇒ q | 如果…则… | p真q假时为假 |
| 双条件 | p ↔ q / p ⇔ q | 当且仅当 | p和q同真或同假时为真 |
重点：蕴含连接词的真值表（material implication / 实质蕴含悖论）：
p → q 只在 p 真 q 假时为假，在其他三种情况（p假q假、p假q真、p真q真）下均为真。这意味着"假命题蕴含任何命题"（Ex Falso Sequitur Quodlibet）。这在日常语言中可能违反直觉（比如"如果太阳从西边出来，那么我是总统"在逻辑上竟然是真的），但在形式逻辑中是合理的——因为从假的前提可以逻辑地推出任何结论（爆炸原理）。
联结词的完备集：实际上，所有布尔函数都可以只用一种联结词表示。例如 NOR（↓）和 NAND（↑）各自都是完备的——这就是为什么数字电路中可以只用NAND门构建任何电路。
真值表（Truth Table）是枚举命题公式在所有可能赋值下的真值情况的表格。真值表是命题逻辑的基本决策工具。
复合命题的真值表示例：验证德·摩根定律 ¬(p ∨ q) ↔ (¬p ∧ ¬q)
| p | q | p∨q | ¬(p∨q) | ¬p | ¬q | ¬p∧¬q | ¬(p∨q)↔(¬p∧¬q) |
|---|---|---|---|---|---|---|---|
| T | T | T | F | F | F | F | T |
| T | F | T | F | F | T | F | T |
| F | T | T | F | T | F | F | T |
| F | F | F | T | T | T | T | T |
最后一列全为 T，证明该公式是永真式（Tautology），即德·摩根定律成立。
逻辑等价（Logical Equivalence）：如果两个命题公式在所有真值赋值下都有相同的真值，则称它们逻辑等价，记为 A ≡ B。
重要的逻辑等价式（每一个在真值表验证中都成立）：
| 名称 | 形式 | 直观含义 |
|---|---|---|
| 双重否定律 | ¬¬p ≡ p | 否定之否定 |
| 幂等律 | p ∧ p ≡ p, p ∨ p ≡ p | 重复无意义 |
| 交换律 | p ∧ q ≡ q ∧ p, p ∨ q ≡ q ∨ p | 顺序无关 |
| 结合律 | (p∧q)∧r ≡ p∧(q∧r), (p∨q)∨r ≡ p∨(q∨r) | 括号可重组 |
| 分配律 | p∧(q∨r) ≡ (p∧q)∨(p∧r), p∨(q∧r) ≡ (p∨q)∧(p∨r) | 且对或的分配 |
| 德·摩根定律 | ¬(p∧q) ≡ ¬p ∨ ¬q, ¬(p∨q) ≡ ¬p ∧ ¬q | 否定的分配 |
| 蕴含律 | p → q ≡ ¬p ∨ q | 蕴含的本质 |
| 假言易位 | p → q ≡ ¬q → ¬p | 逆否命题等价 |
| 双条件律 | p ↔ q ≡ (p → q) ∧ (q → p) | 双向蕴含 |
| 吸收律 | p ∧ (p ∨ q) ≡ p, p ∨ (p ∧ q) ≡ p | 吸收冗余信息 |
| 三段论 | (p → q) ∧ (q → r) → (p → r) | 蕴含传递性 |
永真式（Tautology）：在所有真值赋值下都为真的命题公式。例如 p ∨ ¬p（排中律 Law of Excluded Middle）和 ¬(p ∧ ¬p)（无矛盾律 Law of Non-Contradiction）都是永真式。
矛盾式（Contradiction）：在所有真值赋值下都为假的命题公式。例如 p ∧ ¬p。
可满足式（Satisfiable Formula）：至少存在一种真值赋值使其为真的公式。永真式当然可满足，但反之不成立。
范式（Normal Form）是命题公式的标准表示形式，在自动推理、逻辑电路设计和SAT求解中具有重要作用。
合取范式（Conjunctive Normal Form, CNF）：一系列子句（clause）的合取，每个子句是文字（literal）的析取。例如：(p ∨ ¬q) ∧ (¬p ∨ q ∨ r)
析取范式（Disjunctive Normal Form, DNF）：一系列子句的析取，每个子句是文字的合取。例如：(p ∧ q) ∨ (¬p ∧ r)
定理：每个命题公式都存在等价的合取范式和析取范式。
在实际应用中，CNF有特殊的重要性。著名的SAT求解器（如MiniSat、Z3、Glucose）都以CNF作为输入格式。将公式转化为CNF后，可以应用单元传播（Unit Propagation）、矛盾子句学习（Conflict-Driven Clause Learning, CDCL）等高效算法进行可满足性判定。现代CDCL求解器可以处理拥有数百万变量的CNF实例，这是逻辑理论在工程中最成功的应用之一。
逻辑推理（Logical Inference）是从前提推出结论的过程。推理规则是形式系统中由已知公式产生新公式的变换规则。常用的推理规则：
| 规则名称 | 拉丁文名称 | 形式 | 说明 |
|---|---|---|---|
| 肯定前件 | Modus Ponens | p, p→q ∴ q | 如果p成立且p蕴含q，则q成立 |
| 否定后件 | Modus Tollens | ¬q, p→q ∴ ¬p | 如果q不成立且p蕴含q，则p不成立 |
| 假言三段论 | Hypothetical Syllogism | p→q, q→r ∴ p→r | 蕴含的传递性 |
| 析取三段论 | Disjunctive Syllogism | p∨q, ¬p ∴ q | 排除一个选项后得到另一个 |
| 归谬法 | Reductio ad Absurdum | p→(q∧¬q) ∴ ¬p | 如果从p推出矛盾，则¬p |
| 附加律 | Addition | p ∴ p∨q | 从单个命题推出析取 |
| 简化律 | Simplification | p∧q ∴ p | 从合取推出一个分量 |
| 吸收律 | Absorption | p→q ∴ p→(p∧q) | 蕴含的强化形式 |
在数学实践中，推理不是孤立应用单个规则，而是组合使用。自然演绎系统（Natural Deduction）更接近这种实践。例如，证明 (p∧q)→(r→s) 时，会先假设 p∧q，从中简化出 p，再应用已有的前提推导出 r→s，最后使用→-引入规则关闭假设。
可靠性（Soundness）：形式系统只证明真公式。如果 ⊢A（A可证明），则 ⊨A（A是永真式）。可靠性是形式系统最基本的要求——如果系统能证明假命题，它就是有缺陷的。
完备性（Completeness）：形式系统能证明所有真公式。如果 ⊨A（A是永真式），则 ⊢A（A可证明）。完备性意味着推理规则足够强大，没有遗漏任何真命题。
可判定性（Decidability）：存在算法可以在有限步内判定一个命题公式是否为永真式。最简单的算法就是真值表法——2ⁿ 行（n为原子命题数）。虽然指数级的复杂度在 n 很大时不可行，但至少在理论上，命题逻辑的永真性判定总是可以完成的。更高效的算法包括 DPLL（Davis-Putnam-Logemann-Loveland）及其改进 CDCL，它们在实践中可以处理数百万变量的实例。
SAT问题（Boolean Satisfiability Problem）是命题逻辑中最经典的计算问题：给定一个命题公式，判断是否存在真值赋值使其为真。SAT是第一个被证明的NP完全问题（Cook-Levin定理, 1971）。
尽管SAT是NP完全的，但现代SAT求解器（如MiniSat, Glucose, CaDiCaL）使用CDCL算法和高效的启发式策略，在实践中可以解决具有数百万变量的大型实例。SAT求解器广泛应用于：
谓词逻辑（Predicate Logic），又称一阶逻辑（First-Order Logic, FOL），在命题逻辑的基础上引入了个体变元（individual variables）、谓词（predicates）和量词（quantifiers），表达能力远强于命题逻辑。
如果说命题逻辑相当于编程语言中的布尔表达式，那么谓词逻辑就相当于带有量词和函数调用的完整逻辑语言。它足以表达几乎所有的数学命题——这就是为什么一阶逻辑在数学基础中占据中心地位。
谓词逻辑的语言包括以下组成部分：
项（Term）由常元、变元和函数符号组合而成。例如：f(a, x), +(*(3, x), 1)（即 3x+1）。
公式（Formula）由谓词、项和逻辑联结词、量词组合而成。例如：∀x (P(x) → Q(x))，∃y R(a, y)。
全称量化：∀x P(x) 表示"对所有 x，P(x)成立"
存在量化：∃x P(x) 表示"存在某个 x，使 P(x)成立"
量词的辖域（Scope）：量词所作用的公式范围称为其辖域。在 ∀x (P(x) → Q(x)) 中，∀x 的辖域是 P(x) → Q(x)。在产生歧义时，可以使用括号显式标定辖域。
自由与约束变元：
只有封闭公式才是真正有明确真值的逻辑命题。自由变元使得公式成为一个"有待填充的模板"。
全称量词和存在量词之间存在对偶关系：
¬∀x P(x) ≡ ∃x ¬P(x)
¬∃x P(x) ≡ ∀x ¬P(x)
这些关系可以理解为：
这种对偶性类似于德·摩根定律在量词层面的推广。在自然语言中，这两种表达方式往往可以相互替换，这是逻辑等价的重要体现。
量词分配：
注意后两个公式只是单项蕴含而非等价。例如∀x (P(x) ∨ Q(x)) 成立并不意味着 ∀x P(x) 或 ∀x Q(x) 分别成立——P和Q可能互补覆盖所有情况。
量词与蕴含：
与命题逻辑类似，谓词逻辑公式也可以化为前束范式（Prenex Normal Form, PNF）——所有量词前置。具体步骤如下：
例如：∀x P(x) → ∃y Q(y) 的前束范式是 ∃x ∃y (P(x) → Q(y))。
前束范式在证明理论中有重要作用，因为它将公式的"量词部分"和"无量词部分"（矩阵）分离开来，使后续的斯柯伦化（Skolemization）和Herbrand定理的应用成为可能。
这是命题逻辑和谓词逻辑的关键分界线：命题逻辑是可判定的（有真值表法），而谓词逻辑不是。这反映了一阶逻辑更强的表达能力带来的计算复杂性代价。
尽管一阶逻辑非常强大，但它无法表达一些重要的数学概念——这是由一阶逻辑的元性质（紧致性定理、洛文海姆-斯科伦定理）所决定的：
这些局限性推动了高阶逻辑（Higher-Order Logic, HOL）和无穷逻辑（Infinitary Logic）的发展。高阶逻辑允许对关系和函数进行量化（如"存在一个关系R使得…"），表达能力更强，但代价是失去了完备性——高阶逻辑不再是完备的，也没有完全的证明系统。
尽管如此，由于一阶逻辑有完备的证明系统和良好的元性质（紧致性、洛文海姆-斯科伦等），它在数学基础中仍然占有中心地位。大部分数学可以通过集合论编码降为一阶逻辑——ZFC集合论就是一阶的。
**斯柯伦化（Skolemization）**是将前束范式转化为无量词形式（但引入新函数符号）的过程，用于消去存在量词。基本思想是对每个 ∃x 引入一个依赖于所有外围全称量词的新函数。
例如公式 ∃x ∀y P(x, y) 在斯柯伦化后变为 ∀y P(c, y)（c 是常元）。而 ∀x ∃y P(x, y) 则变为 ∀x P(x, f(x))（f 是斯柯伦函数）。
Herbrand定理：一个前束范式公式（无量词部分）不可满足当且仅当存在一个仅包含常量的Herbrand展开——将全称量词替换为所有可能的项——的有限子集不可满足。这为自动定理证明提供了理论基础：通过枚举Herbrand基（Herbrand Base）中的项，可以机械化地判定一阶公式的不可满足性。
Herbrand定理是归结原理（Resolution Principle）的基础。归结原理由罗宾逊（J. A. Robinson, 1965）提出，是现代自动定理证明器的核心算法。归结原理的工作流程如下：
公理系统（Axiomatic System）是从一组公理（axioms）出发，通过推理规则（inference rules）推导出所有定理（theorems）的形式系统。一个典型的公理系统包含以下要素：
希尔伯特风格的公理系统是最经典的形式，以命题逻辑为例，它只需三个公理模式和一个推理规则：
公理模式（Axiom Schemas）：
推理规则：
这个系统虽然简洁到只有11个符号（三个公理模式 + 一条规则），但它足以推导出命题逻辑的所有永真式。事实上，这是命题逻辑的一个极小完备公理系统。
一个简单的证明示例：证明 p → p（自反性）
这个简单的例子展示了形式证明的全部流程——每一步都是纯粹的符号变换，不依赖直观理解。
自然演绎（Natural Deduction）由根岑（Gerhard Gentzen, 1935）在其博士论文中提出，比希尔伯特系统更接近人类的自然推理方式。其核心思想是：每个逻辑联结词有引入规则（Introduction Rules）和消去规则（Elimination Rules）。
例如蕴含的规则：
自然演绎的优势是更直观、更接近数学实践中的推理方式，适合教学和计算机实现。许多交互式定理证明器（如Coq、Isabelle）的核心基于自然演绎或类似框架。
相继式演算（Sequent Calculus），又称Gentzen系统LK（Logistischer Kalkül），是根岑提出的另一种形式系统，通过对称的左右规则来处理逻辑推理。
相继式（Sequent）的形式为：Γ ⊢ Δ，其中 Γ 和 Δ 是公式的序列（或集合）。Γ ⊢ Δ 的含义是"Γ中所有公式的合取蕴含Δ中所有公式的析取"——也就是说，如果 Γ 的所有前提成立，则 Δ 中至少一个结论成立。
关键规则：
根岑的主定理（Hauptsatz / Cut-Elimination Theorem）指出：任何带有Cut规则的证明都可以转化为不使用Cut规则的证明。这意味着我们可以系统地排除证明中的中间步骤——每个定理都有"直接"证明。这一结果在证明论中极为重要，它揭示了证明的结构性质。Cut消去定理就像编程中的"函数内联"——任何使用中间函数的结果都可以展开为直接的代码。
对于一个公理系统，我们关心以下性质：
需要特别注意：完备性和可判定性是不同的概念。一个系统可以是完备的但不可判定（如谓词逻辑），也可以是不完备的但可判定的（如Presburger算术）。
证明论（Proof Theory）是数理逻辑的一个分支，将数学证明本身作为数学对象进行研究。它最早由希尔伯特提出，作为希尔伯特计划的核心工具。
证明论的核心思想是将证明形式化——将证明视为一种数学结构（如树形结构），然后用数学方法分析证明的结构和性质。这不是研究"如何进行数学思考"，而是研究"证明本身可以用什么结构来表示，这些结构有什么性质"。
希尔伯特计划（Hilbert's Program）是20世纪初大卫·希尔伯特提出的一个宏大计划，目标是：
希尔伯特计划的核心方法论是元数学（Metamathematics）：用"有限方法"（Finitary Methods）研究数学本身。希尔伯特希望通过这种方法一举奠定数学的确定性基础。他在1930年的一次著名广播演讲中慷慨陈词："我们必须知道——我们终将知道！"（Wir müssen wissen — wir werden wissen!）
希尔伯特计划在1931年被哥德尔的不完备性定理彻底动摇。
第一不完备性定理：
任何包含皮亚诺算术的一致公理系统都是不完备的——即存在一个语句 φ，使得 φ 和 ¬φ 在系统中都不可证明。
这意味着任何足够强大的数学系统都无法捕捉所有的数学真理。存在数学真理超越系统的证明能力。
第二不完备性定理：
任何包含皮亚诺算术的一致公理系统都无法证明自身的一致性。
这意味着数学系统的一致性证明必须依赖比系统本身更强的元理论。不可能"自举"式地证明系统的可靠性。
哥德尔编码（Gödel Numbering）是证明中的关键技术。通过将公式和证明映射为自然数，哥德尔在算术中编码了关于算术本身的论述，构造了自指语句。这个自指语句大致表述为："这个语句在系统中不可证明"。如果该语句可证明，则系统不一致（因为证明了它不可证明）；如果不可证明，则该语句为真——系统不完备。
尽管希尔伯特计划的核心目标被证明不可实现，证明论本身继续蓬勃发展：
Curry-Howard 对应（Curry-Howard Correspondence）揭示了逻辑证明与计算程序之间的深刻同构关系：
| 逻辑 | 程序理论 |
|---|---|
| 命题 | 类型 |
| 证明 | 程序/项 |
| 蕴含 → | 函数类型 → |
| 合取 ∧ | 积类型 × |
| 析取 ∨ | 和类型 + |
| 全称 ∀ | 全称类型（泛型） |
| 存在 ∃ | 存在类型 |
| 假 ⊥ | 空类型（Void） |
| 证明规范化 | 程序求值 |
| 切消除 | 函数内联/β-归约 |
| 经典排中律 | call/cc 控制操作符 |
这个对应关系是证明论和类型论的统一基础，也是现代函数式编程语言（如 Haskell、Agda、Coq）的理论基石。当一个Haskell程序员使用Maybe类型时，他实际上是在使用逻辑中的析取；当一个Coq用户编写一个定理证明时，他同时也在编写一个程序。
模型论（Model Theory）研究形式语言与数学结构之间的关系。如果说证明论关注"句法"（公式如何被证明），模型论则关注"语义"（公式在什么情况下为真）。
结构（Structure，又称解释）包括：
模型：如果一个公式（或公式集 Σ）在某个结构中为真，则称该结构是这个公式（或 Σ）的一个模型。
例子：群论公理（结合律、单位元存在、逆元存在）的模型包括整数集 ℤ 上的加法群、置换群 S₃、矩阵群 GL(n,ℝ) 等。这些群的结构各不相同，但都满足相同的群论公理——这就是"公理"的抽象力量：一套公理可以刻画一类结构。
可满足性（Satisfiability）：一个公式集 Σ 在存在模型时称为可满足的。一个理论是可满足的当且仅当它至少有一个模型。
可定义性（Definability）：如果存在一个公式 φ(x) 使得结构 𝔄 中的元素 a 满足 φ(a) 当且仅当 a 具有性质 P，则称 P 在 𝔄 中是可定义的。
模型论的可定义性概念直接对应于编程中的"谓词抽象"——并不是所有数学性质都可以用一阶公式表达，这反映了一阶逻辑的局限性。
紧致性定理（Compactness Theorem）：一个公式集 Σ 可满足当且仅当 Σ 的每个有限子集都可满足。
这是模型论中最基本也是最重要的定理。其推论包括：
下洛文海姆-斯科伦定理（Downward Löwenheim-Skolem Theorem）：如果一个可数语言的理论有一个模型，则它有一个可数模型。
上洛文海姆-斯科伦定理（Upward Löwenheim-Skolem Theorem）：如果一个理论有一个无穷模型，则对任意基数 κ ≥ |L|（语言的大小），该理论存在一个基数为 κ 的模型。
这些定理揭示了一阶逻辑的核心弱点：它无法区分不同大小的无穷集合。实数域的一阶理论（ℛ）既有无穷多个可数模型，也有无穷多个不可数模型——一阶逻辑根本"看不见"实数的不可数性。
斯科伦悖论（Skolem's Paradox）：集合论（如ZFC）存在可数模型（由下洛文海姆-斯科伦定理），但ZFC内部却可以证明不可数集合的存在。这并非真正的矛盾，只是说明"可数性"这一概念是相对于模型而言的——一个集合在模型外部看来是可数的，但模型内部没有建立该集合与自然数之间的双射（因为该双射不在模型中）。
量词消去（Quantifier Elimination）是指一个理论中的每个公式都等价于一个无量词公式。如果一个理论有量词消去，那么该理论上的所有问题都可以归结为无量词的组合问题，从而大大简化判定过程。
著名的量词消去结果：
量词消去为理论的可判定性提供了重要路径。例如，实闭域理论的量词消去算法可以直接用于求解带量词的实多项式不等式——这是CAD算法（Cylindrical Algebraic Decomposition）的理论基础。
可计算性理论（Computability Theory），又称递归论（Recursion Theory），研究什么是"可计算的"以及计算的固有限制。
核心问题：哪些函数可以通过算法计算？哪些问题是算法不可解的？是否存在"不可解"的问题？
图灵机（Turing Machine, 1936）是艾伦·图灵提出的抽象计算模型。一个图灵机由以下部分组成：
图灵机的精妙之处在于：尽管其结构极其简单（只有有限状态 + 无限纸带），但它足以模拟任何其它计算模型——这就是图灵完全性（Turing Completeness）的概念。
丘奇-图灵论题（Church-Turing Thesis）：任何"直观可计算的"函数都可以用图灵机计算。这不是一个数学定理（因为它涉及"直观可计算"这个非形式的概念），而是可计算性概念的经验假设——至今没有被反例推翻。
其他等价的计算模型：
停机问题（Halting Problem）是图灵在1936年证明的经典不可判定问题：
不存在一个算法能够判定：给定任意图灵机 M 和输入 w，M 在输入 w 上是否最终停机。
证明思路（反证法）：
这个证明的精妙之处与哥德尔不完备性定理异曲同工——都利用了自引用（self-reference）来制造悖论。
停机问题的不可判定性意味着任何具有一定表达能力的形式系统中都存在不可判定的问题。这是计算的本质极限，而不是因为我们不够聪明或计算机不够快。
除了停机问题，还有许多其他不可判定的问题：
图灵归约（Turing Reduction）：如果问题A的解可以转化为问题B的解（通过有限次调用B的"神谕"），则称A可图灵归约为B。这给出了问题之间的难度比较。
可归约度（Turing Degree）：将所有彼此可相互归约的问题归为一个等价类，称为一个可归约度。可归约度按照"难度"形成一个偏序结构，称为图灵度（Turing Degrees）。
复杂度层级：
可计算层级（Computable ⊆ 递归可枚举 ⊆ … ⊆ 算术层级 ⊆ 解析层级…）
可判定问题构成系统的底层。再往上是递归可枚举问题（半可判定——停机时输出"是"，但可能永远不停机）。继续往上延伸出算术层级、解析层级——层级越高，问题的"不可判定程度"越强。
在可计算性之上，计算复杂性理论（Computational Complexity Theory）进一步研究问题的"资源消耗"：
P ≠ NP 问题是计算机科学和数学中最重要的未解问题之一（克雷数学研究所的千禧年难题之一）。
一阶谓词逻辑是完备的：任何一阶逻辑的通用有效公式都可以在标准公理系统中证明。
意义：
（已在证明论部分详细讨论，这里是总结）
第一不完备性定理终结了搜寻完全数学公理系统的尝试。
第二不完备性定理终结了通过相对简单的元理论证明数学系统一致性的尝试。
两者共同确立了形式化方法的根本局限性。
一阶逻辑是满足紧致性和洛文海姆-斯科伦性质的最强逻辑。
任何比一阶逻辑更强的逻辑必然放弃紧致性或洛文海姆-斯科伦性质（或两者）。这从"元性质"的角度刻画了一阶逻辑的独特地位——一阶逻辑之所以"特殊"，不是偶然的，而是因为它恰好位于这两个重要性质的交叉点上。
在足够丰富的语言中，该语言的真理谓词不能在系统内部定义。
这解决了"什么是真理"的形式化问题，表明真理概念相对于形式系统是超越的。该结果的证明也使用了自指技巧（类似哥德尔编码），构造了一个"说真话者悖论"（与说谎者悖论对称）："这个语句在系统内部不成立"。
虽然不是严格意义上的数理逻辑定理，但康托尔的对角线论证（Cantor's Diagonal Argument）是数理逻辑中的经典技术。它证明了实数的不可数性：
假设实数可数，将它们排列成一个列表。然后构造一个新实数，使其第n位不同于列表中第n个数的第n位。这个数不在列表中——矛盾。图灵和哥德尔都直接借用了对角线论证的思想。实际上，停机问题、不可定义性定理和不完备性定理的证明中，对角线论证都以不同形式出现。
程序验证：
类型系统：
数据库理论：
人工智能：
在软件工程师的日常工作中，数理逻辑以多种形式出现：
入门阶段（2-4周）：
进阶阶段（4-8周）：
深入阶段（8-12周）：
专题阶段（按需选择）：