逻辑、量词与规格说明

应用应允许管理员打开记录，或者在获得批准时允许记录的所有者打开它。程序员分别写出 (admin or owner) and approved 与 admin or (owner and approved)。两段代码看起来都合理，但未经批准的管理员会得到不同结果。哪一段符合需求？必须先确定陈述的含义，才能判断实现。

逻辑帮助我们明确：什么情况使陈述为真，变量在哪个论域中取值，以及什么证据能够确立或否定陈述。阅读算法和 AI 主张也需要这些能力：“每个输入”“存在一个模型”和“模型在这个样本上成功”提出了不同义务。改变一个量词，可能改变整个结论。

回忆检查：解释函数定义为什么必须包含定义域，以及为什么一个有效反例能否定全称恒等式。如果不清楚，请复习模块 01。本模块使用经典二值逻辑：在确定的解释下，命题非真即假。数据库空值、异常、未知信息和概率不确定性需要额外建模，不能悄悄作为这些真值表中的第三个值。

命题（proposition）是在给定情境下具有确定真值的陈述句。“七是奇数”为真，“七是偶数”为假；错误陈述仍然可以是命题。“请打开文件”是命令，“文件打开了吗？”是问题，本模块不为它们赋予真值。确定文件与观察时间后，“文件已打开”才有明确真值。

字母 $p,q$ 代表命题。赋值（valuation）为每个命题字母指定真或假。公式与当前赋值不同：同一公式可能在一个赋值下为真，在另一个赋值下为假。计算公式真值，就是按联结词定义处理输入；证明两个公式等价，则必须证明它们在每个赋值下输出相同。

否定 $\neg p$ 翻转真值。合取 $p\land q$ 当且仅当两者都真时为真。析取 $p\lor q$ 当至少一个为真时为真。数学中的“或”包含两者都真的情况。排他选择必须另写，例如 $(p\lor q)\land\neg(p\land q)$。日常语言有时把“或”理解为只能选一项，规格说明应明确消除这种歧义。

真值表（truth table）列出所有可能赋值。两个不同命题字母有四行，三个有八行。证明表中的恒等式，不必知道应用当前处在哪一行。相反，只观察今天发生的情况不能证明规则永远一致；遗漏的行可能正是规则需要处理的特殊情形。

括号表达结构。管理员规则是 $a\lor(o\land r)$，其中 $a$ 表示管理员，$o$ 表示所有者，$r$ 表示批准。最外层是析取。另一写法 $(a\lor o)\land r$ 最外层是合取，要求每次成功都获得批准。通常否定优先于合取，合取优先于析取，但明确括号更便于审核。字母相同不代表含义相同。

否定复合陈述时必须包含它失败的所有方式。“两个检查都通过”在任意一个失败时为假；“至少一个检查通过”只有在两者都失败时才为假。这得到德摩根律（De Morgan’s laws）：

$\equiv$ 表示公式的逻辑等价，而非两个数的相等。核对四行，再用语言解释规则，把机械计算与含义联系起来。

当输入为布尔值时，Python 的 not、and、or 符合这些定义。但 Python 也接受其他对象，and 和 or 可能返回操作数而非 bool。例如 "ready" or "" 返回 "ready"。这属于语言行为，不是新的逻辑真值。实验使用真正的 True 与 False，使对应关系明确。

蕴含 $p\Rightarrow q$ 表示：当前件 $p$ 为真时，后件 $q$ 必须为真。它只禁止一种情况：$p$ 真而 $q$ 假。因此真值定义为 $\neg p\lor q$。这叫实质蕴含（material implication），并不宣称 $p$ 导致 $q$，不宣称事件按时间顺序发生，也不宣称 $p$ 确实发生。因果与时间是另外的主张。

“如果请求获批，它有审核人”：令 $p$ 表示获批，$q$ 表示有审核人。未获批请求无论有没有审核人都不违反这条规则，因为规则只在获批情况下承诺。前件为假的真值行通常称为空真（vacuous truth），表示义务未被触发，而非已经找到审核人。

蕴含一般不等价于逆命题（converse） $q\Rightarrow p$。能被四整除蕴含偶数，但偶数未必能被四整除，六就是反例。否命题（inverse）为 $\neg p\Rightarrow\neg q$，一般也不等价。逆否命题（contrapositive）为 $\neg q\Rightarrow\neg p$，与原式等价：展开后分别为 $\neg p\lor q$ 与 $q\lor\neg p$，每个赋值下相同。

“$p$ 是 $q$ 的充分条件”表示 $p\Rightarrow q$，在规则成立时，知道 $p$ 就足以确立 $q$。“$q$ 是 $p$ 的必要条件”表示同一蕴含：没有 $q$ 就不能有 $p$。必要条件未必充分。例如审批要求审核人，但有审核人未必获批。反转方向会引入更强、可能错误的规则。

“$p$ 仅当 $q$”为 $p\Rightarrow q$，把 $q$ 作为必要条件；“如果 $q$，则 $p$”为 $q\Rightarrow p$。当且仅当（if and only if）要求两个方向，写作 $p\Leftrightarrow q$，两输入真值相同时为真。精确定义接受条件通常需要等价，而单向保证只需要蕴含。

由 $p$ 与 $p\Rightarrow q$ 推出 $q$，叫肯定前件式（modus ponens）；由 $\neg q$ 与 $p\Rightarrow q$ 推出 $\neg p$，叫否定后件式（modus tollens）。单凭 $q$ 不能推出 $p$，单凭 $\neg p$ 不能推出 $\neg q$。蕴含表中的行能暴露这些无效推理。

假设某检查通过保证记录有效。观察到有效记录，并不能证明这个检查执行过，因为别的过程也可能验证记录。检查未执行，也不证明记录无效。这是逻辑限制，与代码是否可靠无关。阅读 AI 定理时，不应把充分条件变成观察到成功的必要解释。

谓词（predicate）是真值依赖输入的陈述模板。“$x$ 是偶数”在赋值或量化前不是封闭命题。写作 $P(x)$，并声明如 $x\in\mathbb{Z}$ 的论域。如果输入改为实数，“偶数”就需要另行定义，整数概念不能自动扩展到所有数系。

没有被绑定的变量是自由变量。把 $x=6$ 代入 $P(x)$ 得到确定陈述；另一方法是量化。$\forall x\in D,\ P(x)$ 表示论域中每个元素满足谓词；$\exists x\in D,\ P(x)$ 表示至少一个元素满足。符号表达义务，并非只要写成程序循环就能检验任何论域。

构造性地确立存在陈述，需要给出见证（witness），并证明它属于论域且满足谓词。否定全称陈述，需要给出反例（counterexample），同样必须属于论域。负整数不能反驳只讨论非负整数的主张，分数解不能见证整数中的存在性。

有限论域可以逐一检查每个成员来确立全称陈述，也可找到一个见证后确立存在陈述。无限论域的有限成功搜索不能确立全称结论；但一个有效见证仍能确立无限论域上的存在性。找到整数解足以证明存在，而在某范围内找不到解不足以证明所有整数中不存在。

空论域上的全称陈述为真，因为没有违反它的成员；存在陈述为假，因为没有候选见证。Python 的 all([]) 与 any([]) 使用相同约定。空目录通过全称质量规则，并不说明有有用记录。如果需求要求存在，必须另写合取条件。

限制论域的陈述可展开为更大论域上的公式。“每个获批请求有审核人”为 $\forall r,\ A(r)\Rightarrow H(r)$；“有某个获批请求有审核人”为 $\exists r,\ A(r)\land H(r)$。全称限制使用蕴含，存在限制使用合取。第二句错误地使用蕴含，会让未获批请求因前件为假而成为见证。

常数与参数也需要明确作用域。$x>t$ 可以只量化 $x$，留下阈值 $t$ 为自由变量，于是 $\forall x\in D,\ x>t$ 依赖选定阈值。对固定数据集或模型的训练主张同样依赖这些选择，除非显式量化它们。“对这个模型”和“对所有模型”并非措辞变体。

实际规格应为每个谓词写出简短论域声明：本目录中的请求、当前注册审核人、零到长度减一的整数位置。这能防止把小目录上的真陈述理解为未来所有条目的承诺，也说明布尔表代表哪些对象、哪些未列情况超出范围。

令 $R(r,v)$ 表示审核人 $v$ 获准审核请求 $r$，请求论域为 $D$，审核人论域为 $V$。$\forall r\in D\ \exists v\in V,\ R(r,v)$ 表示每个请求有至少一个合适审核人。审核人的选择可以依赖请求，并不要求一个人处理全部请求。

在 $\exists v\in V\ \forall r\in D,\ R(r,v)$ 中，先选一个审核人，然后要求此人适合每个请求。这一般更强；公共审核人可以给每个请求作见证，所以它蕴含前式。逆方向可能因不同请求需要不同人而失败。量词顺序准确揭示选择可依赖哪些先前变量。

无限论域也受顺序影响。整数上 $\forall x\exists y,\ y=x+1$ 为真：给定 $x$，选 $y=x+1$。反过来的 $\exists y\forall x,\ y=x+1$ 为假：若同一 $y$ 对所有 $x$ 成立，它在 $x=0$ 时等于一，在 $x=1$ 时等于二，不可能。这是覆盖无限论域的论证，而非对有限整数样本的外推。

若谓词与固定论域不变，两个全称量词可交换，因为两种顺序都要求每个配对成立；两个存在量词也可交换，因为都寻找一个成功配对。这不允许任意交换混合量词。如果后一个论域依赖先前变量，必须先检查这种依赖。

全称的否定是存在否定；存在的否定是全称否定：

第一式说全称规则失败，因为有成员违反；第二式说不存在，因为每个候选都失败。从外到内应用规则，并保持顺序。否定 $\forall r\exists v\ R(r,v)$ 得到 $\exists r\forall v\neg R(r,v)$：有一个请求没有合适审核人。它没有要求所有请求都没有任何审核人，后者强得多。

量化蕴含还需要否定联结词。$\neg(p\Rightarrow q)\equiv p\land\neg q$，因此“每个获批请求有审核人”的否定是“存在获批但无审核人的请求”。批准条件保持肯定。只给结论加“不”并保持全称量词，不会正确描述原规则失败的所有方式。

括号与朗读能使作用域清楚。在 $\forall x\in D,\ (P(x)\Rightarrow Q(x))$ 中，两次 $x$ 都被绑定。将存在量词移入或移出蕴含会改变依赖。持续一致地重命名绑定变量不改变含义，改变论域或移动量词则可能改变。

程序约定连接允许的起始状态与承诺的结束状态。前置条件（precondition）说明调用前必须成立的事实；后置条件（postcondition）说明在满足前置条件时，调用结束的结果应满足什么。“前置条件成立且程序终止时，后置条件成立”是部分正确性主张；完全正确性还要求每个允许输入都会终止。模块 04 将证明这些义务。

前置条件应表达真实假设，而非隐藏难处理的有效情况。整数除法要求除数非零是合理的；搜索有限列表中的首次匹配时，若只为避免分析循环而要求首项已等于目标，就偏离调用者需要的操作。缩小论域可以合理，但必须明确并符合用途。

设列表 $a$ 长度为 $n$，目标为 $t$，搜索返回整数 $j$。精确后置条件是：

第一分支表示不存在；第二表示位置有效、目标匹配、之前没有匹配。仅要求 $a_j=t$ 不能保证首次出现，也不能描述缺失。范围限制避免把越界索引当作有意义的数学检验；代码中要先使用短路条件保护索引。

断言（assertion）是预期在某个指定程序点成立的陈述，可在开发中提供可执行反馈。调用后的断言检查部分后置条件；循环中的断言检查该执行过程中的候选不变式。通过这些检查是有用证据，却不证明所有执行都保持不变式；一般论证必须覆盖假设下可达的所有状态。

状态谓词需要观察点。“位置 $i$ 之前都已检查”可能在迭代开始成立；“位置 $i$ 也已检查”可能在结束成立。把断言跨过更新语句而不调整含义，可能产生差一错误。谓词、索引论域与代码行的位置关系是规格的一部分。

不是所有条件都应放进 assert。Python 优化模式可以禁用断言，所以调用者必须得到可靠拒绝的输入验证应使用普通条件与异常。这不改变逻辑语义，却影响运行时是否执行检查。本系列用断言捕捉内部不一致，用明确验证实现输入约定。

“训练结束就保存报告”不保证训练会结束；“记录被接受则校验和有效”不保证有效记录都会被接受。精确接受条件要写等价，完成要求增加终止义务，至少接受一条记录要增加存在性。分开承诺才能准确审核。

约定也说明模型之外的问题。有限批准表不描述谁能修改它、权限何时过期、身份如何验证；这些需要更多状态与谓词。明确一条小规则有价值，但不等于完整安全设计。固定数据生成假设下的定理，也不能自动确定真实数据是否满足该假设。

命题公式若在至少一个赋值下为真，则可满足（satisfiable）；在每个赋值下为真，则有效（valid）或为重言式；没有任何真赋值，则不可满足。可满足未必有效：$p\land q$ 四行中仅一行为真。$p\land\neg p$ 是矛盾式，任何赋值都为假。

这些词量化了赋值。固定有限命题字母的公式有有限完整真值表。穷尽全表可证明它有效，因为确实检查了论域中每个赋值；找到一行可证明可满足；全表都失败可证明不可满足。

这比为无限整数恒等式检查几个数更强。关键是是否穷尽完整论域，而非是否使用计算机。有限区间不能穷尽所有整数。有限目录可以穷尽，但结论只关于该目录，除非另有论证连接到更大的情境。

逻辑后承表示每个满足前提的赋值也满足结论。$p$ 与 $p\Rightarrow q$ 蕴涵 $q$，因为两前提都真的行不能让 $q$ 为假。如果前提不一致，就没有满足行，因此经典逻辑中的后承空真；但不一致规格仍无用，因为没有实现能同时满足全部要求。

检查规格时，应同时问约束能否满足，以及目标结论是否由它推出。“获批记录必须审核”“任何记录不得审核”“有获批记录”三者不一致。删去存在要求后，可通过不批准任何记录来满足，但这样的修复可能违反产品目的，尽管公式不再矛盾。

有限模型检查以明确的有限对象与状态为模型，可以找到违反需求的状态或配对。反例比布尔失败更有信息：它指出不一致的输入。保存并重现见证，解释有关公式，然后确定应修改代码还是原规则。

枚举也有限制。$m$ 个独立布尔输入有 $2^m$ 个赋值；小规则适合穷举，输入增加后会迅速昂贵。先进求解器可以利用结构，但仍需忠实规格。大型系统的抽样有用，但应报告为抽样，不能称为完整有效性检查。抽样通过概率也不同于全称真理。

AI 中“每个测试输入都分类正确”量化测试集；“每个未来可能输入都分类正确”量化另一通常大得多的论域。第二式不能从第一式换一个词就得到。统计论证在抽样假设下可以支持概率结论，后续模块会研究这些假设。逻辑先揭示差距，统计才可能衡量它。

使用 Python 3.11 或更新版本，在 Windows 可运行 python filename.py 或 py filename.py，其他系统按需使用 python3。把下载文件存入同一目录，在终端运行；设置方法见 Python 入门。无需安装包。执行前预测关键行，保存输入并解释真值。每次实验解释十分：预测三分，结果解释四分，故障或变化分析三分。

四十分钟：先写两个布尔输入的四种赋值，预测蕴含与逆命题列，然后运行。脚本检查逆否等价与两条德摩根律。解释为什么完整枚举能证明这些命题等价，却不能证明无关整数定理。把蕴含实现改成 p and q，保存一个不一致赋值并修复。结尾非布尔 Python 示例是语言区别，不是增加真值。

下载 lab1_truth_tables.py

"""Enumerate Boolean valuations; establish only the displayed equivalences."""
from itertools import product


def implies(p, q):
    return (not p) or q


def main():
    print("p q | not p | p and q | p or q | p -> q | q -> p")
    for p, q in product((False, True), repeat=2):
        values = (p, q, not p, p and q, p or q, implies(p, q), implies(q, p))
        print(" ".join(str(int(v)) for v in values))
        assert implies(p, q) == implies(not q, not p)
        assert (not (p and q)) == ((not p) or (not q))
        assert (not (p or q)) == ((not p) and (not q))
    print("Contrapositive and both De Morgan laws: all 4 valuations agree.")
    print("Converse mismatch at p=False, q=True:", implies(False, True), implies(True, False))
    print("Python non-Boolean example: 'ready' or '' =", repr("ready" or ""))


if __name__ == "__main__":
    main()

p q | not p | p and q | p or q | p -> q | q -> p
0 0 1 0 0 1 1
0 1 1 0 1 1 0
1 0 0 0 1 0 1
1 1 0 1 1 1 1
Contrapositive and both De Morgan laws: all 4 valuations agree.
Converse mismatch at p=False, q=True: True False
Python non-Boolean example: 'ready' or '' = 'ready'

四十分钟：$P(x,y)$ 表示 $y=x+1$。预测两组目录中的逐输入见证与公共见证。缩小第二论域会移除 $x=1$ 的见证，运行前指出失败。解释三个空论域情况，不要只记输出。把谓词改成 $y\ge x$，预测较大目录是否有公共见证。每条结论都写论域，脚本没有枚举所有整数。

下载 lab2_quantifiers.py

"""Witnesses over an explicitly finite catalogue, including empty domains."""


def investigate(xs, ys):
    predicate = lambda x, y: y == x + 1
    per_x = {x: [y for y in ys if predicate(x, y)] for x in xs}
    common = [y for y in ys if all(predicate(x, y) for x in xs)]
    every_has_some = all(any(predicate(x, y) for y in ys) for x in xs)
    some_for_every = any(all(predicate(x, y) for x in xs) for y in ys)
    negation = any(all(not predicate(x, y) for y in ys) for x in xs)
    assert negation == (not every_has_some)
    return per_x, common, every_has_some, some_for_every


def main():
    xs = (-1, 0, 1)
    for ys in ((-2, -1, 0, 1, 2), (-1, 0, 1)):
        witnesses, common, forall_exists, exists_forall = investigate(xs, ys)
        print("X =", xs, "Y =", ys)
        print("Per-input witnesses:", witnesses)
        print("Common witnesses:", common)
        print("forall x exists y:", forall_exists, "exists y forall x:", exists_forall)
    for xs, ys in (((), (0,)), ((0,), ()), ((), ())):
        result = investigate(xs, ys)
        print("Empty case X =", xs, "Y =", ys, "results:", result[2:])
    print("These checks concern these catalogues, not all integers.")


if __name__ == "__main__":
    main()

X = (-1, 0, 1) Y = (-2, -1, 0, 1, 2)
Per-input witnesses: {-1: [0], 0: [1], 1: [2]}
Common witnesses: []
forall x exists y: True exists y forall x: False
X = (-1, 0, 1) Y = (-1, 0, 1)
Per-input witnesses: {-1: [0], 0: [1], 1: []}
Common witnesses: []
forall x exists y: False exists y forall x: False
Empty case X = () Y = (0,) results: (True, True)
Empty case X = (0,) Y = () results: (False, False)
Empty case X = () Y = () results: (True, False)
These checks concern these catalogues, not all integers.

四十分钟：比较管理员例外与错误括号。预测八行有几行不一致，运行后解释为什么两处都有管理员且无批准。修复在完整布尔论域上检查。最后目录再现局部与公共审核人的区别；解释这为何是规格问题，而非布尔求值故障。

下载 lab3_access_rule.py

"""Find all counterexamples to a changed parenthesisation of an access rule."""
from itertools import product


def intended(admin, owner, approved):
    return admin or (owner and approved)


def faulty(admin, owner, approved):
    return (admin or owner) and approved


def main():
    print("Rule: admin OR (owner AND approved)")
    mismatches = []
    for admin, owner, approved in product((False, True), repeat=3):
        want = intended(admin, owner, approved)
        got = faulty(admin, owner, approved)
        if want != got:
            mismatches.append((admin, owner, approved))
            print(f"admin={admin}, owner={owner}, approved={approved}: expected={want}, faulty={got}")
        repaired = admin or (owner and approved)
        assert repaired == want
    assert mismatches == [(True, False, False), (True, True, False)]
    print("Repair agrees on all 8 Boolean valuations.")
    requests = ("r1", "r2")
    reviewers = ("a", "b")
    approved_pairs = {("r1", "a"), ("r2", "b")}
    per_request = all(any((r, v) in approved_pairs for v in reviewers) for r in requests)
    one_for_all = any(all((r, v) in approved_pairs for r in requests) for v in reviewers)
    print("Every request has a reviewer:", per_request)
    print("One reviewer covers all requests:", one_for_all)


if __name__ == "__main__":
    main()

Rule: admin OR (owner AND approved)
admin=True, owner=False, approved=False: expected=True, faulty=False
admin=True, owner=True, approved=False: expected=True, faulty=False
Repair agrees on all 8 Boolean valuations.
Every request has a reviewer: True
One reviewer covers all requests: False

练习 1–12 预计 110 分钟，每题五分；练习 13–14 可选，额外 25 分钟。写明论域、中间逻辑步骤与结论范围。只写最终真值不能得满分。

九道选择题自动评分，书面解释自评后得剩余一分。即使答对也读反馈。测验分数反映被测技能，不证明全部后续主张。

必读十五分钟：在 MIT Mathematics for Computer Science 链接的开放教材中，阅读命题章节的真值表与蕴含讨论。比较记法，并给出自己的假前件例子。

必读二十分钟：阅读同书谓词公式部分中的全称、存在量词与否定。选择一个混合量词陈述，声明论域，并说明哪个见证可依赖哪个变量。后续证明与归纳部分留到模块 04。

选读：查阅官方 Python 真值与布尔运算文档，解释 and、or 为何可返回操作数。本课定义与例子为原创，教材及文档用于进一步学习。

联结词定义决定真值行，真值行决定等价、可满足与有效。量词说明哪些论域成员必须成功，以及见证可以如何变化。规格连接允许输入与承诺结果，反例指出失败承诺。完整有限检查确立有限模型上的主张，无限主张需要覆盖论域的论证。

结业任务：为管理员规则写括号；翻译并否定请求—审核人需求；写首次匹配约定；解释完整布尔赋值与有限整数测试的区别。使用练习六十分、实验解释三十分、测验十分的课程评分。反馈后解释每个答案，不只依靠总分。

模块 03 使用这些规则定义集合、分类关系并证明成员恒等式。学习关系性质前，回忆“每个配对”“某个见证”与“并非每个”的含义。课程概览列出下一课的开放情况。