math - 希尔伯特系统 - 自动证明

Question

我试图证明 ~(a->~b) => a 在希尔伯特风格系统中的陈述。不幸的是，似乎不可能想出一个通用的算法来找到一个证明，但我正在寻找一种蛮力类型的策略。欢迎任何关于如何攻击它的想法。

Answer 1

如果您喜欢组合逻辑中的“编程” ，那么

• 您可以自动将一些逻辑问题“翻译”到另一个领域：证明组合逻辑项的相等性。
• 通过良好的函数式编程实践，您可以解决这个问题，
• 之后，您可以将答案翻译回您的原始逻辑问题的希尔伯特式证明。

库里-霍华德通信确保了这种翻译的可能性。

不幸的是，仅对于（命题）逻辑的一个子集来说，情况是如此简单：使用条件限制。否定是一个并发症，我对此一无所知。因此，我无法回答这个具体问题：

¬ ( α ⊃ ¬ β ) ⊢   α

但是在否定不是问题的一部分的情况下，如果您已经练习过函数式编程或组合逻辑，那么提到的自动翻译（和反向翻译）可能会有所帮助。

---

当然，还有其他帮助，我们可以留在逻辑领域：

• 在一些更直观的演绎系统中证明问题（例如自然演绎）
• 然后使用提供“编译器”可能性的元定理：将自然演绎的“高级”证明转换为希尔伯特式演绎系统的“机器代码”。我的意思是，例如，称为“演绎定理”的元逻辑定理。

---

至于定理证明器，据我所知，其中一些的能力得到了扩展，以便它们可以利用交互式人工协助。例如Coq就是这样。

---

---

附录

让我们看一个例子。如何证明α ⊃ α？

希尔伯特系统

• Verum ex quolibet _{α , β}被假定为一个公理方案，说明句子α ⊃ β ⊃ α预期是可演绎的，对任何子句α , β进行实例化
• 链式法则_{α , β , γ} 被假定为一个公理方案，说明句子 ( α ⊃ β ⊃ γ ) ⊃ ( α ⊃ β ) ⊃ α ⊃ γ预期是可推导的，对任何子句α , β进行实例化
• 假定后件推理规则：假设 α ⊃ β是可演绎的，并且α也是可演绎的，那么我们期望有理由推断出α ⊃ β也是可演绎的。

让我们证明定理：对于任何α命题， α ⊃ α是可推导的。

让我们介绍以下符号和缩写，开发“证明演算”：

证明演算

• VEQ _{α , β} : ⊢   α ⊃ β ⊃ α
• 铬_{α , β , γ} : ⊢ ( α ⊃ β ⊃ γ ) ⊃ ( α ⊃ β ) ⊃ α ⊃ γ
• MP : 如果 ⊢   α ⊃ β和 ⊢   α , 那么还有 ⊢   β

树形图表示法：

公理方案——Verum ex quolibet：

    ━━━━━━━━━━━━━━━━[ VEQ _{α , β} ]
          ⊢   α ⊃ β ⊃ α

公理方案——链式法则：

    ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━[ CR _{α , β , γ} ]
          ⊢ ( α ⊃ β ⊃ γ ) ⊃ ( α ⊃ β ) ⊃ α ⊃ γ

推论规则 - 作案方式：

     ⊢   α ⊃ β           ⊢   α
    ━━━━━━━━━━━━━━━━━━━[ MP ]
                     ⊢   β

证明树

让我们看一下证明的树形图表示：

━━━━━━━━━━━━━━━━━━━━━━━━━━[ CR _{α , α ⊃<em>α, α} ] ━━━━━━━━━━ ━━━━━━ [ VEQ α _{, α ⊃ <em>α} ]
⊢ [ α ⊃( α ⊃<em>α)⊃<em>α]⊃( α ⊃<em>α⊃<em>α )⊃<em>α⊃<em>α ⊢   α ⊃ ( α ⊃ α ) ⊃ α
━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ ━━━━━━━━━━━━━━━━━━━━━━━━━[ MP ] ━━━━━━━━━━ [ VEQ _{α , α} ]
                                          ⊢ ( α ⊃ α? _ _ _ _ _                                              _   _ _ _ _ _
                                          _ ━━━━━━━━━━━━━━━━━[ MP ]
                                                                                     ⊢   α ⊃ α

证明公式

让我们看一个更简洁（代数？微积分？）证明的表示：

( CR _{α , α ⊃<em>α, α} VEQ _{α , α ⊃ α} ) VEQ _{α , α} : ⊢   α ⊃ α

所以，我们可以用一个公式来表示证明树：

• 树的分叉（modus ponens）通过简单的连接（括号）呈现，
• 并且树的叶子由相应的公理名称的缩写呈现。

值得记录一下具体的实例化，这里用子索引参数排版。

从下面的一系列示例中可以看出，我们可以开发一个证明演算，其中公理被表示为某种基本组合子，而前件式被表示为仅仅是其“前提”子证明的应用：

示例 1

VEQ _{α , β} : ⊢   α ⊃ β ⊃ α

意思是

用α , β实例化的Verum ex quolibet公理方案为陈述提供了证明，即α ⊃ β ⊃ α是可推导出的。

示例 2

VEQ _{α , α} : ⊢   α ⊃ α ⊃ α

用α实例化的Verum ex quolibet公理方案，α为陈述提供了证明，即α ⊃ α ⊃ α 是可推导出的。

示例 3

VEQ _{α , α ⊃<em>α} : ⊢   α ⊃ ( α ⊃ α ) ⊃ α

意思是

用α实例化的Verum ex quolibet公理方案，α ⊃<em>α 为该陈述提供了证明，即α ⊃ ( α ⊃ α ) ⊃ α是可推导出的。

示例 4

铬_{α , β , γ} : ⊢ ( α ⊃ β ⊃ γ ) ⊃ ( α ⊃ β ) ⊃ α ⊃ γ

意思是

用α , β , γ实例化的链式法则公理方案提供了一个证明，即 ( α ⊃ β ⊃ γ ) ⊃ ( α ⊃ β ) ⊃ α ⊃ γ是可推导的。

示例 5

CR _{α , α ⊃<em>α, α} : ⊢ [ α ⊃ ( α ⊃<em>α) ⊃ α ] ⊃ ( α ⊃ α ⊃<em>α) ⊃ α ⊃ α

意思是

用α , α ⊃<em>α, α实例化的链式法则公理方案为以下陈述提供了证明，即 [ α ⊃ ( α ⊃<em>α) ⊃ α ] ⊃ ( α ⊃ α ⊃<em>α) ⊃ α ⊃ α是可推导的。

例 6

CR _{α , α ⊃<em>α, α} VEQ _{α , α ⊃ α} : ⊢ ( α ⊃ α ⊃<em>α) ⊃ α ⊃ α

意思是

如果我们将CR _{α , α ⊃<em>α, α}和VEQ _{α , α ⊃ α}通过modus ponens组合在一起，那么我们得到证明以下陈述的证明： ( α ⊃ α ⊃<em>α) ⊃ α ⊃ α是可推导的。

例 7

( CR _{α , α ⊃<em>α, α} VEQ _{α , α ⊃ α} ) VEQ _{α , α} : ⊢   α ⊃ α

如果我们将复合证明 ( CR _{α , α ⊃<em>α, α} ) 与VEQ _{α , α ⊃ α} (通过modus ponens ) 结合起来，那么我们会得到一个更加复合的证明。这证明了以下陈述：α ⊃ α是可推导出的。

组合逻辑

虽然以上这一切确实为预期定理提供了证明，但似乎很不直观。看不到人们如何“找出”证据。

让我们看看另一个研究类似问题的领域。

无类型组合逻辑

组合逻辑也可以看作是一种极简的函数式编程语言。尽管它是极简主义，但它完全是图灵完备的，但更重要的是，即使使用这种看似模糊的语言，以模块化和可重用的方式，从“正常”函数式编程和一些代数见解中获得一些实践，也可以编写非常直观和复杂的程序， .

添加打字规则

组合逻辑也有类型化的变体。语法增加了类型，而且，除了减少规则之外，还添加了类型规则。

对于基础组合器：

• K _{α , β}被选为基本组合子，包含类型 α → β → α
• S _{α , β , γ}被选为基本组合子，居住型 ( α → β → γ ) → ( α → β ) → α → γ。

打字应用规则：

• 如果X属于α → β型，Y属于α型，那么 X Y属于β型。

符号和缩写

• K _{α , β} : α → β → α
• S _{α , β , γ} : ( α → β → γ ) → ( α → β )* → α → γ。
• 如果X : α → β和Y : α，则 X Y : β。

库里-霍华德对应

可以看出，“模式”在证明演算和这种类型化的组合逻辑中是同构的。

• 证明演算的Verum ex quolibet公理对应于组合逻辑的K基组合子
• 证明演算的链式法则公理对应于组合逻辑的S基组合子
• 证明演算中的推理方式规则对应于组合逻辑中的“应用”操作。
• 逻辑的“条件”连接词⊃对应于类型论的类型构造器→（和类型化组合逻辑）

函数式编程

但是有什么收获呢？为什么我们要将问题转化为组合逻辑？我个人觉得它有时很有用，因为函数式编程是一门拥有大量文献并应用于实际问题的东西。人们可以习惯它，当被迫在日常编程任务和实践中使用它时。在组合逻辑约简中可以很好地利用函数式编程实践的一些技巧和提示。如果在组合逻辑中发展了“转移”实践，那么它也可以用于在希尔伯特系统中寻找证明。

外部链接

链接函数式编程（lambda 演算、组合逻辑）中的类型如何转化为逻辑证明和定理：

• 菲利普·瓦德勒 (1989)。免费定理！.

链接（或书籍）如何学习方法和实践直接在组合逻辑中编程：

• 大卫·马多雷 (2003)。Unlambda 编程语言。Unlambda：你的函数式编程语言噩梦成真。
• Curry, Haskell B. & Feys, Robert & Craig, William (1958)。组合逻辑。卷。我。阿姆斯特丹：北荷兰出版公司。
• 约翰·特罗普 (1999)。二进制 Lambda 微积分和组合逻辑。可从作者的John's Lambda Calculus and Combinatory Logic Playground下载 PDF 和 Postscript 。

Answer 2

希尔伯特系统通常不用于自动定理证明。使用自然演绎编写计算机程序来做证明要容易得多。来自CS 课程的材料：

关于希尔伯特系统的一些常见问题解答： 问：如何知道要使用哪个公理模式，以及要进行哪些替换？因为有无限多的可能性，所以不可能全部尝试，即使在原则上也是如此。A：没有算法；至少没有一个简单的。相反，一个人必须聪明。在纯数学中，这不被视为一个问题，因为人们最关心的是证明的存在。然而，在计算机科学应用中，人们对自动推理过程感兴趣，所以这是一个致命的缺陷。希尔伯特系统通常不用于自动定理证明。问：那么，为什么人们关心希尔伯特系统？A: 以先决条件作为其唯一的演绎规则，它为人类如何设计数学证明提供了一个可口的模型。正如我们将看到，

Answer 3

你也可以通过设置 ¬ α = α → ⊥ 来解决这个问题。然后我们可以采用其中一个答案的附录中所示的希尔伯特风格系统，并通过分别添加以下两个公理常数使其成为经典：

Ex Falso Quodlibet: E _α : ⊥ → α
Consequentia Mirabilis: M _α : (¬ α → α) → α

¬ (α → ¬ β) → α 的后续证明如下：

1. α ⊢ α（同一性）
2. ⊥ ⊢ β → ⊥ (Ex Falso Quodlibet)
3. α → ⊥, α ⊢ β → ⊥ (Impl Intro Left 1 & 2)
4. α → ⊥ ⊢ α → (β → ⊥) (Impl Intro Right 3)
5. ⊥ ⊢ α (Ex Falso Quodlibet)
6. (α → (β → ⊥)) → ⊥, α → ⊥ ⊢ α (Impl Intro Left 4 & 5)
7. (α → (β → ⊥)) → ⊥ ⊢ α (Consequentia Mirabilis 6)
8. ⊢ ((α → (β → ⊥)) → ⊥) → α (Impl Intro Right 7)

从这个后续证明中，可以提取一个 lambda 表达式。上述后续证明的一个可能的 lambda 表达式如下所示：

λy.(M λz.(E (y λx.(E (zx)))))

此 lambda 表达式可以转换为 SKI 术语。上述 lambda 表达式的一个可能的 SKI 术语如下所示：

S (KM)) (L2 (L1 (K (L2 (L1 (KI))))))
其中 L1 = (S ((S (KS)) ((S (KK)) I)))
和 L2 = ( S (K (S (KE))))

这给出了以下希尔伯特风格的证明：

引理1：链式法则的弱化形式：
1：（（A→B）→（（C→A）→（C→B）））→（（（A→B）→（C→A））→ ((A → B) → (C → B))) [链]
2: ((A → B) → ((C → (A → B)) → ((C → A) → (C → B)) )) → (((A → B) → (C → (A → B))) → ((A → B) → ((C → A) → (C → B)))) [链]
3: ( (C → (A → B)) → ((C → A) → (C → B))) → ((A → B) → ((C → (A → B)) → ((C → A) → (C → B)))) [Verum Ex]
4: (C → (A → B)) → ((C → A) → (C → B)) [链]
5: (A → B) → (( C → (A → B)) → ((C → A) → (C → B))) [MP 3, 4]
6: ((A → B) → (C → (A → B))) → ( (A → B) → ((C → A) → (C → B))) [MP 2, 5]
7: ((A → B) → ((A → B) → (C → (A → B) ))) → (((A → B) → (A → B)) → ((A → B) → (C → (A → B)))) [链]
8: ((A → B) → ( C → (A → B))) → ((A → B) → ((A → B) → (C → (A → B)))) [Verum Ex]
9: (A → B) → (C → (A → B)) [Verum Ex]
10: (A → B) → ((A → B) → (C → (A → B))) [MP 8, 9]
11: ((A → B) → (A → B)) → ((A → B) → (C → (A → B))) [MP 7, 10]
12: (A → B) → ( A → B) [同一性]
13: (A → B) → (C → (A → B)) [MP 11, 12]
14: (A → B) → ((C → A) → (C → B) ) [MP 6, 13]
15: ((A → B) → (C → A)) → ((A → B) → (C → B)) [MP 1, 14]

引理 2：Ex Falso 的弱化形式：
1: (A → ((B → ⊥) → (B → C))) → ((A → (B → ⊥)) → (A → (B → C)) ) [链]
2: ((B → ⊥) → (B → C)) → (A → ((B → ⊥) → (B → C))) [Verum Ex]
3: (B → (⊥ → C ) )) → ((B → ⊥) → (B → C)) [Chain]
4: (⊥ → C) → (B → (⊥ → C)) [Verum Ex]
5: ⊥ → C [Ex Falso]
6 : B → (⊥ → C) [MP 4, 5]
7: (B → ⊥) → (B → C) [MP 3, 6]
8: A → ((B → ⊥) → (B → C)) [MP 2, 7]
9: (A → (B → ⊥)) → (A → (B → C)) [MP 1, 8]

最终证明：
1：(((A → (B → ⊥)) → ⊥) → (((A → ⊥) → A) → A)) → ((((A → (B → ⊥)) → ⊥) → ((A → ⊥) → A)) → (((A → (B → ⊥)) → ⊥) → A)) [链]
2: (((A → ⊥) → A) → A) → ( ((A → (B → ⊥)) → ⊥) → (((A → ⊥) → A) → A)) [Verum Ex]
3: ((A → ⊥) → A) → A [奇异果]
4： ((A → (B → ⊥)) → ⊥) → (((A → ⊥) → A) → A) [MP 2, 3]
5: (((A → (B → ⊥)) → ⊥) → ((A → ⊥) → A)) → (((A → (B → ⊥)) → ⊥) → A) [MP 1, 4]
6: (((A → (B → ⊥)) → ⊥) → ((A → ⊥) → ⊥)) → (((A → (B → ⊥)) → ⊥) → ((A → ⊥) → A)) [引理 2]
7: (((A → (B → ⊥)) → ⊥) → ((A → ⊥) → (A → (B → ⊥)))) → (((A → (B → ⊥)) → ⊥) → ((A → ⊥) → ⊥ )) [引理1]
8: ((A → ⊥) → (A → (B → ⊥))) → (((A → (B → ⊥)) → ⊥) → ((A → ⊥) → (A → (B → ⊥)))) [Verum Ex]
9: ((A → ⊥) → (A → ⊥)) → ((A → ⊥) → (A → (B → ⊥))) [引理 2]
10: ((A → ⊥) → (A → A )) → ((A → ⊥) → (A → ⊥)) [引理 1]
11: (A → A) → ((A → ⊥) → (A → A)) [Verum Ex]
12: A → A [同一性]
13: (A → ⊥) → (A → A) [MP 11, 12]
14: (A → ⊥) → (A → ⊥) [MP 10, 13]
15: (A → ⊥) → ( A → (B → ⊥)) [MP 9, 14]
16: ((A → (B → ⊥)) → ⊥) → ((A → ⊥) → (A → (B → ⊥))) [MP 8 , 15]
17: ((A → (B → ⊥)) → ⊥) → ((A → ⊥) → ⊥) [MP 7, 16]
18: ((A → (B → ⊥)) → ⊥) → ((A → ⊥) → A) [MP 6, 17]
19: ((A → (B → ⊥)) → ⊥) → A [MP 5, 18]

好长的证明！

再见

Answer 4

在希尔伯特微积分中寻找证明非常困难。

您可以尝试将后续微积分或自然演绎中的证明翻译为希尔伯特微积分。

Answer 5

1. 哪个具体的希尔伯特系统？有吨。
2. 可能最好的方法是在后续微积分中找到一个证明并将其转换为希尔伯特系统。

Answer 6

我使用波兰符号。

由于您引用了维基百科，我们假设我们的基础是

1 CpCqp。

2 CCpCqrCCpqCpr。

3 CCNpNqCqp。

我们想证明

NCaNb |-

我使用定理证明器Prover9。因此，我们需要将所有内容都括起来。此外，Prover9 的变量为 (x, y, z, u, w, v5, v6, ..., vn)。所有其他符号都被解释为函数或关系或谓词。所有公理之前也需要一个谓词符号“P”，我们可以认为它的意思是“可以证明……”或更简单的“可证明”。Prover9 中的所有句子都需要以句号结尾。因此，公理 1、2 和 3 分别变为：

1 P(C(x,C(y,x)))。

2 P(C(C(x,C(y,z)),C(C(x,y),C(x,z))))。

3 P(C(C(N(x),N(y)),C(y,x)))。

我们可以将统一替换规则和分离规则合并到 浓缩 分离规则中。在 Prover9 中，我们可以将其表示为：

-P(C(x,y)) | -P(x) | P(y)。

“|” 表示逻辑析取，“-”表示否定。Prover9 用反证法证明。该规则用文字表达可以解释为“如果 x 则 y 不是可证明的，或者 x 不是可证明的，或者 y 是可证明的”。因此，如果它确实认为如果 x，则 y 是可证明的，则第一个析取失败。如果它确实认为 x 是可证明的，那么第二个析取失败。因此，如果，如果 x，那么 y 是可证明的，如果 x 是可证明的，那么第三个析取，即 y 是可证明的，遵循该规则。

现在我们不能在 NCaNb 中进行替换，因为它不是重言式。“一”也不是。因此，如果我们把

P(N(C(a,N(b))))。

作为一个假设，Prover9 会将“a”和“b”解释为无效函数，从而有效地将它们转换为常数。我们也想让 P(a) 作为我们的目标。

现在我们还可以使用各种定理证明策略来“调整”Prover9，例如加权、共振、子公式、pick-given ratio、电平饱和（甚至是我们自己的）。我将通过将所有假设（包括推理规则）和目标变成提示来稍微使用提示策略。我还将最大权重降低到 40，并将最大变量数设为 5。

我使用带有图形界面的版本，但这是整个输入：

set(ignore_option_dependencies). % GUI handles dependencies

if(Prover9). % Options for Prover9
assign(max_seconds, -1).
assign(max_weight, 40).
end_if.

if(Mace4).   % Options for Mace4
assign(max_seconds, 60).
end_if.

if(Prover9). % Additional input for Prover9
formulas(hints).
-P(C(x,y))|-P(x)|P(y).
P(C(x,C(y,x))).
P(C(C(x,C(y,z)),C(C(x,y),C(x,z)))).
P(C(C(N(x),N(y)),C(y,x))).
P(N(C(a,N(b)))).
P(a).
end_of_list.
assign(max_vars,5).
end_if.

formulas(assumptions).

-P(C(x,y))|-P(x)|P(y).
P(C(x,C(y,x))).
P(C(C(x,C(y,z)),C(C(x,y),C(x,z)))).
P(C(C(N(x),N(y)),C(y,x))).
P(N(C(a,N(b)))).

end_of_list.

formulas(goals).

P(a).

end_of_list.

这是它给我的证据：

============================== prooftrans ============================
Prover9 (32) version Dec-2007, Dec 2007.
Process 1312 was started by Doug on Machina2,
Mon Jun  9 22:35:37 2014
The command was "/cygdrive/c/Program Files (x86)/Prover9-Mace43/bin-win32/prover9".
============================== end of head ===========================

============================== end of input ==========================

============================== PROOF =================================

% -------- Comments from original proof --------
% Proof 1 at 0.01 (+ 0.01) seconds.
% Length of proof is 23.
% Level of proof is 9.
% Maximum clause weight is 20.
% Given clauses 49.

1 P(a) # label(non_clause) # label(goal).  [goal].
2 -P(C(x,y)) | -P(x) | P(y).  [assumption].
3 P(C(x,C(y,x))).  [assumption].
4 P(C(C(x,C(y,z)),C(C(x,y),C(x,z)))).  [assumption].
5 P(C(C(N(x),N(y)),C(y,x))).  [assumption].
6 P(N(C(a,N(b)))).  [assumption].
7 -P(a).  [deny(1)].
8 P(C(x,C(y,C(z,y)))).  [hyper(2,a,3,a,b,3,a)].
9 P(C(C(C(x,C(y,z)),C(x,y)),C(C(x,C(y,z)),C(x,z)))).  [hyper(2,a,4,a,b,4,a)].
12 P(C(C(C(N(x),N(y)),y),C(C(N(x),N(y)),x))).  [hyper(2,a,4,a,b,5,a)].
13 P(C(x,C(C(N(y),N(z)),C(z,y)))).  [hyper(2,a,3,a,b,5,a)].
14 P(C(x,N(C(a,N(b))))).  [hyper(2,a,3,a,b,6,a)].
23 P(C(C(a,N(b)),x)).  [hyper(2,a,5,a,b,14,a)].
28 P(C(C(x,C(C(y,x),z)),C(x,z))).  [hyper(2,a,9,a,b,8,a)].
30 P(C(x,C(C(a,N(b)),y))).  [hyper(2,a,3,a,b,23,a)].
33 P(C(C(x,C(a,N(b))),C(x,y))).  [hyper(2,a,4,a,b,30,a)].
103 P(C(N(b),x)).  [hyper(2,a,33,a,b,3,a)].
107 P(C(x,b)).  [hyper(2,a,5,a,b,103,a)].
113 P(C(C(N(x),N(b)),x)).  [hyper(2,a,12,a,b,107,a)].
205 P(C(N(x),C(x,y))).  [hyper(2,a,28,a,b,13,a)].
209 P(C(N(a),x)).  [hyper(2,a,33,a,b,205,a)].
213 P(a).  [hyper(2,a,113,a,b,209,a)].
214 $F.  [resolve(213,a,7,a)].

============================== end of proof ==========================