这篇博客是Micheal Huth和Mark Ryan写的《计算机科学中的逻辑》这本书的一个简单介绍[1]。它会讲到书里第一章的前五个部分。为了让事情简单点，这个介绍写得很随意。所以，书里很多复杂的定理和证明这里都没提。
陈述句
我们检查程序对不对，主要就是想看看程序代码是不是按照我们想的那么运行。有很多方法可以做到这一点：
- 你可以写一堆测试，看看程序在不同情况下是不是正常工作。
- 你也可以写个模糊测试器，用随机输入不停地跑程序，确保它不会出错。等等。
但这些方法的问题是，总有点不确定。你怎么能确定只用几个测试就能保证程序完全没问题呢？可能有些情况你没测到，结果就出错了。
这就是形式化方法的好处：它们不会给错误留任何机会，可以用来检查程序是不是总是按我们想的那么运行。
不过，要用这些方法，我们首先得有个非常详细的程序说明。这些方法之所以叫“形式化”，是因为它们用数学技术来验证程序对不对。所以，我们需要一个程序说明，这样我们才能严格地提出和证明我们的观点。
我们可能会本能地用自然语言来写这个说明。毕竟，用自然语言描述东西对我们来说很自然：这就是你和朋友聊天或和同事争论的方式；我们习惯用这种方式表达和思考。但是，自然语言不适合写程序说明——这样做就像用画笔的毛来拧螺丝一样。问题是自然语言太复杂，太模糊了。想想这句话：
男人用望远镜看见了女人 |
这句话可以有两种理解：
- 男人通过望远镜看到了女人。
- 男人看到了一个拿着望远镜的女人。
在现实生活中，我们通常会根据上下文猜出正确的意思，或者让对方解释清楚。但
是，在做数学论证时，绝对不能有歧义，所以我们需要别的东西：一种更简单的语言，可以清楚地表达我们的意思，一种有明确规则并且可以推理的语言。
如果我们想让计算机自动帮我们做这种正确性检查，那么它得足够严格，这样我们才能写程序来验证和处理这种语言里的句子。
虽然自然语言不适合做这个，但它很熟悉。所以，我们先从思考开始，看看能不能想出更简单的东西。
我们通常用陈述句来论证；这些句子描述了世界的一些事情。比如，看看下面两个英文句子：
如果下雨而我没有带伞，那我就会被淋湿。下雨了，但我没被淋湿。 |
和
如果一个矩阵是方阵，且其行列式不为零，则该矩阵是可逆的。该矩阵是方阵，但不可逆。 |
你能从这些句子中推断出什么？你会怎么证明？虽然这两个句子说的东西完全不同（一个是常识，另一个是关于线性代数），但它们的结构是一样的，论证的结构也一样。
比如，从第一句话我们可以提出这个论点：
我没有被淋湿。所以，下雨而我没有带伞这不可能是真的。既然我知道下雨了，那就意味着我带了伞。
同样，从第二句话开始，我们可以几乎一样地重复这个论点，只需要换几个词！
该矩阵不可逆。所以，它是方阵且行列式不为零的说法不成立。因为我知道它是方阵，所以行列式一定为零。
另外，如果我们忽略句子的实际意思，只关注它们的结构（并对我们刚刚提出的论点做同样的事情），你会发现它们是一样的：
- 如果 x 且不是 y，则z
- 不是 z，且 x， 所以y
所以现在我们知道了，我们感兴趣的不是句子的内容，而是它们的逻辑结构，因为这是我们可以推理的。我们可以用这些陈述句描述我们喜欢的任何东西，然后用它们的结构提出合理的论证。
主要思想总结：
- 为了验证程序的正确性，我们需要对其行为进行可论证和推理的描述。
- 自然语言不适合写这些说明，因为它复杂且含糊不清。
- 在自然语言中，我们用陈述句来描述世界，并用它们的结构来进行论证。
命题逻辑
正如刚才展示的，我们可以用陈述句来描述世界，并且为了推理这些描述，我们需要处理这些句子的结构。但是，我们还在用自然语言，这意味着还是有一些问题。比如，看看下面三个句子：
- 我今天没有做饭，但是冰箱里还有剩菜。
- 冰箱里有剩菜，今天我又没有做饭。
- 因为冰箱里还有剩菜，所以今天我没有做饭。
它们都传达相同的信息。这三个句子之间的唯一区别在于向读者呈现信息的方式。在对话环境中，这些细微的差异非常重要，但就我们的目的而言，我们并不关心。对我们来说，所有这些变化只会使语言更难使用。
想象一下，编写一个程序或解析器来提取这些信息会有多难，即使是对于简单的英语句子！所以，我们的语言应该有更简单的语法，并且只关注信息的结构。记住上一节中的内容，我们实际上并不需要知道这些“陈述句”究竟在讲述什么。
所以我们将用单个字母来表示无法进一步分解的陈述：命题原子。
它们可以是真，也可以是假。然后，我们将用一组连接词将这些命题原子连接成更有趣的公式。以下是规则，并附有一些例子：
假设第一个命题原子 p表示“现在是冬天”。假设第二个命题原子 qq表示“天气很冷”。那么：
连接词 ∧ 类似于英语中的“and”。它表示两边的陈述或公式都是真的。
- 比如，p∧q表示“现在是冬天，天气很冷”。
- 连接词本身称为“连词”，两边的东西称为“连词”。
- 当且仅当两个连词都为真时，整个连词才为真。
类似地，∨类似于英语中的“或”。它表示至少有一个陈述为真。
- p∨q 表示“现在是冬天或天气很冷”。
- 该操作称为析取，两侧的公式称为“析取”。
- 如果至少有一个析取为真，则整个析取为真。
¬ 是所有运算符中唯一一个不真正将两件事联系在一起的运算符 - 它只是反转一个公式，就像英语中的“not”一样。
- 比如，¬p的意思是“现在不是冬天”。
- 这个操作称为否定，如果你要否定的东西是假的，那么它就是真的。
最后一个联结词是 →→，称为“蕴涵”。它就像英语中的“如果……那么……”，所以顺序很重要！比如，p→qp→q 表示“如果是冬天，那么天气很冷”，而 q→pq→p 表示“如果天气很冷，那么天气就是冬天”。
- 箭头左侧的公式称为“前件antecedent”，箭头右侧的公式称为“后件consequent”。
- 只有当前件为真且后件为假时，蕴涵才为假。
关于这些连接词，还有一些值得一提的事情。
第一个与析取有关：它被引入为类似于英语中的“或”一词，但有一点不同。
在英语中，当我们说“a 或 b”时，我们通常是指其中一个，而不是两个。这就是所谓的排他或，因为我们排除了两个选项为真。然而，析取是包容性的——如果两个析取项都为真，它仍然为真。
下一个例子是为了强调在处理逻辑蕴涵时顺序确实很重要。考虑以下语句
- 如果我正在做面包，那么我就正在烘烤。
这是正确的。但是如果你把前件和后件互换一下，就会得到这样的结果：
- 如果我在烘焙，那么我就是做面包。
现在这显然是错误的；也许你可以去烤蛋糕！
最后，在逻辑中处理蕴涵时，我们并不关心因果关系。也就是说，当我们说一件事暗示另一件事时，前因和后果之间不必有任何关系。比如，考虑这个句子
- 如果埃及人建造了金字塔，那么胡萝卜就是橙色的。
在英语中，这毫无意义，因为埃及金字塔与胡萝卜的颜色毫无关系。但从逻辑上讲，我们并不关心这些关系。
现在，我们有了一种方法，可以将简单的陈述（命题原子）组合成公式，用逻辑连接词来描述这个世界更有趣的事情。
主要思想总结：
- 因为我们只关心逻辑结构而不是具体含义，所以我们用单个字母来表示无法进一步分解的简单句子（命题原子）。
- 有一组四个联结词，我们可以用来将命题原子组合成逻辑公式。
- 连接词有一个应用顺序。
- 这使我们能够明确地将有关世界的陈述编码为可以严格论证的形式。
更多点击标题见原文。