1

在Propositions as Types中，它是这样写的：

1935 年，年仅 25 岁的根岑 15 引入了两种新的逻辑公式——自然演绎法和连续微积分——这两种方法被确立为制定逻辑的两个主要系统，并且一直保持到今天。他展示了如何规范化证明以确保它们不会“迂回”，从而产生希尔伯特系统一致性的新证明。而且，最重要的是，为了匹配 Peano 引入的存在量化符号 ∃ 的使用，Gentzen 引入了符号 ∀ 来表示全称量化。他将蕴涵写为 A ⊃ B（如果 A 成立，则 B 成立），合取为 A & B（A 和 B 都成立），析取为 A ∨ B（至少 A 或 B 中的一个成立）。

什么是迂回证明？你能举个简单的例子吗？为什么会出现问题？

4

1 回答 1

2

让我们以连词为例：A ∧ B.

如果我们知道A和B，我们可以推断A ∧ B：

 A   B
------- I
 A ∧ B

这称为引入规则。

对偶，如果我们知道A ∧ B我们可以推断A, 或B:

 A ∧ B          A ∧ B
------- E1     ------- E2
   A              B

这些是淘汰规则。

然后，如果我们知道A我们可以证明 A首先使用引入规则进行推导A ∧ A，然后使用排除规则将其分解为A（和另一个A）：

 A   A
------- I
 A ∧ A
-------- E1
   A

而这种迂回可以出现在较大的样张中。

没有理由进行这次往返：我们在开始的地方结束了！

后续演算“禁止”排除规则之后的引入规则。Gentzen 的结果表明，具有此属性的逻辑与允许引入规则之后的消除规则的逻辑一样强。如今这很重要，因为证明的空间要小得多：首先我们消除（尽可能/需要尽可能小的公式），然后我们引入（建立目标）。这实际上很有用，例如，对于自动证明搜索或程序合成。

编辑这个答案的第一个版本有证据证明A ∧ B：

 A ∧ B         A ∧ B
------- E1    ------- E2
   A             B
  ----------------- I
         A ∧ B

然而，除了直接证明：

A ∧ B

-------- ID A ∧ B

它似乎是唯一的其他“简单证明”。在 Haskell 语法中，人们会这样写：

proof :: (a, b) -> (a, b)
proof (x, y) = (x, y)
-- or
proof x = x
proof = id

哪些是相同的（除了严格属性，逻辑不感兴趣），并且是唯一合理的定义。例如：

proof :: (a, b) -> (a, b)
proof x = fst (x, x)

也是有效的，不再聪明了。

于 2016-01-22T11:50:08.513 回答