语法与语义的分离
现代逻辑学奠基性的解耦：把"能推导出什么"和"什么为真"拆开，各自独立定义、互不依赖，然后再追问二者如何关联。
两个独立的方面
- 语法（
⊢）——证明：由固定规则（公理加推理规则，如分离规则 modus ponens）操作的有限字符串。纯粹形式化——证明可以由一台完全不理解任何意义的机器来检验。"Γ ⊢ φ"意为"存在一个从Γ推出φ的推导"。- 语义（
⊨）——模型中的真：一个结构给符号赋予解释，⊨表示某公式成立。纯粹的意义。"Γ ⊨ φ"意为"Γ的每一个模型都使φ为真"。
关键在于这两者是分别定义的：⊢ 从不提及模型；⊨ 从不提及证明。可推导的公式集合与为真的公式集合没有任何先验理由应当相同——把这两者各自独立地精确化，正是逻辑学得以数学化的关键所在：
- 希尔伯特／形式主义赋予了语法以严谨性（证明即机械的重写）；
- 塔斯基（1933）赋予了语义以严谨性（对"
M ⊨ φ"的递归定义）。
这个分裂为何是全局的关键
一旦二者成为独立的对象，soundness（⊢ ⟹ ⊨）与completeness（⊨ ⟹ ⊢）就变成了必须被证明的定理，而不再是定义——并且每一个都是通过跨越这道鸿沟来证明的：
- 可靠性把真通过规则推过去（语义 ← 语法）；
- 完全性从一个一致的理论构造出一个模型（语义 ← 语法，方向相反）。
而且这个分裂是永久性的：这正是证明论（研究 ⊢）与模型论（研究 ⊨）成为两个不同领域的原因，也是哥德尔不完全性得以被表述的原因——它恰恰出现在算术中这两侧未能重合的地方（⊨_ℕ 超出了 ⊢_PA）。Curry–Howard 对应关系是同一个语法↔语义主题在更高一层的回响（证明 ↔ 程序）。