推理规则/经典规则(排中律/反证法双重否定消除)

推理规则/经典规则

推理规则允许我们构建证明
排除规则自上而下分解判断,它们通常用于证明的开始,引入规则自下而上分解判断,它们通常用于证明结束
我们现在可以在后续证明中使用 α → β, β → γ ⊢ α → γ 作为引理或作为派生推理规则
从技术上讲，定理是 ⊢ α 形式的序列，左边没有假设的十字转门符号。演绎定理说我们总能想到Prop中的sequents作为描述定理。
等价陈述和双条件
如果 α ⊢ β 和 β ⊢ α 都成立，我们写α ⊣⊢ β并说α，β是等价的。
这和说的一样⊢ α → β 和 ⊢ β → α都是定理。
我们还有α ⊣⊢ β 当且仅当 ⊢ α ↔ β我们通过以下方式定义双条件箭头 (↔)
α ↔ β = (α → β) ∧ (β → α)
证明很少从头开始。在实践中，我们使用派生规则作为快捷方式和/或信息隐藏。
id : α → α
g : α → β f : β → γ/(f ◦ g) : α → γ
经典规则
许多计算机科学家喜欢建设性命题逻辑
许多数学家更喜欢经典逻辑,这需要额外的推理规则
它打破了引入/排除规则之间的和谐

(lem)：排中律；排中律是说这个命题是真和这个命题是假必居其一,也就是“A是B或者不是B”.比如说“这个矛是最锋利的,可刺穿任何盾,这个盾最坚固,任何矛都刺不破”就不符合排中律.
(pbc)：反证法；
(¬¬E)：双重否定消除。
其中任何一个就足够了——其他的都是可导出的。他们都没有计算内容

经典规则对建构主义者来说是有问题的。
例如，⊢ α ∨ ¬α说每个命题要么是对的要么是错的——没有“中间”选项。
为了证明它，您应该提供 α 的证明或 ¬α 的证明

经典命题逻辑的连接词不再是独立的。
例如，我们可以证明
α ∨ β ⊣⊢ ¬(¬α ∧ ¬β) α → β ⊣⊢ ¬α ∨ β
可以从小子集开始并明确定义其余部分{¬, ∧} {⊥, →} {¬, ∧, ∨}并且定义的连接词的推理规则变得可推导。
稍后我们会看到集合 {¬, ∧, ∨} 对于自动证明搜索很重要

讲义包含一长串经典定理
使用自然演绎证明它们是一种很好的做法
稍后我们还将看到如何使用交互式证明助手来证明其中一些

问题证明将建设性命题逻辑扩展到经典命题逻辑
通过添加 (lem) 或 (pbc) 或 (¬¬E)——在感觉在所有三个扩展中都可以推导出相同的公式。
回答：
第 1 步：首先，我们从 (pbc) 导出 (¬¬E) 和 (lem)。

1. ¬¬α       hyp
2. ¬α       hyp
3. ⊥        ¬E, 1,2
4. α        pbc, 2-31. ¬(α ∨ ¬α)    hyp
2. α            hyp
3. α ∨ ¬α       ∨I 1,2
4. ⊥            ¬E,1,3
5. ¬α           ¬I, 2-4
6. ¬α           hyp
7. α ∨ ¬α       ∨Ir,6
8. ⊥            ¬E,1,7
9. ¬¬α          ¬I, 6-8
10. ⊥           ¬E, 5,9
11. α ∨ ¬α      pbc, 1-10

第 2 步：现在我们从 (¬¬E) 导出 (pbc)。然后我们可以从(pbc) 导出 (lem) - 因此从 (¬¬E) — 与步骤 1 相同。
记住 (pbc) 所说的：如果我们可以从 ¬α 推导出 ⊥，那么我们可以得出 α。
因此，我们确实可以找到一些证明 ⊥ 来自 ¬α。将此引理称为“（*）”。
我们必须证明 α 如下：

1. ¬α        hyp
2. ⊥        (∗), 1
3. ¬¬α      ¬I, 1-2
4. α        ¬¬E, 3

第 3 步：最后从 (lem) 导出 (pbc)，再次使用 (∗)。和以前一样，然后可以导出 (¬¬E) 如第 1 步。

1. α ∨ ¬α        lem
2. α            hyp
3. ¬α           hyp
4. ⊥            (∗)
5. α            ⊥E, 5
6. α            ∨E, 2,3,4-6

推理规则/经典规则(排中律/反证法双重否定消除)相关推荐

【数理逻辑】命题逻辑 ( 等值演算 | 幂等律 | 交换律 | 结合律 | 分配律 | 德摩根律 | 吸收率 | 零律 | 同一律 | 排中律 | 矛盾律 | 双重否定率 | 蕴涵等值式 ... )
文章目录一.等值演算二.等值式三.基本等值式四.基本运算五.等值演算基于上一篇博客 [数理逻辑]命题逻辑 ( 命题与联结词回顾 | 命题公式 | 联结词优先级 | 真值表可满足式矛盾式 ...
【逻辑与计算理论】Lambda 演算的类型与其 Lambda 演算建模
Lambda演算的类型我们已经掌握了直觉逻辑(Intuitionistic Logic,IL), -------------------------------------------------- ...
Pygame实战：风靡全球的经典泡泡龙小游戏来袭，你会喜欢嘛？（附源码）
导语比如:百变的消消乐,还记得嘛?今天就出一个消除类--泡泡龙小游戏,希望你们喜欢哈~! <泡泡乐>是一款适合全年龄玩家的游戏,采用非常经典的"泡泡龙"式的消除泡泡 ...
离散数学知识点总结（6）：自然推理系统；13 个推理规则；如何使用推理规则
文章目录自然推理系统的定义 13个推理规则如何在自然推理系统中构造有效论证的方法直接证明法附加前提证明法(cp规则) 反证法 / 归谬法(Proofs by Contradiciton) 对位 ...
关于声回波对消（回声消除）的一些个人的非严谨粗糙认识
声回波(回声)现象:从听筒里听见自己的声音的一种现象.可以分成声学回声和电路回声,声学回声是指从话筒发出的话音经过房间等通道传播后又被麦克风捕捉传送进通话通道,再被话筒播放出来的声音.声学回声具有时变 ...
文法的左递归性和回溯的消除
文法的左递归性和回溯的消除 1. 文法左递归的消除当一个文法是左递归文法时,采用自上而下分析法会使分析过程进入无穷循环之中.文法左递归是指文法中的某个非终结符 A 存在推导 A ⇒+ Aα ,而自上 ...
数理逻辑学习笔记[0] 命题逻辑：语义
文章目录 1 命题逻辑:语义 1.1 命题和连接符 1.2 真值函数和真值表 1.3 操作和替换规则 1.4 范式 1.5 连接符的完备集 1.6 推理及有效性勘误集 ml-1_1.pdf 1 命题 ...
【数理逻辑】命题逻辑 ( 命题逻辑推理正确性判定 | 形式结构是永真式 - 等值演算 | 从前提推演结论 - 逻辑推理 )
文章目录一. 命题逻辑推理正确性判定二. 形式结构是永真式 ( 等值演算 ) 三. 从前提推演结论 ( 逻辑推理 ) 一. 命题逻辑推理正确性判定命题推理 , 根据前提 , 推理出结论 ; ...
Hinton：我终于想明白大脑怎么工作了！神经学家花三十年，寻找反向传播的生物机制...
作者:Anil Ananthaswamy 编译:梦佳「有一天晚上,我回家吃饭,激动地说『我终于想明白大脑是怎么工作的了!』我15岁的女儿对我说,怎么又来了,老爸.」 ...

推理规则/经典规则(排中律/反证法双重否定消除)

推理规则/经典规则

推理规则/经典规则(排中律/反证法双重否定消除)相关推荐

最新文章

热门文章