写下群的公理——结合律、单位元、逆元。这几行符号本身不指任何东西，它只是一张筛子：整数加法通过，可逆矩阵通过，自然数加法没通过。通过的结构就是它的模型。
数学家因此在两个层面工作。语法层：按规则重排符号，一步步推，全程有限、机械、可交给机器（$T\vdash\varphi$）。语义层：到每个模型里看它真不真——一句 $\forall x$ 要检查无穷多个 $x$，人查不完（$T\models\varphi$）。1929 年哥德尔证明：两层结果完全一样。
别与不完备定理混淆：完备性（1929）说推演规则够用，不完备（1931）说算术公理不够；前者关于逻辑，后者关于某个理论。
左边是语义蕴涵：$T$ 的每个模型都让 $\varphi$ 为真；右边是语法可导：存在一串有限长的形式推导。$\Leftarrow$ 是可靠性，容易；内容全在 $\Rightarrow$：不存在「所有模型里都成立、却永远证不出来」的一阶命题。
真理是关于无穷的概念，证明是有限的对象，两者外延竟然相等。这是「无穷被有限捕获」的第一个精确版本，也是自动定理证明的地基——机器只会摆弄符号，完备性保证它不会漏掉任何普遍真理。
反面立刻浮现：证明既然有限，就只用得到有限条公理——下一张卡片那台造世界的机器正是从这里长出来。
关系数据库的查询语言就是一阶逻辑的工程化身：关系代数与一阶公式一一对应，SQL 的 WHERE 与 EXISTS 就是联结词与量词，Datalog 与 Prolog 同源。形式化验证里 Lean 与 Coq 的底座虽是更强的类型论，但真正把子目标自动关掉的那一层（SMT）跑的仍是一阶逻辑。
一堆句子若自相矛盾，矛盾一定在有限多句里就已暴露——推出矛盾的那个证明本身有限，只来得及用到有限条前提。反过来说就是紧致性定理：若每个有限子集都有模型，整个（可以无穷大的）集合就有模型。
这条听着像废话的原理，其实是一台造世界的机器。想要一个「无穷大的自然数」？在算术语言里添一个常数 $c$ 与无穷多条公理 $c>0,\ c>1,\ c>2,\dots$。任取有限多条，最苛刻的无非说 $c>n$，让 $c$ 当 $n+1$ 即可——普通自然数就是模型。于是紧致性断言整套公理有模型：那里面住着一个大于所有标准自然数的元素。结论令人不安——一阶语言说不出「有限」，也钉不死「这就是自然数」。
「紧致」不是比喻：把完备理论当作点、单句划出的集合当作基本开集，得到的拓扑空间（Stone 空间）恰好紧致——这条定理就是「有限子覆盖」的逻辑翻版。
它把「证明是有限的」这条不值一提的观察，兑换成了无中生有的存在性。Löwenheim–Skolem 是同一台机器的另一个出口——可数语言的理论只要有无穷模型，就有每种无穷基数的模型。于是 ZFC 若一致就有可数模型，尽管它内部证明了不可数集存在。这个 Skolem 悖论不是矛盾：「不可数」是模型内部的判断，指模型里没有那个一一对应，站在外面当然找得到。「有多少」取决于你站在哪里数。
de Bruijn–Erdős 定理：无限图若每个有限子图都可 $k$ 着色，则整图可 $k$ 着色——紧致性直接给出。反过来看更有意思：紧致性在有限模型上失效，这正是数据库理论必须另建「有限模型论」的原因——现实的表都是有限的，经典模型论的主力定理在那里全部作废。
牛顿与莱布尼茨的无穷小 $dx$——比任何正数都小却不是零——被 Berkeley 主教讥为「死去量的鬼魂」，19 世纪被 $\varepsilon$–$\delta$ 驱逐。1960 年 Robinson 用上一张卡片那台机器把它请了回来：往实数的理论里加一个常数 $\epsilon$ 与无穷多条公理 $0<\epsilon<1/n$，每个有限子集显然可满足，于是存在一个含真无穷小的有序域——超实数 $^*\mathbb{R}$。
在 $^*\mathbb{R}$ 里，导数不再是「极限」，就是差商本身：算出 $\frac{f(x+\epsilon)-f(x)}{\epsilon}$，再取它的标准部分（离它最近的那个实数）。连续性也不必再动用三重量词：$x$ 与 $y$ 无限接近就蕴含 $f(x)$ 与 $f(y)$ 无限接近。
这叫转移原理：凡一阶语言写得出的性质，在实数里成立当且仅当在超实数里成立——$^*\mathbb{R}$ 好用的理由全在这里：它自动是有序域，每个实函数自动有延拓。「一阶」是关键限制：「有上界的子集有上确界」量化的是子集，属二阶，不转移，$^*\mathbb{R}$ 确实不完备。老一代无穷小论证偶尔翻车，翻的正是这类车。
一个被放逐一个半世纪的直觉，最后不是被分析学、而是被逻辑平反。更漂亮的是它顺带解释了历史：那些「不严格」的推理为何常常给出正确结果——它们是转移原理的非形式版本，而转移原理是定理；同时它也划清了这些推理会在何处出错。
不完备定理说「PA 里有真而不可证的句子」。这里问的是另一个更工程的问题：给定一个理论，有没有算法判断任意一句话是不是它的定理？
分水岭窄得惊人。只含加法的自然数算术（Presburger）可判定；补上乘法就是 PA，立刻不可判定；而实数上带加法乘法的一阶理论（实闭域），Tarski 1951 年证明它又可判定——看似更大的结构反而更驯服。
关键不在对象多不多，而在能否在理论内部把整数定义出来：有了整数就能编码图灵机，也就把停机问题塞了进来。实闭域里没有一阶公式挑得出整数，于是可判定。不可判定性只有一个源头——自指的能力。
Tarski 的方法叫量词消去：每个公式都能等价改写成不含量词的形式。上式是最小的例子——左边要在无穷多个 $x$ 里搜索，右边只需对系数做有限次算术判断。无量词公式的真假可以直接算，量词逐个消去，整个理论便可判定。
可判定不等于容易：Presburger 算术的判定问题有双指数时间下界，可判定与可行之间还隔着一整片荒原。真正的美在那条分水岭本身——它精确落在「结构能否在自身内部模拟计算」上。哥德尔（不完备）、图灵（停机）、Tarski（真理不可定义）三条路在这里汇成一句话：能自指者，必失判定。
SMT 求解器（Z3、CVC5）正是这些可判定片段的工程化：线性整数算术、位向量、数组、未解释函数各配一套判定过程再拼装，编译器验证（CompCert）、内核验证（seL4）、符号执行与程序合成底下跑的都是它。这条线也反过来指导设计——Datalog 长盛不衰，正因它刻意停在可判定的那一侧：为系统挑规约语言，本质是在表达力与可判定性之间选一个点。