希尔伯特系统 - 自动证明

Question

我试图证明以下陈述 ~(a->~b) => a 希尔伯特风格系统。不幸的是，似乎不可能提出一个通用算法来找到证明，但我正在寻找一种强力类型的策略。欢迎任何有关如何解决此问题的想法。

Answer 1

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

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

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

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

Ø (α ⊃ Øβ)   ⊢   α

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

---

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

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

---

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

---

---

附录

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

希尔伯特系统

• Verum ex quolibet_α,β 被假定为公理方案，陈述句子 α ⊃ β ⊃ α 预计是可推导的，可为任何子句 α,β
• < strong>链式法则_α,β,γ被假设为一个公理方案，指出句子 (α ⊃ β ⊃ γ) ⊃ (α ⊃ β) ⊃ α ⊃ γ 预计是可推导的，可实例化任何子句 α,β
• Modus ponens< /strong> 被假设为推理规则：假设 α ⊃ β 是可推导的，并且 α 也是可推导的，那么我们期望有理由推断 α ⊃ β 也是可推论的。

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

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

证明演算

• VEQ_α,β :   ⊢   α ⊃ β ⊃ α
• CR_{α,β ,γ}:   ⊢   (α ⊃ β ⊃ γ) ⊃ (α ⊃ β) ⊃ < em>α⊃ γ
• MP：如果⊢   α ⊃ β 和   ⊢   α，那么还有   ⊢   β

树形图表示法：

Axiom 方案 — Verum ex quolibet：

   ––––––––––––––––– [VEQ_α,β ]
        ⊢   α ⊃ β ⊃ α

公理方案 — 链式法则：

   ────────────────────────────────────────────────────────────────── [CR_α,β,γ]
        ⊢   (α ⊃ β ⊃ γ) ⊃ (α ⊃ β) ⊃ < em>α⊃ γ

推理规则 — modus ponens：

     ⊢   α ⊃ β          ⊢   α
   ────────────────────────────────────── [MP]
                ⊢   β

证明树

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

◈ⅩⅩⅩⅩⅩⅩⅩⅩⅩⅩⅤ ⊃α,α⊃α ⊃α ，α]
   
⊃α,α⊃ α]

⊢   [α⊃(α⊃α)⊃α]⊃(α⊃ α⊃α)⊃α⊃α
                 
⊢   α ⊃ (α ⊃ α) ⊃ α

──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────── ──────────── [MP]     ────────────────────── [VEQ_α,α]
                    sp;             
⊢   (α ⊃ α ⊃ α) ⊃ α ⊃ α
                    sp;               
⊢   α ⊃ α ⊃ α

                    sp;             
──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────── ────────[MP]
                    sp;                     sp;                     sp;        
⊢   α ⊃ α

证明公式

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

(CR_{α,α⊃α,α} VEQ_{α,α ⊃ α}) VEQ_{α,< em>α}:   ⊢   α⊃ α

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

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

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

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

示例 1

VEQ_α,β :   ⊢   α ⊃ β ⊃ α

表示用

α 实例化的 Verum ex quolibet 公理方案,β 为以下陈述提供了证明：α ⊃ β ⊃ α 是可推论的。

示例 2

VEQ_α,α： ⊢   α ⊃ α ⊃ α

Verum ex quolibet 公理方案实例化 α,< em>α 为以下陈述提供了证明，即 α ⊃ α ⊃ α 是可推论的。

示例 3

VEQ_α、α⊃α： ⊢   α ⊃ (α ⊃ α) ⊃ α

表示

Verum ex quolibet 公理用 α 实例化的方案，α⊃α 提供了该语句的证明，即 α ⊃ ( α ⊃ α) ⊃ α 是可推导的。

示例 4

CR_α、β、γ： ⊢   (α ⊃ β ⊃ γ) ⊃ (α ⊃ β) ⊃ < em>α⊃ γ

表示

用α、β、<实例化的链式法则公理方案em>γ 为以下陈述提供了证明： (α ⊃ β ⊃ γ) ⊃ (α< /em> ⊃ β) ⊃ α⊃ γ 是可推导的。

例5

CR_{α,α⊃α,α:   ⊢   [α ⊃ (α⊃α) ⊃ α] ⊃ (α ⊃ α⊃α) ⊃ α⊃ α}

表示

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

例6

CR_{α,α⊃α,α VEQα,α ⊃ α:   ⊢   (α ⊃ α⊃α) ⊃ α⊃ α}

意思是

如果我们组合CR_{α,α⊃α,α} 和 VEQ_{α,α ⊃ α} 一起通过 modus ponens ，那么我们就得到了证明以下命题的证明： (α ⊃ α⊃α) ⊃ α< /em>⊃ α 是可推导的。

例7

(CR_{α,α⊃α,α< /sub> VEQα,α ⊃ α) VEQ< /strong>α,α:   ⊢   α⊃ α}

如果我们结合复合证明 (CR_{α,α⊃α,α}) 与 VEQ_{α, α ⊃ α}（通过modus ponens），然后我们得到一个更复杂的证明。这证明了以下命题： α⊃ α 是可推论的。

组合逻辑

虽然上面的这一切确实为预期的定理提供了证明，但是看起来很不直观。不知道人们如何才能“找出”证据。

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

无类型组合逻辑

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

添加类型规则

组合逻辑也有类型变体。语法通过类型进行了增强，甚至除了归约规则之外，还添加了类型规则。

对于基本组合子：

• 选择K_α、β作为基本组合子，居住类型 α → β → α
• 选择S_α,β,γ作为基本组合子，驻留类型(α → β → γ) → (α → β) → < em>α → γ。

应用的打字规则：

• 如果X属于α类型→β且Y属于α类型em>，然后
  X Y 属于 β 类型。

符号和缩写

• K_α,β: α → β< /em> → α
• S_{α,β,γ< /sub>: (α → β → γ) → (α → β >)* → α → γ。}
• 如果X：α→β和Y：α，那么
  X Y：β。

柯里-霍华德对应

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

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

函数式编程

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

外部链接

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

• Wadler, Philip (1989)。 免费定理！ 。

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

• Madore, David (2003)。 Unlambda 编程语言。 Unlambda：你的函数式编程语言噩梦成真。
• 库里、哈斯克尔 B. 和费斯、罗伯特和克雷格·威廉 (1958)。 组合逻辑。 卷。我。阿姆斯特丹：北荷兰出版公司。
• 约翰·特罗普（1999）。 二元 Lambda 演算和组合逻辑。可从作者的 John's Lambda Calculus and Combinatory Logic Playground 下载 PDF 和 Postscript 版本。

Answer 2

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

有关希尔伯特系统的一些常见问题解答：
问：如何知道哪条公理
要使用的模式，以及
进行替换？由于有
无限多种可能性，就是
即使在
原则。 A：没有算法；在
至少不简单。相反，一个人有
要聪明。在纯数学中，
这不被视为一个问题，因为
其中最关心的是
一个证明的存在。然而，在
计算机科学应用，一是
对自动扣除感兴趣
过程，所以这是一个致命的缺陷。这
希尔伯特系统通常不用于
自动定理证明。问：那么，为什么
人们关心希尔伯特吗
系统？答：以肯定前件为原则
单一演绎规则，它提供了
人类如何设计的可口模型
数学证明。正如我们将看到的，
更适合的方法
计算机实现产生证明
不太“像人类”。

Answer 3

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

Ex Falso Quodlibet: E_α : ⊥ → α< br>
奇迹后果： 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]< br>
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)) [链]
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]< br>
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 |- a。

我使用定理证明器 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)))。

我们可以将统一替换和分离的规则合并为 condensed 脱离。在 Prover9 中，我们可以将其表示为：-P

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

“|”表示逻辑或，“-”表示否定。 Prover9 通过反证法证明。该规则用文字表述可以被解释为“要么不是如果 x 则 y 是可证明的情况，或者不是 x 是可证明的情况，或者 y 是可证明的情况”。因此，如果确实成立如果 x,则 y 是可证明的，则第一个析取失败。如果它确实证明 x 是可证明的，则第二个析取失败。因此，如果，如果 x，则 y 可证明，如果 x 可证明，则第三个析取项，即 y 可证明，遵循该规则。

现在我们不能在 NCaNb 中进行替换，因为它不是同义反复。也不是“a”。因此，如果我们输入

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

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

现在我们还可以使用各种定理证明策略“调整”Prover9，例如加权、共振、子公式、选择给定比率、水平饱和（甚至发明我们自己的策略）。我将稍微使用一下提示策略，将所有假设（包括推理规则）和目标都放入提示中。我还将最大权重降低到 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 ==========================