推理规则/经典规则
推理规则允许我们构建证明
排除规则自上而下分解判断,它们通常用于证明的开始,引入规则自下而上分解判断,它们通常用于证明结束
我们现在可以在后续证明中使用 α → β, β → γ ⊢ α → γ 作为引理或作为派生推理规则
从技术上讲，定理是 ⊢ α 形式的序列，左边没有假设的十字转门符号。 演绎定理说我们总能想到Prop中的sequents作为描述定理。
等价陈述和双条件
如果 α ⊢ β 和 β ⊢ α 都成立，我们写α ⊣⊢ β并说α，β是等价的。
这和说的一样⊢ α → β 和 ⊢ β → α都是定理。
我们还有α ⊣⊢ β 当且仅当 ⊢ α ↔ β我们通过以下方式定义双条件箭头 (↔)
α ↔ β = (α → β) ∧ (β → α)
证明很少从头开始。 在实践中，我们使用派生规则作为快捷方式和/或信息隐藏。
id : α → α
g : α → β f : β → γ/(f ◦ g) : α → γ
经典规则
许多计算机科学家喜欢建设性命题逻辑
许多数学家更喜欢经典逻辑,这需要额外的推理规则
它打破了引入/排除规则之间的和谐
(lem)：排中律；排中律是说这个命题是真和这个命题是假必居其一,也就是“A是B或者不是B”.比如说“这个矛是最锋利的,可刺穿任何盾,这个盾最坚固,任何矛都刺不破”就不符合排中律. (pbc)：反证法； (¬¬E)：双重否定消除
其中任何一个就足够了——其他的都是可导出的。 他们都没有计算内容
经典规则对建构主义者来说是有问题的。
例如，⊢ α ∨ ¬α说每个命题要么是对的要么是错的——没有“中间”选项。
为了证明它，您应该提供 α 的证明或 ¬α 的证明
经典命题逻辑的连接词不再是独立的。
例如，我们可以证明
α ∨ β ⊣⊢ ¬(¬α ∧ ¬β) α → β ⊣⊢ ¬α ∨ β
可以从小子集开始并明确定义其余部分{¬, ∧} {⊥, →} {¬, ∧, ∨}并且定义的连接词的推理规则变得可推导。
稍后我们会看到集合 {¬, ∧, ∨} 对于自动证明搜索很重要
讲义包含一长串经典定理
使用自然演绎证明它们是一种很好的做法
稍后我们还将看到如何使用交互式证明助手来证明其中一些
问题 证明将建设性命题逻辑扩展到经典命题逻辑 通过添加 (lem) 或 (pbc) 或 (¬¬E)——在感觉在所有三个扩展中都可以推导出相同的公式。
回答：
第 1 步：首先，我们从 (pbc) 导出 (¬¬E) 和 (lem)。
1. ¬¬α hyp2. ¬α hyp3. ⊥ ¬E, 1,24. α pbc, 2-31. ¬(α ∨ ¬α) hyp2. α hyp3. α ∨ ¬α ∨I 1,24. ⊥ ¬E,1,35. ¬α ¬I, 2-46. ¬α hyp7. α ∨ ¬α ∨Ir,68. ⊥ ¬E,1,79. ¬¬α ¬I, 6-810. ⊥ ¬E, 5,911. α ∨ ¬α pbc, 1-10
第 2 步：现在我们从 (¬¬E) 导出 (pbc)。 然后我们可以从(pbc) 导出 (lem) - 因此从 (¬¬E) — 与步骤 1 相同。
记住 (pbc) 所说的：如果我们可以从 ¬α 推导出 ⊥，那么我们可以得出 α。
因此，我们确实可以找到一些证明 ⊥ 来自 ¬α。 将此引理称为“（*）”。
我们必须证明 α 如下：
1. ¬α hyp2. ⊥ (∗), 13. ¬¬α ¬I, 1-24. α ¬¬E, 3
第 3 步：最后从 (lem) 导出 (pbc)，再次使用 (∗)。 和以前一样，然后可以导出 (¬¬E) 如第 1 步。
1. α ∨ ¬α lem2. α hyp3. ¬α hyp4. ⊥ (∗)5. α ⊥E, 56. α ∨E, 2,3,4-6
