谓词逻辑速成课

我开始写作程序员逻辑因为当时没有适合程序员的好逻辑资源。现在书出版了，新的问题是没有好资源免费为程序员准备的逻辑资源。

所以，要解决那问题（也许还有点炒作这本书），我把《LfP》的第二章改成了一篇博客文章。所有脚注均为书中未包含的编辑评论。请欣赏！

第二章：逻辑速成课

形式逻辑是一个非常强大的工具，但它也非常简单。在本章中，我们将激励并解释基本概念和语法。这包括谓词、蕴含算子、集合和集合量词。

你可能已经通过编程经验熟悉很多内容！

谓词

从第一近似来看，谓词是一个返回布尔值的函数。作为程序员，你可能写过几十个谓词。这些都是谓词：

• Positive(x)当 x 大于 0 时 为真。
• IsSum(x, y, z)如果 x 加 y 等于 z，则为真。
• RAMAtLeast(c, r)如果计算机 成立c至少r物理内存的字节。

我说“对第一近似”是因为谓词是一个数学概念，而不是编程构造。程序函数需要附带计算答案的方法，而谓词只是定义答案。取RAMAtLeast：软件实现会依赖于编程语言、操作系统，甚至可能的物理硬件。

但谓词呢？如果计算机有内存，则为真;没有，则为假。仅此而已。

这意味着谓词可以比编程函数更抽象，表达一些我们甚至无法计算，或者至少还不知道怎么计算的事情。这些谓词同样有效：

• CanRunProgram(c)如果计算机 成立c能够运行我们的程序，无论“有能力”最终意味着什么。
• RainyDayInCa(date)如果 在 上，则为真date加拿大某地下雨了。
• NotAlone()如果外星人是真实存在的，那才是真的。

另一方面，Positive(x)计算简单：只需检查x > 0.谓词的力量在于它们可以跨越整个抽象范围。所以我们引入一些语法来区分抽象谓词和具体谓词。

如果谓词是抽象的，我会用“反向刻写”包裹主体：

# concrete
Positive(x) = x > 0
IsSum(x, y, z) = x + y == z

# abstract
CanRunProgram(c) = `c can run our program`

这不是数学界常见的惯例，但对我们来说足够清晰。用来区分谓词与“普通”函数，比如add_two，谓词总是TitleCase函数总是snake_case.

在你写的程序中找到一些谓词。这些是抽象谓词还是具体谓词？[^练习题]

解决方案

谓词通常是不改变程序或世界状态并返回布尔值的函数。我最近写的一个是document_has_exactly_one_foo.无论你找到什么谓词，都应该是具体的，因为实际上不可能编写出一个“抽象”谓词。

不过你可能会在设计文档中看到一两个抽象谓词。

既然谓词返回布尔值，现在是个好时机来做一些布尔运算。不同的编程语言有不同的符号表示AND、包含OR和NOT。数学家用∧、∨和¬。我是不是我打算用这些，因为键盘上没有这些。

我会用&&,||， 和!作为我们的象征。所以X && !Y意思是“X为真，Y为假”。

在三个常用的布尔算符之上，数学家还识别出第四个算符，=>.但在我们深入探讨这意味着什么之前，先试着练习刚才学到的内容。

一个实际例子

谓词作为我们用人类语言谈论系统的方式和用编程语言编码它们之间的桥梁。我们回到CanRunProgram.我曾经见过一个项目有以下要求：

电脑必须有足够的内存和快速的CPU，或者一块好的显卡（GPU）。

我觉得这很困惑。这句话在英语中听起来很自然，但我们可以通过逻辑形式化来找到问题。我们先为每个子需求写述谓词，如下：

RAM(c) = `c has enough RAM`
CPU(c) = `c has a fast CPU`
GPU(c) = `c has a good GPU`

这些谓词是抽象的，因为我们不知道它们具体意味着什么。64GB“够内存”吗？32GB吗？具体细节对我们来说无关紧要，因为这已经足够写入CanRunProgram作为一个具体的数学表达式。

CanRunProgram(c) = RAM(c) && CPU(c) || GPU(c)

现在问题更清晰了：是a && b || c应当被解读为(a && b) || c或当a && (b || c)?谓词形态不对，我们有两种不同的方式让它有意义：

# way 1
CanRunProgram(c) = RAM(c) && (CPU(c) || GPU(c))

# way 2
CanRunProgram(c) = (RAM(c) && CPU(c)) || GPU(c)

这两种解释在英语中都很合理！但它们在某些输入上有不同的输出。我们可以通过列出RAM/CPU/GPU所有可能的值组合，看看它们给出的CanRunProgram.这被称为真值表。

有两种输入组合，一种解释给出“假”，另一种给出“真”。供应商有可能意思是在编写要求时，这是第一种解释，但我阅读这是第二种解释。

我确定程序能在我的电脑上运行，它失败是因为内存不足，我觉得厂商骗了我。用数学方法表达需求要好得多！

用形式逻辑表达属性比用非正式英语更不含糊。为了教学，我们假设预期谓词为(RAM(c) && CPU(c)) || GPU(c).

本章我们将使用真值表进行案例分析决策表.

如果你在生成真值表时遇到困难，可以尝试使用真值表生成器。我提供了一个简单的生成器给你.试试看p || !q然后再去尝试。

为 制作一个真值表!P && !Q以及!(P || Q).

解决方案

这些是一样的。这被称为德摩根定律。

条件谓词

现在让我们对谓词做一个变体。对于我们的CanRunProgram举个例子：有些程序有原生版本和网页版。原生版本使用本地计算机的资源，而网页版在某个云端电脑上完成大部分处理。

所以原生版本需要一台高性能的电脑，但任何电脑可以运行网页客户端。

如果电脑运行的是原生版本，它必须有足够的内存和快速的CPU，或者需要好的显卡（GPU）才能使用这个程序。但如果不是运行原生版本，那就没问题。

为了建模这一点，我们需要一个新的谓词，Native(p).Native是程序的属性，而非计算机的属性，因此CanRunProgram则取决于两者：

CanRunProgram(c, p) = `true unless Native(p),
  in which case (RAM(c) && CPU(c)) || GPU(c)`

我这里用回溯记号是因为谓词一半仍是非正式英语。事实证明，我们已经具备了使其具体化的工具。当Native(p)是错误的，CanRunProgram(c, p)这应该自动成立：我们甚至不需要看电脑规格。

CanRunProgram(c, p) =
  !Native(p) || ((RAM(c) && CPU(c)) || GPU(c))

这是怎么运作的？如果我们把右边抽出一个新的谓词，会更容易看出，比如Beefy(c)，因此我们有!Native(p) || Beefy(c).这是该表达式的真值表（使用N(p)对于Native(p)以及B(c)对于Beefy(c)):

当Native(p)是错误的，!Native(p) || Beefy(c)无论 值如何，都为真Beefy(c).当Native(p)成立，则表达式等于Beefy(c).所以我们只在运行原生版本时查看电脑配置，其他版本则忽略。

写作技巧!P || Q意思是“检查”Q仅当P“是真的”在数学中非常常见。如此普遍以至于数学家们会用特殊算子来表示：=>，或含义算符。P => Q（“P 蕴含 Q”）与写作相同!P || Q.这样表达，我们的谓词为：

CanRunProgram(c, p) =
  Native(p) => (RAM(c) && CPU(c)) || GPU(c)

=>绑定比&&以及||:A && B => C是(A && B) => C，不是A && (B => C).

蕴含算符非常强大，在很多地方都很有用，比如编写规范或制作系统模型。我们可以用它来说明某个布尔语句比另一个“更强”。例如，“this code crashs when pass a 0”比“this code contains a bug”更强。

如果某个输入崩溃，肯定包含bug！但即使程序没有崩溃，也可能出现像“offby-by-one”这样的错误。或者，用数学方式写成：

CrashesOnInput(code, 0) => HasBug(code)

蕴含也非常有用，因为它是传递性的。如果P => Q以及Q => R那么我们知道P => R，无论P、Q和R实际上是什么。如果CanRenderVideo(c) => CPU(c) && RAM(c)，则CanRenderVideo(c) => CanRunProgram(c).

假设我们再加两个条件，使得CanRunProgram是

CanRunProgram(c, p) =
  `true unless Native(p) and either Q(p) or R(p),
  in which case (RAM(c) && CPU(c)) || GPU(c))`

写这句话时可以用=>.然后不使用=>.哪个更容易读？

解决方案

1. Native(p) && (Q(p) || R(p)) => (RAM(c) && CPU(c)) || GPU(c)
2. !(Native(p) && (Q(p) || R(p))) || ((RAM(c) && CPU(c)) || GPU(c))

我个人觉得（1）更容易阅读，因为我们没有那么多嵌套表达式。

RAM(c)意思是“计算机”c内存充足“。修改为”计算机”c有足够的内存来运行程序p”.对其他谓词也做类似的修改，然后写CanRunProgram.

解决方案

CanRunProgram(c, p) =
  Native(p) => (RAM(c, p) && CPU(c, p)) || GPU(c, p)

1. 使用=>，写成表达式“如果Native(p)则 为真Web(p)是假的，且如果Web(p)则 为真Native(p)是错误的“。
2. 使用&&，写下表达式”Native(p)以及Web(p)两者都不成立“。
3. 使用||，写下表达式”Native(p)是假的，或者Web(p)是错误的“。

解决方案

1. (Native(p) => !Web(p)) && (Web(p) => !Native(p))
2. !(Web(p) && Native(p))
3. !Native(p) || !Web(p)

假设谓词：

IfElse(c, x, y) =
  (c => x) && (!c => y)

假设c、x和y都是布尔值。

1. 当IfElse是真的？当它是假的吗？
2. 这通常是什么常见的代码构造？

解决方案

1. (c => x) && (!c => y)等价于(!c || x) && (c || y).如果你通过案件处理，你应该会发现IfElse当c为真且x是真的，或者当c是假的，且y是真的。
2. 正如名字所示，IfElse是模拟条件句。

套装

谓词默认有未类型输入。在CanRunProgram(c),c可以是一台计算机，但c也可以是机器人，或者数字26，或者字符串“数字26”。在编程中，我们希望给它一个类型，明确表示只应传递给计算机。

类似这样的：

CanRunProgram(c) = `c is a computer`
    && ((RAM(c) && CPU(c)) || GPU(c))

现在，即使我们把一个好的GPU粘在贵宾犬上，CanRunProgram(poodle)仍然为假。为了使“c 是计算机”的概念在数学上可表示，数学家使用集合。

集合是一组无序的唯一值集合，如“所有计算机”、“所有 500 千字节以下的网页”或“所有有效 Java 程序字符串”。通常，我们这样写集合的元素：

Computer = {my_laptop, your_laptop, your_other_laptop, ... }

那么“c 是计算机”等价于说“c 是集合的一个元素”Computer”.我们写作c in Computer.

CanRunProgram(c) = c in Computer && ((RAM(c) && CPU(c)) || GPU(c))

为了让我们的谓词定义更简洁，我借用一个常见的编程语法，写成CanRunProgram(c: Computer)意思是”c必须是 的元素Computer“，像这样：

CanRunProgram(c: Computer) = (RAM(c) && CPU(c)) || GPU(c)

这将使编写包含多个受限参数的谓词变得更容易。

数学家把集合当作数学基石，可以用来构建更复杂的概念。例如，他们可能用集合定义对，写为(a, b)作为{a, {b}}，然后定义列表[a, b, c]为一对的集合{(0, a), (1, b), (2, c)}.然后，通过基于集合的列表“抽象”实现，他们可以丢弃集合，直接处理列表。

作为程序员，我们不需要在使用列表前写出正式定义，更倾向于处理更复杂的抽象。即便如此，集合仍然是有用的编程数据类型。我们将在下一章中看到这一点。

集合运算

就像我们有数字算术和布尔算术一样，我们也有集合算术。给定集合{A, B}以及{B, C}，我们能做的基本事情有：

1. 将它们合并，或者合并成一个大集合：{A, B} | {B, C} == {A, B, C}
2. 将它们相交，或者找到共同元素：{A, B} & {B, C} == {B}
3. 取集合差，或从其中一组减去另一组：{A, B} - {B, C} == {A}

我们也可以检验一个集合是否是另一个集合的子集。EvenIntegers是 的子集Integers因为 的每个元素EvenIntegers也是 的元素Integers.该价值 2不是 的子集Integers，但场景 {2}是。

子集类似于编程语言的子类型。如果一种语言说Rectangle是 的一个子类型Shape“，这意味着所有矩形的集合是所有形状集合的子集。我们将作为合同这一更广泛主题的一部分，更详细地探讨子类型化。

1. 使用这些套装ram,cpu， 和gpu构造集合can_run_program，所有通过的计算机的集合CanRunProgram(c).
2. 给定集合Child以及Adult表达“没有人既是孩子又是成年人”，即说这两个集合不重叠。你可以使用{}意指空集合。
3. 该对称差两个集合的集合是这两个集合中恰好一个元素的所有集合。例如，的对称差{A, B}以及{B, C}是{A, C}.仅用基本集合运算，求任意集合的对称差S以及T.

解决方案

1. can_run_program = (ram & cpu) | gpu
2. Child & Adult == {}.另一种方式是Child - Adult == Child && Adult - Child == Adult.
3. 一种方式是(S - T) | (T - S);另一个是(S | T) - (S & T).

它对映射和过滤集也非常有用。标准数学符号是{f(x) | P(x)}但我发现初学者会搞混哪边是地图，哪边是过滤。所以这本书我会用更明确的语法：

例如，所有偶数的集合为{x in Int: x % 2 == 0}所有偶数平方根的集合为{sqrt(x) for x in Int: x % 2 == 0}.这有时被称为集合理解或集合构建符号。

后来，集合理解成为我们理解数据库查询的基石。

岁月Images为一组图像，每张图像为记录，包含名称、高度、宽度和大小字段（千字节）。写出集合理解：

1. 所有图像名称的集合。
2. 所有大于10 kb的图像集合。
3. 方形图像的所有高度集合。

解决方案

1. {img.name for img in Images}
2. {img in Images: img.size > 10}
3. {img.height for img in Images: img.height == img.width}

量词

让我们暂时放开软件需求，转向另一个问题。软件开发团队通常要求对主代码的修改首先作为拉取请求的一部分提出，而该请求必须由其他团队成员审核。

更简洁地说：

拉取请求必须由团队成员审核后才能合并。

假设有两个集合，PullRequest以及Developer，我们可以在谓词中使用。我可以从这些抽象谓词开始表达规则：

ReviewedBy(pr: PullRequest, d: Developer) =
  `d reviewed pull request pr`

CanMerge(pr: PullRequest) = `someone reviewed pr`

这两个谓词都是抽象的，但看起来我们应该能够CanMerge通过定义具体ReviewedBy.

为此，我们需要一个量词，或者一个作用于整集合的逻辑表达式。谓词逻辑中有两个常见的量词。第一个，也就是我们这里要用的，叫做some.

有些

some x in set: P(x)意味着P(x)对于 为真至少有一个 x在该集合中set.

CanMerge(pr: PullRequest) =
  some d in Developer: ReviewedBy(pr, d)

我会把这理解为”CanMerge对于拉取请求元素成立pr如果至少有一个元素d在显元组中，其中ReviewedBy(pr, d)是真的“。或者，简单来说就是”有开发人员审核了拉取请求“。

价值d称为变量。令牌some是对集合进行量化的Developer或者，或者，作用域为该集合。这使得我们对它的使用成为一个有作用域的量词。

更罕见的是，表达式对我们想命名的任何值都成立。例如，陈述some x in set: (P(x) && Q)是相同的Q && some x in set: P(x)，无论如何set是。

在这种情况下，我们可以选择不包含集合，写成：

(some x: (P(x) && Q)) == (Q && some x: P(x))

这种some没有作用域到集合，因此我们称之为无作用域量词。我们几乎所有使用的内容词都是作用域的。

为了防止远古数学恐怖，我们只能量化集合和值，不能量化谓词。[^function-sets]如果你想了解更多关于远古数学恐怖的信息，请查看附录超越逻辑.

全部

目前情况是，CanMerge太宽松了。如果审核员发现了重大安全漏洞怎么办？如果五名开发者审查拉取请求，其中两名发现了缺陷怎么办？

大多数公司采用更严格的合并要求：

拉取请求必须至少由一名团队成员审核，且所有审核员必须批准该请求，在合并之前。

按照我们的习惯，我们先用抽象谓词来写需求。

ApprovedBy(pr: PullRequest, d: Developer) = `d approved pr`

SomeoneReviewed(pr: PullRequest) =
  some d in Developer: ReviewedBy(pr, d)
EveryoneApproves(pr: PullRequest) =
  `everyone who reviewed pr also approved it`

CanMerge(pr: PullRequest) =
  SomeoneReviewed(pr) && EveryoneApproves(pr)

这为引入另一个量词——所有——提供了机会。all x in set: P(x)说P(x)对所有 都成立x在我们的套装里。有了这个，看起来比如我们的新谓词可以写成这样：

EveryoneApproves(pr: PullRequest) =
  all d in Developer: Approved(pr, d)

但这不对：它要求每一位开发者都必须批准拉取请求，包括病假或育儿假的开发者。我们只想要求所有审核拉取请求的开发者都批准了。

我们可以默示修正这一点。请记住P => Q手段!P || Q.则ReviewedBy(pr, d) => Approved(pr, d)意味着d是批准了拉取请求，还是根本不审核。

EverybodyApproves(pr: PullRequest) =
  all d in Developer: ReviewedBy(pr, d) => Approved(pr, d)

我们经常用=>仅为all在元素的子集上。

大多数编程语言都有内置量词函数，我们将在后面章节详细讨论。如果你选择的语言没有，通常可以用循环来近似量词。例如，你可以写SomeoneReviewed像这样一个伪代码：

fun SomeoneReviewed(pr: PR) {
  for (d in developers) {
    if(ReviewedBy(pr, d)) return true;
  }
  return false;
}

我们为什么需要SomeoneReviewed一点都不？如果所有审核过PR的人都批准了，那就一定有人审核过，不是吗？找出一个边缘情况，比如EveryoneApproved是true以及SomeoneReviewed是false.

解决方案

如果没有任何开发者审核过PR，那么EveryoneApproved是真的（所有评审者都认可！）SomeoneReviewed是错误的（没人审核过）。

一般来说，all x in {}: P(x)总是成立的（无论如何）P是）和some x in {}: P(x)总是假的。

定义Nat作为自然数的集合：0、1、2 等。

1. 写出逻辑陈述“每个自然数都小于自身加1”。
2. 写出逻辑陈述“0小于或等于每个自然数”。

解决方案

1. all x in Nat: x < x + 1
2. all x in Nat: 0 <= x

1. 写下逻辑陈述：“每一个PR，都有开发者批准它”。
2. 写下逻辑陈述：“有开发者审核了每一个拉取请求”。

这两种情况下，你都需要把一个量词放进另一个量词里面。

解决方案

1. all pr in PR: some d in Developer: ApprovedBy(pr, d)
2. some d in Developer: all pr in PR: ReviewedBy(pr, d)

能力与保证权衡

既然我们已经看过两者all以及some我想指出一件重要的事：some x in set: P(x)对于大集合，更可能成立，且all x in set: P(x)对于小集合，更可能成立。

如果我们有两个不同的集合和set1是 的子集set2我们应预期会找到某个谓词P(x)其中all x in set1: P(x)以及some x in set2: !P(x).我们可以说set1担保P(x).让我们来看三个例子：

1. “所有 ASCII 字符”集合是“所有 Unicode 字符”集合的一个子集。ASCII 保证/保证每个可表示字符恰好包含一个字节，所以我可以查看字符串ABC并且立刻知道是三个字节。Unicode 并不保证这一点，字符串ABC如果用西里尔字母，可能有六个字节。
2. “我们能通过只读访问文件做的事情”集合是“我们能用完全访问文件做的事情”的一个子集。只读访问保证程序不会更改文件内容。而完全访问时，任何有漏洞的程序都可能覆盖我们的数据。
3. “所有只使用布尔、AND、或和NOT的逻辑公式”集合是“所有逻辑公式”的一个子集。前者保证每个公式都可以转化为真值表。如何制作一个真值表some x in Nat: OddPerfectNumber(x)?你不能。数学家们至今还不知道它是不是真的！

同时，我们需要Unicode来表示表情符号，写入权限以更新数据，并设置量词以表达最有趣的谓词。这就是能力与保证的权衡：语言、格式或工具能做的事情越多，它保证的事情就越少。

我们几乎会在本书的每一章中看到这种权衡。

重写规则

在书的开头，我说逻辑是布尔数学，就像算术是数字的数学一样。懂算术让我们简化数值表达式。例如，我们如何简化函数f(x, y) = -10x + 2(y + 5x):

1. 2(y + 5x)是相同的2y + 10x.
2. -10x + 2y + 10x是相同的10x - 10x + 2y.
3. 前两项是相反的，所以它们相互抵消。
4. 所以我们刚刚有了f(x, y) = 2y.

在逻辑中，这些简化被称为重写规则。你小时候可能已经用过一条重写规则：

你后悔吗？不吗？那你不是不后悔吗？

这里的重写规则是!!a == a.这意味着!!(!!Sorry)是相同的Sorry.

我们在逻辑中常用的一些重写规则包括：

蕴涵算子也有重写规则。其中一个，对位时，对我们非常有用。

量词也有重写规则：

常数提取适用于任何满足||或&&.分发只适用于some/||以及all/&&.

有些规则出现的频率比其他规则高。今后我们将大量使用德摩根定律、逆否定律和量词对偶性。更详细的列表已加入重写规则.即使是小众规则，在重构代码时也很有用。

使用重写规则来简化!(some x: !P(x)).

解决方案

all x: P(x)

请举一个每种分布规则的真实例子。

解决方案

这里有两个我想出来的：

1. “本周所有日子都温暖晴朗”与“本周所有日子都温暖且阳光明媚”是一样的。
2. “某人有蓝眼睛或绿色眼睛”与“某人有蓝眼睛或有人有绿色眼睛”是一样的。

some只有 在 上分配||以及all只有 在 上分配&&.找到满足的谓词：

1. (some x: P(x)) && (some x: Q(x)) != some x: P(x) && Q(x)
2. all x: P(x) || Q(x) != (all x: P(x)) || (all x: Q(x))

提示：无论哪种情况，都让左边为真，右边为假。

解决方案

答案很多，这里只有两个（假设如此）Person是所有曾经存在过的人的集合：

1. (some p in Person: Alive(p)) && (some p in Person: Dead(p))是真的，some p in Person: (Alive(p) && Dead(p))是错误的。
2. all p in Person: Alive(p) || Dead(p)是真的，all p in Person: Alive(p) || all p in Person: Dead(p)是错误的。

定理

你可能听说过数学家试图证明定理。定理只是一个永远为真的数学陈述，而证明则是一套清晰的步骤，让你从已知的真理到证明定理为真。

我列出的每个重写规则都是定理，我们可以证明它们总是有效的。以逆否认号为例。为了证明我们总能重写!Q => !P进入P => Q， 我们：

1. 从以下开始!Q => !P.
2. 应用含义的定义，得到!!Q || !P.
3. 去除双重负面以得到Q || !P.
4. 再次应用蕴含的定义，得到P => Q.

瞧，我们刚写了证明！试着从另一边开始P => Q.

从这里开始P => Q并重写为!Q => !P.

解决方案

首先将其重写为!P || Q.然后替换Q其中!(!Q)要获得!(!Q) || !P.然后将其重写为!Q => !P.

大多数定理可以用多种方式证明。这里有一个完全不同的逆变重写规则的证明：

1. 绘制 的真值表P => Q以及!Q => !P.
2. 它们是一样的。

定理是数学的基础。定理告诉我们逻辑工具（如逆否定律或德摩根定律）是否真正有效。我们可以使用逻辑机制，而不必知道支持它们的定理，就像我们知道的一样117*92 == 92*117无需先写证明。

话虽如此，我们也可以证明关于代码的定理，这是我们将在单独章节中讲述的专业话题。

符号

数学家喜欢说逻辑是一种“语言”。语言的意义在于清晰地传达复杂的思想，有时最好的方式就是创造新的词汇和语法。

在逻辑中，只要1）保持一致，2）我们能清晰解释符号，我们可以提出新的构造和公式写法。事实上，这种做法是被鼓励的。例如，“1到10之间的整数集合”的常规写法占用了大量空间：

{1, 2, 3, 4, 5, 6, 7, 8, 9, 10}

如果我想更简洁，我可以想出一个简短的说法：

{1, 2, 3, ... 100}

如果我想更简洁，我可以定义新的语法：

1..=100 = {1, 2, 3, ... 100}
1..<100 = {1, 2, 3, ... 99}

这并非完全无歧义：什么是10..=9?我定义为空集：如果a > b，则a..=b是空的。类似地，a..<b当 是空的a >= b.

重写那条规则（如果a > b，则a..=b是空的）利用all量词。假设两者都有a以及b都属于整数集合。

解决方案

all a, b in Int: a > b => (a..=b == {})

写1..=100使用集合滤波器符号。集合上的滤波器Int.

解决方案

{x in Int: 1 <= x && x <= 100}

写IsDivisibleBy(num, divisor)，如果 ，则成立num可被整除divisor.用途some以及..=.

解决方案

IsDivisibleBy(num, divisor) =
  some x in 1..=num:
    x*divisor == num

我觉得另一个非常有用的符号是合取列表。复杂的系统通常有复杂的要求：

Rules = A && B && (C || D) && (E || (F && G))

这很难读！为了更容易理解，我们不如这样写：

Rules =
  1. A
  2. B

  3. || C
     || D

  4. || E
     || a. F
        b. G

像这样的数字4.以及像这样的字母a.总是表示 AND。如果我想要一个 OR 列表，我总是用||.

摘要

• 谓词是一种可以定义在任意输入上的布尔函数。
• 集合是唯一元素的无序集合。集合可以包含任何类型的值，唯独谓词除外。
• 量化表达式是对集合中每个（或任一）元素进行检查的表达式。
• 数学符号是灵活的。只要清晰且一致，我们可以提出新的符号、运算符和语法。
• 逻辑公式可以重写和简化。

以下是我们学到的所有符号和语法：

• 谓词总是TitleCase(x).函数总是小写，且snake_case(x).
• 或者，或者，不：&&,||,!
• 暗示：=>
• 集合并集、交集、差分：|,&,-
• 设置地图和筛选：{x^2 for x in set: x > 2}
• 量词：all x以及some x
• 各种句法糖。

就这些！这就是形式逻辑的所有基础。考虑到情况，其实也没多少。

难点当然在于应用。知道除法是一回事，但意识到“用5个鸡蛋放大食谱只用3个鸡蛋”其实是除法问题，完全是另一回事。书的其余部分讲的是软件场景中逻辑有用的方法，以及如何制造它很有用。

让我们用逻辑来理解这个世界。

了解更多

本章仅是数学逻辑基础的非常宽泛概述。更全面且详尽的论述包括（按复杂度递增）罗伯特·S·沃尔夫的数理逻辑之旅迈克尔·赫斯和马克·瑞安的计算机科学中的逻辑，以及理查德·爱泼斯坦的经典数理逻辑.

我们所讲的逻辑被称为一阶逻辑，因为谓词不能作为集合中的值，也不能传递给其他谓词。高阶逻辑能力更多，保证更少;详见附录超越逻辑更多信息。

没有谓词和量词的逻辑（仅包含布尔、AND、或和NOT）称为命题逻辑。

正式名称some以及all分别是存在量词和全称量词。数学家使用符号∃和∀。量化表达式有一些句法变体;见附录数学符号更多。

能力与保证权衡中的“能力”有时也被称为“力量”，如最小幂规则（更倾向于用“最弱”的编程语言来解决任务）。我也见过“保证”称为“功率”。

由于“功率-功率权衡”不明确，我们在本文中避免使用“功率”一词。

《程序员逻辑》现已发布于电子书以及树书格式。请访问官方网站了解更多信息!

1. 先说明一下期望：这本书基于一阶经典逻辑，因为这足够你驱动几百页的应用。没有建设性逻辑，没有λ演算，没有Curry-Howard法典等等。目标读者是那些不懂行的人任何数学。
2. 一真的我做过一个重要的设计决定：“书中用到的所有数学都应该能在标准美式键盘上打字”。大多数“官方”数学符号都是手写的，这让它们在电脑上使用起来非常困难！
3. 博客文章的用途是OR代替||在表格中表示，因为||拆解Markdown表格格式。
4. 未显示：这本书有大量索引和相互链接;这条以及所有其他“这对某某有用”的评论都有其他章节的页码。
5. 我最初是在通讯中探讨这个想法的有些测试比其他的更强;书中第四章用它来激励属性测试。
6. 是的，呃，好的，在审阅这篇帖子时我刚意识到我搞错了，对的实际数学惯例实际上是{{a}, {a, b}}.抱歉如果这毁了整本书。至少现在已经在勘误表里了.
7. 这本书用了基于0的索引来做列表（除非讨论的是其他语言），自然数从0开始。不同的数学分支有不同的惯例，我只是遵循大多数程序员习惯的做法。
8. 这本书做了一件事不是Cover是类型理论。这有几个原因，主要是我找不到简单、实用和实际逻辑的平衡。它确实涵盖了一些基本内容，比如使非法州变得难以代表以及Liskov子型。
9. 我在制作这个模型时学到了一个极其糟糕的事实：SVG标准中“点”定义为1/72英寸，而TeX定义“点”为1/72.27英寸。我在这里写了更多关于历史的内容.
10. 给它起个该死的名字花了很久。我以前叫它能力与可处理性权衡但这本书本身就够矫揉造作了。感谢切尔西特洛伊终于想出可行的东西。
11. 这是书中最棒的主意。我喜欢连词表。