逻辑最深刻的一点：它研究的不是「什么是真的」，而是「从真如何必然推出真」。「所有 A 都是 B，x 是 A，所以 x 是 B」——这个推理有效，无论 A、B、x 具体指什么。把内容全抽走，只剩形式的骨架，而有效性只住在骨架里。
命题逻辑的原料是「命题」——能判真假的陈述——和四个连接词：与（$\land$）、或（$\lor$）、非（$\neg$）、蕴含（$\to$）。真值表就是逻辑的乘法表：给定各部分的真假，整体的真假被机械算出。逻辑在这里第一次变成了可计算的东西。
命题变量 $p,q,\dots$ 取值真/假。蕴含可被定义为 $p \to q \equiv \neg p \lor q$——「$p$ 推出 $q$」等价于「要么 $p$ 假，要么 $q$ 真」。这解释了上表最反直觉的一行：前提为假时，蕴含恒真（空承诺不算违约）。若一个公式在所有赋值下都真，称为重言式（tautology），它就是逻辑意义上「永远成立」的规律。
真正的震撼是一个三重同构：推理、开关电路、集合运算，是同一个结构的三张脸。$\land$ 对应串联、对应集合的交；$\lor$ 对应并联、对应并集；De Morgan 律 $\neg(p\land q)\equiv\neg p\lor\neg q$ 既是逻辑定律，又是电路化简规则，又是集合恒等式。这个共同骨架叫布尔代数。当 Boole 说「思维的规律可以像代数一样运算」时，他没料到一百年后它会变成每颗 CPU 的物理蓝图。
数字电路：一个「与非门」（NAND）就能搭出全部逻辑，整颗处理器不过是命题逻辑的硅基实现。SAT 求解器——判断一堆逻辑约束能否同时满足——是芯片验证、软件测试、排班调度的核心引擎，也是理论计算机科学里第一个被证明 NP 完全的问题。编译器的类型检查、数据库的条件下推，底层都在跑命题逻辑。
命题逻辑有个致命的哑口：它说不出「所有」和「存在」。「所有素数都大于 1」在命题逻辑里只是一个不可拆的原子。谓词逻辑补上了这块——引入量词「对所有 $x$」（$\forall x$）、「存在 $x$」（$\exists x$），以及能带变量的谓词 $P(x)$（「$x$ 是素数」）。
就这一步扩张，逻辑突然能写下整个数学。「每个数都有后继」这类命题的骨架，全是量词与谓词的编织。谓词逻辑就是数学家写严格陈述时脑中那套隐形的语法。
$\forall x\,P(x)$ 意为「对论域中每个 $x$，$P(x)$ 成立」；$\exists x\,P(x)$ 意为「至少有一个 $x$ 使 $P(x)$ 成立」。核心难点在量词的嵌套顺序：
左边说「每个数都有比它大的数」（真）；右边说「存在一个数比所有数都大」（在自然数里假）。同样的符号，调换顺序，真假逆转。
数学严格性的秘密几乎都藏在量词顺序里。微积分的 $\varepsilon$–$\delta$ 极限定义 $\forall\varepsilon\,\exists\delta\,\forall x\,(\dots)$ 之所以两百年才被 Cauchy、Weierstrass 打磨出来，正因为人类直觉不擅长处理「先给我任意小的 $\varepsilon$，我再找 $\delta$」这种依赖顺序的三层量词。会精确地读量词顺序，几乎就等于会读数学——连续与一致连续之差，也只是两个量词换了位置。
SQL 查询本质是谓词逻辑：`WHERE` 是谓词，`EXISTS`/`ALL` 是量词，关系数据库理论直接建在一阶逻辑上。逻辑编程语言 Prolog 让你「写下事实与规则，机器自动推理」。证明助手 Lean、Coq 用一阶（及更高阶）逻辑把整个数学形式化。AI 的知识表示、自动定理证明、程序规约（precondition/postcondition）无不以谓词逻辑为通用语。
想象一句话：「这句话无法被证明。」若它能被证明，那它就是假的——系统证出了假命题，崩溃。若它不能被证明，那它恰好说对了——于是它为真，但系统证不出来。哥德尔 1931 年做的，就是把这句自指的话翻译成一个纯粹关于整数的算术命题。
诀窍叫「哥德尔编码」：给每个符号、公式、证明都编一个唯一的数。于是「某公式可被证明」变成了「某个数具有某种算术性质」。系统被迫开始谈论它自己——说谎者悖论第一次拥有了数学的躯体。
第一不完备定理：任何一致的、能表达基本算术的、公理可被机械枚举的形式系统 $T$，都存在一个语句 $G$，使得 $T$ 既不能证明 $G$，也不能证明 $\neg G$——$G$ 是不可判定的（而按元数学看它为真）。
第二不完备定理：这样的 $T$ 无法在自身内部证明自己的一致性 $\mathrm{Con}(T)$。一个系统若能证明「我不矛盾」，恰恰说明它已经矛盾了。
这是数学史上最深的一次「照镜子」。希尔伯特的宏愿是把全部数学机械化：一套公理，能证明所有真理、且能自证无矛盾。哥德尔从系统内部击碎了这个梦——「真」永远大于「可证」。而真正的美在于：不完备不是谁不够聪明，而是足够丰富的形式系统与生俱来的极限。它和图灵的停机问题、塔斯基的「真不可定义」是同一枚硬币的三面——自指一旦足够强，系统就无法完全把握自己。
它的直系后裔是停机问题：不存在程序能判定任意程序是否会停机——因此不存在「完美的通用 bug 检测器」，程序无法完全自我验证，这为软件工程的可判定性划出硬边界。在 AI 上，「真」与「可证」的分野提醒我们：再强的形式系统（或模型）也有它原理上触不到的真命题，可解释性与对齐无法指望系统对自身给出完备的形式保证。
数学证明通常是「一段能说服同行的论证」——带着直觉、省略和「显然可得」。形式化把它逼到极致：证明变成一串符号，每一步要么是公理，要么由前面几步按明文规则机械得出。意义被彻底抽离，只剩形式——证明于是成了机器能逐字检查的对象。
这看似把数学榨干了灵魂，实则相反：它让「一个证明到底对不对」第一次有了不依赖任何权威的终极裁决。真理的裁判从人的信服，交给了规则的验算。
一个形式系统 = 符号表 + 合式公式的语法 + 若干公理 + 有限条推理规则（最经典的是分离规则 modus ponens：由 $p$ 与 $p\to q$ 得 $q$）。一个证明就是一个有限公式序列，其中每一项要么是公理，要么由前面若干项经某条规则得到；序列的最后一项即被证的定理。判定「这个序列是不是合法证明」是一个纯语法、可机械执行的过程。
最深的美是柯里–霍华德对应（Curry–Howard）：证明就是程序，命题就是类型。「证明 $A\to B$」和「写一个把 $A$ 型输入变成 $B$ 型输出的函数」是同一件事；运行一个程序，对应着化简一个证明。逻辑、计算、类型——三个看似分属哲学、工程、语言学的领域，在最底层是同构的。这解释了为什么现代证明助手同时也是编程语言：在它们眼里，检查证明和运行代码从来就没有区别。
Lean、Coq 等证明助手已把四色定理、开普勒球堆积猜想这类「人类难以逐行复核」的巨型证明完全机械验证；Terence Tao 正用 Lean 把前沿论文形式化。工程上，操作系统内核 seL4、C 编译器 CompCert 被形式验证到「数学上保证无某类 bug」，用于零容错场景。区块链智能合约、加密协议也越来越依赖形式验证堵住代价高昂的逻辑漏洞。