一阶逻辑（FOL）

Parent: logic

数学的标准逻辑：对论域中的元素进行量化（而不是对集合量化——那是二阶逻辑 / MSO）。

语法

• 项（Terms）： 变量、常量，以及作用于项上的函数符号（f(x, c)）。
• 原子公式： 谓词作用于若干项（P(x)、x = y、x < y）。
• 公式： 原子公式在 ¬, ∧, ∨, → 以及量词 ∀x（"对所有元素"）、∃x（"存在某个元素"）下封闭得到。

语义

一个结构（模型）M = 一个论域集合 + 对常量/函数/谓词符号的解释。满足关系 M ⊨ φ 表示"φ 在 M 中为真"。一个句子若在每一个模型中都为真则称为有效的（⊨ φ），若在某个模型中为真则称为可满足的，而 Γ ⊨ φ（蕴涵）表示 Γ 的每一个模型都满足 φ。

两大定理

• 哥德尔完全性定理（1929）： 存在一个可靠且完全的证明系统——⊢ φ ⟺ ⊨ φ（可证明 = 有效）。（不要与不完全性定理混淆：完全性说的是一阶逻辑的有效性；不完全性说的是像算术这样的特定理论无法证明所有真命题。）
• 紧致性： 若 Γ 的每一个有限子集都可满足，则 Γ 本身可满足。这是模型论中的一个主力工具（用来构造无穷/非标准模型）。

症结所在

完全性使有效性成为半可判定的——枚举证明，若 φ 有效，你终会找到它。但你无法在一般情形下判定有效性：这正是一阶逻辑的不可判定性（Entscheidungsproblem，判定问题），而这恰恰是图灵1936年的论文要解决的问题。