一、合取规则（∧\wedge∧）
- 1.1 合取引入（∧i\wedge i∧i）
- 1.2 合取消去（∧e\wedge e∧e）
- 1.3 举例说明
二、双重否定规则（¬¬\neg\neg¬¬）
- 2.1 双重否定的消去规则（¬¬e\neg\neg e¬¬e）
- 2.2 双重否定的引入规则（¬¬i\neg\neg i¬¬i）
- 2.3 举例说明
三、蕴涵消去规则
- 3.1 蕴涵消去规则 / 分离规则 / 箭头消去规则（→ e）
- 3.2 反证规则（MT）
- 3.3 举例说明
四、蕴涵引入规则（→ i）
- 4.1 规则说明
- 4.2 定义
- 4.3 举例说明
五、析取规则（∨\vee∨）
- 5.1 “或引入”（∨i\vee i∨i）
- 5.2 “或消去”（∨e\vee e∨e）
- 5.2 举例说明（例1.18有用到复制规则/copy）
六、否定规则（⊥\perp⊥ 矛盾的概念）
- 6.1 规则说明
- 6.2 定义
- 6.3 举例说明

出自黑皮书《面向计算机科学的数理逻辑系统建模与推理》，书名居然比博客名长那么多。感觉推理有点离散数学的影子，但是又完全不一样，头蛮痛的，可能是要长脑子了吧

一、合取规则（∧\wedge∧）

1.1 合取引入（∧i\wedge i∧i）

前提： Φ\PhiΦ 、 Ψ\PsiΨ

结论： Φ∧Ψ\Phi \wedge \PsiΦ∧Ψ

这个规则写为：

ΦΨΦ∧Ψ∧i\frac{\Phi \quad \Psi }{\Phi \wedge \Psi } \wedge iΦ∧ΨΦΨ∧i

说明：横线上是该规则的两个前提，横线下是结论，横线右边是规则名称，∧i\wedge i∧i 读作“合取引入”。

1.2 合取消去（∧e\wedge e∧e）

规则有两个：

Φ∧ΨΦ∧e1\frac{\Phi \wedge \Psi }{\Phi} \wedge e_1ΦΦ∧Ψ∧e1
Φ∧ΨΨ∧e2\frac{\Phi \wedge \Psi }{ \Psi } \wedge e_2ΨΦ∧Ψ∧e2

∧e1\wedge e_1∧e1 表示有了 Φ∧Ψ\Phi \wedge \PsiΦ∧Ψ 的前提，可以得到 Φ\PhiΦ 的一个证明。

∧e2\wedge e_2∧e2 表示有了 Φ∧Ψ\Phi \wedge \PsiΦ∧Ψ 的前提，可以得到 Ψ\PsiΨ 的一个证明。

注意：∧e1\wedge e_1∧e1 结论中 Φ\PhiΦ 必须匹配前提的第一个合取项，与第二个合取项不相关。∧e2\wedge e_2∧e2 以此类推。 Φ\PhiΦ 可以是任意公式。

1.3 举例说明

二、双重否定规则（¬¬\neg\neg¬¬）

其实直观来看 Φ\PhiΦ 和 ¬¬Φ\neg\neg\Phi¬¬Φ 没有差别。比如“今天不下雨不是真的”和“今天下雨”，只不过前者说法体现得让人感觉更加精心设计。

2.1 双重否定的消去规则（¬¬e\neg\neg e¬¬e）

¬¬ΦΦ¬¬e\frac{\neg \neg \Phi }{\Phi} \neg\neg eΦ¬¬Φ¬¬e

2.2 双重否定的引入规则（¬¬i\neg\neg i¬¬i）

Φ¬¬Φ¬¬i\frac{\Phi }{\neg\neg\Phi} \neg\neg i¬¬ΦΦ¬¬i

2.3 举例说明

三、蕴涵消去规则

3.1 蕴涵消去规则 / 分离规则 / 箭头消去规则（→ e）

ΦΦ→ΨΨ→e\frac{\Phi \quad \Phi \to \Psi }{\Psi} \to eΨΦΦ→Ψ→e

简单说明一下，比如：

p：下过雨了
p→q：如果下过雨了，那么街道是湿的。

则 q 代表“街道是湿的”。现在我们已知“下过雨了”（p），而且知道“下过雨的街道是湿的”（p→q），则结合这两条已知信息（前提），就可以推出“街道是湿的”这个结论（q）。

注意：

3.2 反证规则（MT）

像规则 →e，这个规则消去一个蕴涵。假定有 p→q 和 ¬q，那么若p成立，可以应用 →e 得到 q 成立。于是就会有 q 和 ¬q成立，这是不可能的。因此可以推断出 p 必须是假的，而这只能表明 ¬p 是真的。我们将此推理总结为反证规则(MT)：

Φ→Ψ¬Ψ¬ΦMT\frac{\Phi \to \Psi \quad \neg \Psi }{\neg \Phi} MT¬ΦΦ→Ψ¬ΨMT

可以简单用自然语言描述一个例子：

“如果阿强是中国人，那么他是一个亚洲人。阿强不是亚洲人，因此他不是中国人。”

3.3 举例说明

注意：例1.8这里双重否定和MT的次序是不同的，次序是由矢列式的结构所驱动的。

四、蕴涵引入规则（→ i）

4.1 规则说明

MT规则可以证明矢列 p→qp \to qp→q，¬q⊢¬p\neg q\vdash \neg p¬q⊢¬p的有效性，但 p→q⊢¬q→¬pp \to q \vdash \neg q \to \neg pp→q⊢¬q→¬p 也是合理的，可惜没有构建不出现在证明前提中的蕴含的规则。这种矢列的证明可以这样：

类似地举个例子，p 代表程序期望一个整数值输入 x，q 代表该程序返回一个布尔值 y 作为输出。现在，p → q 的有效性相当于一个假设-保证断言：如果输入是整数，那么输出是布尔值。当输入不是整数值时，同一个程序可能计算出一些莫名其妙的东西或直接崩溃了，此时这个断言也是真的。

这种使用规则 → i 证明 p → q 称为类型检测( type checking)。规则格式如下：

Φ⋮ΨΦ→Ψ→i\frac{\begin{matrix} \Phi \\ \vdots \\ \Psi \end{matrix}}{\Phi \to \Psi } \to iΦ→ΨΦ⋮Ψ→i

这个规则表示：为证明 Φ→Ψ\Phi \to \PsiΦ→Ψ，做临时的假定 Ψ\PsiΨ，然后证明 Φ\PhiΦ。在证明 Ψ\PsiΨ 的过程中，可以使用 Φ\PhiΦ和任何其他公式，诸如前提和当前已经得到的临时结论等等。证明可以包括嵌套矩形框，或者在原有的矩形框关闭后又打开新的矩形框。还有一些规则用来说明在证明中的哪些位置可以使用哪些公式。一般来讲，在一个已知位置的证明中，只有在公式 Φ\PhiΦ 先于该位置出现，而且出现的矩形框都没有关闭的情况下，才可以使用该公式。

紧跟在关闭的矩形框后面的行必须与使用该矩形框的规则所得到的结论模式相匹配。就蕴涵引入而言，这意味着，如果一个矩形框的第一个公式是 Φ\PhiΦ，最后一个公式为 Ψ\PsiΨ，那么紧跟在该矩形框后面的行必须是 Φ→Ψ\Phi \to \PsiΦ→Ψ 。我们还会再遇到涉及证明框的两个证明规则，它们也需要类似的模式匹配。

4.2 定义

若逻辑公式 Φ\PhiΦ 具有有效矢列 ⊢Φ\vdash \Phi⊢Φ，则称 Φ\PhiΦ 是定理。

4.3 举例说明

注意：其实例1.11也指出可以将 Φ1,Φ2,⋯,Φn⊢Ψ\Phi _1,\Phi _2,\cdots ,\Phi _n\vdash \PsiΦ1,Φ2,⋯,Φn⊢Ψ 的任何证明变换为定理：

⊢Φ1→(Φ2→(⋯→(Φn→Ψ)⋯)))\vdash \Phi _1\to (\Phi 2\to (\cdots \to (\Phi _n\to \Psi )\cdots )))⊢Φ1→(Φ2→(⋯→(Φn→Ψ)⋯)))
的一个证明：通过规则 →i→i→i 一次应用于 Φn,Φn−1,⋯,Φ1\Phi _n,\Phi _{n-1},\cdots ,\Phi _1Φn,Φn−1,⋯,Φ1，这n行证明加到原有证明中。

五、析取规则（∨\vee∨）

5.1 “或引入”（∨i\vee i∨i）

引入远比消去容易。
ΦΦ∨Ψ∨i1\frac{\Phi }{\Phi \vee \Psi } \vee i_1Φ∨ΨΦ∨i1

ΨΦ∨Ψ∨i2\frac{\Psi }{\Phi \vee \Psi } \vee i_2Φ∨ΨΨ∨i2

5.2 “或消去”（∨e\vee e∨e）

怎样在证明中使用公式 Φ∨Ψ\Phi \vee \PsiΦ∨Ψ 呢？我们的原则是把假设分解为基本要素，以便用于推理中的论证，提炼出期望的结论。假设要证明某个命题 χ\chiχ，已知假设 Φ∨Ψ\Phi \vee \PsiΦ∨Ψ。因为不知道 Φ\PhiΦ 和 Ψ\PsiΨ 哪一个为真，必须给出两个单独的证明，再结合成一个论断。

首先，假设 Φ\PhiΦ 是真的，得出 χ\chiχ 的证明。
其次，假设 Ψ\PsiΨ 是真的，同样需要给出 χ\chiχ 的证明。
已知上面两个证明，可以从 Φ∨Ψ\Phi \vee \PsiΦ∨Ψ 为真推出 χ\chiχ 为真（因为上面的分析是全面的）。因此规则 ∨e\vee e∨e 写为：

Φ∨ΨΦΨ⋮⋮χχχ∨e\frac{\Phi \vee \Psi \quad \begin{matrix} \Phi & \Psi \\\vdots & \vdots \\\chi &\chi \end{matrix} }{\chi } \vee e χΦ∨ΨΦ⋮χΨ⋮χ∨e

使用要点：

两种情形的结论（规则中的 χ\chiχ ）实际上是同一公式。
两种情形的推理由 ∨e\vee e∨e 规则结合。
两种情形都不能使用其他情形中的临时假设，除非那些情形的矩形框已被证明。
第上面例子的 6 行规则 ∨e\vee e∨e 的理由包含三点：出现在第 1 行的析取和两种情形的两个矩形框的位置行 2 - 3 以及行 4 - 5）。

5.2 举例说明（例1.18有用到复制规则/copy）

注意：在例1.18中我们使用了复制规则，因为规则 → i 要求在内框中以 p 结束。复制（copy）规则允许我们复制前面出现过的公式，除非这些公式依赖于已经关闭的矩形框的临时假设。尽管有些不完美，但是这个附加的规则值得我们在不只一次使用前提或其他任何“可视”公式的自由性上付出一个小的代价。

六、否定规则（⊥\perp⊥ 矛盾的概念）

6.1 规则说明

上面有谈到双重否定规则（¬¬i\neg\neg i¬¬i和¬¬e\neg\neg e¬¬e），但是没见过单独一个否定的情况。因为这些规则涉及矛盾概念，论证是关于推理的，必须保持真值，所以存在兜圈子证明（即已知 Φ\PhiΦ 不能直接推出 ¬Φ\neg \Phi¬Φ）。

下面将得出否定规则公式，请先看 6.2定义解释矛盾概念。

矛盾在逻辑中是非常重要的概念，因为对于我们关心的真值来说，它们都是等价的，即我们能证明：

¬(r∨s→q)∧(r∨s→q)⊣⊢(p→q)∧¬(p→q)\neg (r\vee s\to q)\wedge (r\vee s\to q) \dashv \vdash (p\to q)\wedge \neg (p\to q)¬(r∨s→q)∧(r∨s→q)⊣⊢(p→q)∧¬(p→q)

因为该式两边都是矛盾。

事实上，矛盾可以推出矛盾，矛盾还能推导出任何公式。举个例子解释一下，比如我们接受论断 p∧¬p⊢qp\wedge \neg p\vdash qp∧¬p⊢q，其中：

p：阿强爱上了阿珍
q：月球上没有蟑螂

虽然看上去很好笑，月球上有没有蟑螂和阿强是否爱上阿珍没有关系，但是自然演绎就是有这种性质，即矛盾能推导出任何公式。因此上述论断是有效的。因为如果前提都是矛盾的，那么从这个矛盾出发， ⊢\vdash⊢ 可以得出任何我们想要的结论。⊢\vdash⊢ 可以与后面正式解释的基于语义直觉的真值表相匹配：如果所有前提计算都是“真”，那么结论也必须计算为“真”。而且这不是前提之一（总）是假的情形的一个约束。

最后，由底-消去（bottom-elimination）证明规则，⊥\bot⊥ （矛盾）可以证明论证中的任何编码公式：
⊥Φ⊥e\frac{\bot }{\Phi } \bot e Φ⊥⊥e

⊥\bot⊥本身表示由非-消去（not-elimination）证明规则编码的一个矛盾：
Φ¬Φ⊥¬e\frac{\Phi \quad \neg \Phi }{\bot } \neg e ⊥Φ¬Φ¬e

6.2 定义

矛盾是形如 Φ∧¬Φ\Phi \wedge \neg \PhiΦ∧¬Φ 或 ¬Φ∧Φ\neg \Phi \wedge \Phi¬Φ∧Φ 的表达式，其中 Φ\PhiΦ 是任意公式。

公式 ⊥\perp⊥ 代表矛盾。

6.3 举例说明

数理逻辑 | 自然演绎规则整理相关推荐

解读 V8 GC Log（二）: 堆内外内存的划分与 GC 算法
原作者:洗影上一篇文章介绍了理解 V8 GC Log 的意义在哪,简单介绍了一下 V8 GC 的整体特征.在这篇文章里,我们介绍 V8 中堆内存的划分与新老生代的 GC 算法.这些基础知识是理解 V ...
Glibc：浅谈 malloc() 函数具体实现
简介源代码 __libc_malloc() _int_malloc() __libc_malloc() 分析参数 __malloc_hook 全局钩子 ptmalloc_init 转入 _int_ ...
[week9]东东学打牌
文章目录题意 Input Output 输入样例输出样例提示分析总结代码题意最近,东东沉迷于打牌.所以他找到 HRZ.ZJM 等人和他一起打牌.由于人数众多,东东稍微修改了亿下游戏规则 ...
android物品管理,用 Tasker 与 NFC 实现物品管理
和大多数人一样,找东西是我经常遇到的麻烦事:堆叠成山的文档,乱七八糟的维修工具等等,花在管理查找物品上的时间颇为可观. 东西多自然得整理,有的人会按照分类将不同的东西放到不同的收纳箱里,但不是所有物品 ...
Android开发了解这些自然无惧面试，重难点整理
前言咱们这行似乎每个人都有个常识:程序员做到35岁之后,职业道路就很窄了,但我不信这个邪,我今年37岁,依然活跃在开发一线,并且做到了月入四万+. 偶尔也有人问,你是怎么打破35岁定律的?对于这个问 ...
C语言数理逻辑题目,数学逻辑推理题整理，看看你能答对多少
年龄的秘密 A.B.C三人的年龄一直是一个秘密.将A的年龄数字的位置对调一下,就是B的年龄;C的年龄段两倍是A与B两个年龄的差数;而B的年龄是C的10倍. 请问:A.B.C三人的年龄各是多少? 失误的 ...
缘起和性空-佛教对自然的看法(转载整理)
佛教对自然的看法,可从缘起与性空两个观念来着眼.缘起之说,认为世间的一切都是依于种种的条件.因素而生灭,佛教称此关连性为为因缘.依据因缘说,一切都是无自性.无常性与无法性的.不论从身.心及法来说,一切 ...
【地理】从物理到地理之自然地理提纲整理2——大气圈
==大气圈== 然后顺着地球的圈层结构从外到内以此分析,首先是大气圈.通过对大气圈的研究,我们可以知道大气在地球上的主要运动,进而可以在综合其他知识下分析出区域的天气.气候成因. ·大气圈的基本结构: ...
绿幕抠图/蓝幕布抠图自然背景抠图 Robust Video Matting 内容整理
一.RobustVideoMatting 这个大神算法的一作是由林山川在字节跳动实习期间完成的,他以一作身份发表论文<Real-Time High-Resolution Background M ...
计算机软件理论基础集合论,从数理逻辑观点看计算机专业的理论基础探讨
从数理逻辑观点看计算机专业的理论基础探讨从数理逻辑观点看计算机专业的理论基础探讨计从数理逻辑观点看计算机专业的理论基础探讨算机科学与技术学科包括计算机系统结构.计算机软件与理论.计算机应从数理逻辑观 ...

数理逻辑 | 自然演绎规则整理

目录