1.3 谓词逻辑：对象、量词与程序规格
命题逻辑可以把“管理员 Alice 通过了 MFA”当作一个整体，却无法直接表达“每个管理员都必须通过 MFA”。谓词逻辑把公式内部打开，引入对象、属性、关系和量词。
语言、结构和解释
一阶逻辑的语言可以包含：
- 常量符号：
alice、serverA； - 函数符号：
owner(project)、manager(user)； - 谓词符号：
Admin(x)、Owns(x, y)； - 变量、逻辑联结词和量词。
符号本身没有自动含义。还需要一个结构（解释）：
- 指定讨论域，例如系统中的全部用户；
- 指定常量代表哪个对象；
- 指定函数怎样映射对象；
- 指定谓词对哪些对象成立。
同一个公式在不同结构中可能有不同真值。写规格时必须明确量词的域，不能默认读者知道“所有”究竟指所有用户、活跃用户还是本租户用户。
项、原子公式和复合公式
项（term）指向讨论域中的对象：
x
alice
owner(projectA)
manager(owner(projectA))谓词作用于项，形成原子公式：
Admin(x)
Owns(alice, projectA)
CanDelete(user, project)再通过联结词和量词组合：
∀x (Admin(x) → HasMfa(x))
∃x (Admin(x) ∧ Locked(x))第一条表示域中每个管理员都通过 MFA；第二条表示至少存在一个既是管理员又被锁定的对象。
自由变量和约束变量
在：
∀x (Owns(x, p) → CanEdit(x, p))x 被 ∀x 约束，p 没有被量词约束，是自由变量。带自由变量的公式更像一个依赖参数的条件；所有变量被约束后，才成为有确定真值的句子。
量词只控制自己的作用域：
∀x Admin(x) → HasMfa(x)若缺少括号，具体解析取决于语法约定，也可能让 x 在后半部分成为自由变量。工程规格应写成：
∀x (Admin(x) → HasMfa(x))量词顺序不能随意交换
∀u ∃r CanAccess(u, r)每个用户都至少能访问某个资源，不同用户可以访问不同资源。
∃r ∀u CanAccess(u, r)存在同一个资源，所有用户都能访问它。第二条强得多。
软件需求里的“每个请求都有一个追踪 ID”也有同样区别：
∀request ∃traceId HasTrace(request, traceId)若误写成 ∃traceId ∀request ...，就变成所有请求共享一个追踪 ID。
否定量词
德·摩根律在量词上的对应形式是：
¬∀x P(x) ≡ ∃x ¬P(x)
¬∃x P(x) ≡ ∀x ¬P(x)“并非所有节点都健康”意味着“至少有一个节点不健康”，不是“所有节点都不健康”。这类错误在告警查询和测试断言中很常见。
表达存在且唯一
“每个订单有且只有一个创建者”不能只写存在：
∀o ∃u CreatedBy(o, u)还要表达任意两个创建者其实相同：
∀o ∃u (
CreatedBy(o, u)
∧ ∀v (CreatedBy(o, v) → v = u)
)也可使用记号 ∃!u 表示“存在唯一的 u”，前提是文档已经定义该记号。
必须区分 ∀x(P → Q) 与 ∀x(P ∧ Q)
“所有管理员都通过 MFA”通常写作：
∀x (Admin(x) → HasMfa(x))非管理员使前件为假，不影响该规则。
若写成：
∀x (Admin(x) ∧ HasMfa(x))就要求域中的每个对象都是管理员且通过 MFA，含义完全不同。
存在量词常与合取配合：
∃x (Admin(x) ∧ HasMfa(x))若写成 ∃x(Admin(x) → HasMfa(x))，只要域中存在一个非管理员，公式就可能轻易为真，无法表达“存在一个通过 MFA 的管理员”。
从前置条件到后置条件
程序规格可以用谓词表达状态：
前置条件：amount > 0 ∧ balance(account) >= amount
执行：withdraw(account, amount)
后置条件：
balance'(account) = balance(account) - amount撇号表示执行后的状态。还应写出未变部分（frame condition），否则规格只约束余额变化，却没有禁止方法顺手修改账户所有者。
循环不变量也是谓词。例如计算数组前 i 项之和：
0 <= i <= n
sum = Σ(k=0..i-1) a[k]证明初始化成立、每次迭代保持、退出时推出目标，就能从局部步骤建立整体正确性。第 3、4 章会继续展开证明和归纳。
与类型系统的关系要谨慎表达
逻辑与类型之间存在深刻联系，例如 Curry–Howard 对应把某些类型看作命题、程序看作证明；泛型量化也常借用 ∀、∃ 记号。但不能直接说“所有类型系统的本质就是一阶谓词逻辑”。不同类型系统包含高阶类型、依赖类型、子类型、效应和运行时检查，所用逻辑与语义并不相同。
在普通程序中，谓词更多用于：
- API 前置/后置条件；
- 数据库约束和授权策略；
- 静态分析、符号执行与 SMT 查询；
- 模型检查和测试性质。
数据库查询的三值逻辑提醒
“不存在没有通过 MFA 的管理员”在经典逻辑中可写：
¬∃x (Admin(x) ∧ ¬HasMfa(x))SQL 常对应 NOT EXISTS 查询。但 SQL 的 NULL 引入 UNKNOWN，NOT IN、比较和否定的行为可能不同于经典二值逻辑。把公式落到查询语言时，应检查数据库的空值语义。
一阶逻辑的能力边界
有限命题公式可以用真值表判定。一般的一阶逻辑有效性没有一个对所有输入都保证停机并给出是/否答案的判定算法。特定有限域、受限片段或结合理论的 SMT 问题则可能可判定或在实践中有效求解。
这解释了为什么验证工具经常要求有限边界、限制量词形状，或在超时时返回 unknown。形式化并不意味着任何规格都能自动求解。
完成检查
为多租户项目系统形式化以下规则：
- 每个项目恰好属于一个租户；
- 用户只能编辑自己租户中的项目；
- 每个项目至少有一个负责人；
- 不存在同时属于两个租户的用户；
- 并非所有管理员都能删除审计记录。
逐条标出讨论域、自由变量和量词作用域，并为量词顺序错误各写一个反例。