Software Systems Atlas

中文

English

中文

English

主题

第 10 卷 / 第 1 章 / 第 3 课

1.3 谓词逻辑：对象、量词与程序规格 ​

命题逻辑可以把“管理员 Alice 通过了 MFA”当作一个整体，却无法直接表达“每个管理员都必须通过 MFA”。谓词逻辑把公式内部打开，引入对象、属性、关系和量词。

语言、结构和解释 ​

一阶逻辑的语言可以包含：

  • 常量符号：alice、serverA；
  • 函数符号：owner、manager，可组成 owner(project) 等项；
  • 谓词符号：Admin、Owns，可组成 Admin(x) 等公式；
  • 变量、逻辑联结词和量词。

符号本身没有自动含义。还需要一个结构（解释）：

  1. 指定讨论域，例如系统中的全部用户；
  2. 指定常量代表哪个对象；
  3. 指定函数怎样映射对象；
  4. 指定谓词对哪些对象成立。

同一个公式在不同结构中可能有不同真值。写规格时必须明确量词的域，不能默认读者知道“所有”究竟指所有用户、活跃用户还是本租户用户。

标准一阶逻辑通常使用非空讨论域，并把函数符号解释为对所有域内输入都有值的全函数。若项目可能没有负责人，不能无说明地把 owner(project) 当作总有用户值的函数；可改用关系，或明确一个“未分配”对象及其规则。定义可核对 Open Logic 的结构章节。

以下涉及用户、资源和订单的公式采用按对象类别限制量词的简写。例如 ∀u 表示对用户量化；若只有一个总讨论域，应展开为 ∀u(User(u) → ...)，资源和订单同理。某类对象的子集可以为空，不等于整个讨论域为空。

项、原子公式和复合公式 ​

项（term）指向讨论域中的对象：

text
x
alice
owner(projectA)
manager(owner(projectA))

谓词作用于项，形成原子公式：

text
Admin(x)
Owns(alice, projectA)
CanDelete(user, project)

再通过联结词和量词组合：

text
∀x (Admin(x) → HasMfa(x))
∃x (Admin(x) ∧ Locked(x))

第一条表示域中每个管理员都通过 MFA；第二条表示至少存在一个既是管理员又被锁定的对象。

自由变量和约束变量 ​

在：

text
∀x (Owns(x, p) → CanEdit(x, p))

x 被 ∀x 约束，p 没有被量词约束，是自由变量。带自由变量的公式更像一个依赖参数的条件；所有变量被约束后，才成为有确定真值的句子。

量词只控制自己的作用域：

text
∀x Admin(x) → HasMfa(x)

若缺少括号，具体解析取决于语法约定，也可能让 x 在后半部分成为自由变量。工程规格应写成：

text
∀x (Admin(x) → HasMfa(x))

量词顺序不能随意交换 ​

text
∀u ∃r CanAccess(u, r)

每个用户都至少能访问某个资源，不同用户可以访问不同资源。

text
∃r ∀u CanAccess(u, r)

存在同一个资源，所有用户都能访问它。第二条强得多。

两个用户分别只能访问各自资源，就足以区分这两条公式。下面的 Python 3 标准库示例直接枚举有限集合：

python
users = ["u1", "u2"]
resources = ["r1", "r2"]
access = {("u1", "r1"), ("u2", "r2")}

def every_user_has_resource(users, resources):
    return all(any((u, r) in access for r in resources) for u in users)

def one_resource_for_all(users, resources):
    return any(all((u, r) in access for u in users) for r in resources)

print(every_user_has_resource(users, resources))  # True
print(one_resource_for_all(users, resources))    # False
print(all([]), any([]))                          # True False

all([]) 为真，是因为没有反例；any([]) 为假，是因为没有见证。因此“所有管理员都通过 MFA”在没有管理员时也成立。若业务还要求至少有一名管理员，必须另加存在条件；空集合不会主动替你报缺人。

软件需求里的“每个请求都有一个追踪 ID”也有同样区别：

text
∀request ∃traceId HasTrace(request, traceId)

若误写成 ∃traceId ∀request ...，就要求至少有一个 ID 与所有请求都关联。原来的“每请求存在一个 ID”既不保证每请求只关联一个 ID，也不要求不同请求使用不同 ID。分布式跟踪可能有意让相关请求共享 trace ID，唯一性范围需要另行规定。

否定量词 ​

德·摩根律在量词上的对应形式是：

text
¬∀x P(x) ≡ ∃x ¬P(x)
¬∃x P(x) ≡ ∀x ¬P(x)

“并非所有节点都健康”意味着“至少有一个节点不健康”，不是“所有节点都不健康”。这类错误在告警查询和测试断言中很常见。

表达存在且唯一 ​

“每个订单有且只有一个创建者”不能只写存在：

text
∀o ∃u CreatedBy(o, u)

还要表达任意两个创建者其实相同：

text
∀o ∃u (
  CreatedBy(o, u)
  ∧ ∀v (CreatedBy(o, v) → v = u)
)

也可使用记号 ∃!u 表示“存在唯一的 u”，前提是文档已经定义该记号。

必须区分 ∀x(P → Q) 与 ∀x(P ∧ Q) ​

“所有管理员都通过 MFA”通常写作：

text
∀x (Admin(x) → HasMfa(x))

非管理员使前件为假，不影响该规则。

若写成：

text
∀x (Admin(x) ∧ HasMfa(x))

就要求域中的每个对象都是管理员且通过 MFA，含义完全不同。

存在量词常与合取配合：

text
∃x (Admin(x) ∧ HasMfa(x))

若写成 ∃x(Admin(x) → HasMfa(x))，只要域中存在一个非管理员，公式就可能轻易为真，无法表达“存在一个通过 MFA 的管理员”。

从前置条件到后置条件 ​

程序规格可以用谓词表达状态：

text
前置条件：amount > 0 ∧ balance(account) >= amount

执行：withdraw(account, amount)

后置条件：
balance'(account) = balance(account) - amount

撇号表示执行后的状态。还应写出未变部分（frame condition），否则规格只约束余额变化，却没有禁止方法顺手修改账户所有者。

循环不变量也是谓词。例如计算数组前 i 项之和：

text
0 <= i <= n
sum = Σ(k=0..i-1) a[k]

证明初始化成立、每次迭代保持、退出时推出目标，就能从局部步骤建立整体正确性。第 3、4 章会继续展开证明和归纳。

与类型系统的关系要谨慎表达 ​

逻辑与类型之间存在深刻联系，例如 Curry–Howard 对应把某些类型看作命题、程序看作证明；泛型量化也常借用 ∀、∃ 记号。但不能直接说“所有类型系统的本质就是一阶谓词逻辑”。不同类型系统包含高阶类型、依赖类型、子类型、效应和运行时检查，所用逻辑与语义并不相同。

在普通程序中，谓词更多用于：

  • API 前置/后置条件；
  • 数据库约束和授权策略；
  • 静态分析、符号执行与 SMT 查询；
  • 模型检查和测试性质。

数据库查询的三值逻辑提醒 ​

“不存在没有通过 MFA 的管理员”在经典逻辑中可写：

text
¬∃x (Admin(x) ∧ ¬HasMfa(x))

SQL 常对应 NOT EXISTS 查询。但 SQL 的 NULL 引入 UNKNOWN，NOT IN、比较和否定的行为可能不同于经典二值逻辑。把公式落到查询语言时，应检查数据库的空值语义。

例如 is_admin 已知且非空，而 MFA 状态未知时，本例要求不能认定已满足规则。下面的完整查询可在 PostgreSQL 或 DuckDB 中运行：

sql
WITH users(user_id, is_admin, has_mfa) AS (
  VALUES ('admin-a', TRUE, CAST(NULL AS BOOLEAN)),
         ('member-b', FALSE, FALSE)
)
SELECT
  NOT EXISTS (
    SELECT 1 FROM users WHERE is_admin AND NOT has_mfa
  ) AS unchecked_claim,
  NOT EXISTS (
    SELECT 1 FROM users WHERE is_admin AND has_mfa IS NOT TRUE
  ) AS confirmed_claim;
-- unchecked_claim = TRUE, confirmed_claim = FALSE

第一列漏掉了 NOT has_mfa 在空值上产生的 UNKNOWN，因为 WHERE 只保留 TRUE；第二列用 IS NOT TRUE 同时捕获 FALSE 与 UNKNOWN。这是明确选择“未确认不通过”的策略。查询只核对该表快照，还需另行约束会话有效期与状态来源。布尔谓词语义见 PostgreSQL 比较文档。

一阶逻辑的能力边界 ​

有限命题公式可以用真值表判定。一般的一阶逻辑有效性没有一个对所有输入都保证停机并给出是/否答案的判定算法。已知且可枚举的有限域、受限片段或特定理论的 SMT 问题则可能可判定或在实践中有效求解。

这解释了为什么验证工具经常要求有限边界、限制量词形状，或在超时时返回 unknown。形式化并不意味着任何规格都能自动求解。

完成检查 ​

为多租户项目系统形式化以下规则：

  1. 每个项目恰好属于一个租户；
  2. 用户只能编辑自己租户中的项目；
  3. 每个项目至少有一个负责人；
  4. 不存在同时属于两个租户的用户；
  5. 并非所有管理员都能删除审计记录。

逐条标出讨论域、自由变量和量词作用域，并为量词顺序错误各写一个反例。

参考资料 ​

Built with VitePress | Software Systems Atlas

Copyright 2026 Steven Yang