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

Question

我试图在Hilbert风格的系统中证明语句〜(a-> ~b)=> a .不幸的是,似乎不可能想出一个通用算法来找到证据,但我正在寻找一种强力型策略.关于如何攻击这个的任何想法都是受欢迎的.

Answer 1

如果你喜欢组合逻辑中的 "编程" ,那么

• 您可以自动将一些逻辑问题"翻译"到另一个领域:证明组合逻辑术语的平等性.
• 通过良好的函数式编程实践,您可以解决这个问题,
• 然后,您可以将答案转换回原始逻辑问题的希尔伯特风格证明.

Curry-Howard通信确保了这种翻译的可能性.

不幸的是,情况只是对于(命题)逻辑的一个子集而言非常简单:使用条件限制.否定是一个复杂因素,我对此一无所知.因此,我无法回答这个具体问题:

¬(α ⊃¬ β)⊢   α

但是在否定不是问题的一部分的情况下,如果你已经在函数式编程或组合逻辑中练习,那么所提到的自动翻译(和反向翻译)可以是一种帮助.

当然,还有其他一些帮助,我们可以保持在逻辑领域内:

• 在一些更直观的演绎系统中证明问题(例如自然演绎)
• 然后使用提供"编译"可能性的元校正:将自然演绎的"高级"证明翻译成希尔伯特式演绎系统的"机器代码".我的意思是,例如,金属学定理称为" 演绎定理 ".

至于定理证明,据我所知,其中一些的能力得到了扩展,以便他们可以利用互动的人类援助.例如,Coq就是这样.

附录

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

希尔伯特系统

• 八角前quolibet _α,β被假定为公理模式,声称那句话α ⊃ β ⊃ α预计将抵扣,实例化任何subsentences α,β
• 链式法则_α,β,γ 被假定为公理模式,声称那句话(α ⊃ β ⊃ γ)⊃(α ⊃ β)⊃ α ⊃ γ预计将抵扣,实例化任何subsentences α,β
• 肯定前件被假定为推理的规则:只要 α ⊃ β是抵扣,也α是可推论,那么我们预期是合理的推断,也α ⊃ β是推断出来.

让我们证明定理:α ⊃ α是可推论的任何α命题.

让我们介绍以下符号和缩写,开发一个"证明微积分":

证明微积分

• VEQ _α,β:⊢   α ⊃ β ⊃ α
• CR _α,β,γ:⊢(α ⊃ β ⊃ γ)⊃(α ⊃ β)⊃ α ⊃ γ
• MP:如果⊢   α ⊃ β和⊢   α,那么也⊢   β

树图表示法:

公理计划 - Verum ex quolibet:

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

公理方案 - 链规则:

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

推理规则 - 模式推理:

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

证明树

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

━━━━━━━━━━━━━━━━━━━━━━━━━━━━[ CR _{α,α ⊃ α,α} ]━━━━━━━━━━━━ ━━━[ VEQ _{α,α ⊃ α} ]
⊢[ α ⊃(α ⊃ α)⊃ α ]⊃(α ⊃ α ⊃ α)⊃ α ⊃ α                         ⊢   α ⊃(α ⊃ α)⊃ α
━━━━━ ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ ━[ MP ]━━━━━━━━━━━[ VEQ _α,α ]
                                          ⊢(α ⊃ α ⊃ α)⊃ α ⊃ α                                              ⊢   α ⊃ α ⊃ α
                                          ━━━━━━━━━━━ ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━[ MP ]
                                                                                     ⊢   α ⊃ α

证明公式

让我们看一下证明的均匀(代数？微积分？)表示:

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

所以,我们可以用一个公式表示证明树:

• 树的分叉(modus ponens)通过简单的连接(括号)呈现,
• 并且树的叶子由相应公理名称的缩写表示.

值得保留具体实例的记录,'这里使用子索引参数进行排版.

因为它会从一系列下面的例子可以看出,我们可以开发出防结石,其中公理记做排序的基础组合程序,并肯定前件记载为一个单纯的应用程序的"前提" subproofs的:

例1

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

意思是

八角前quolibet与实例化的公理模式α,β提供的声明证明,即α ⊃ β ⊃ α是可推论.

例2

VEQ _α,α:⊢   α ⊃ α ⊃ α

八角前quolibet与实例化的公理模式α,α提供的声明证明,即α ⊃ α ⊃ α 是可推论.

例3

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

意思是

八角前quolibet公理模式实例有α,α ⊃ α提供的声明证明,即α ⊃(α ⊃ α)⊃ α是可推论.

例4

CR _α,β,γ:⊢(α ⊃ β ⊃ γ)⊃(α ⊃ β)⊃ α ⊃ γ

意思是

链规则与实例化公理模式α,β,γ提供的声明证明,即(α ⊃ β ⊃ γ)⊃(α ⊃ β)⊃ α ⊃ γ是推断出来.

例5

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

意思是

链式法则公理模式与实例化的α,α ⊃ α,α提供了证明为语句,即[ α ⊃(α ⊃ α)⊃ α ]⊃(α ⊃ α ⊃ α)⊃ α ⊃ α是可推论.

例6

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

意思是

如果我们结合CR _{α,α ⊃ α,α}和VEQ _{α,α ⊃ α}通过一起假言推理,那么我们得到了证明下面的语句证明:(α ⊃ α ⊃ α)⊃ α ⊃ α是可推论.

例7

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

如果我们结合复方证明(CR _{α,α ⊃ α,α}连同)VEQ _{α,α ⊃ α}(通过肯定前件),那么我们得到一个更复方证明.这证明下面的语句:α ⊃ α是可推论.

组合逻辑

尽管上述所有这些确实为预期定理提供了证据,但似乎非常不直观.无法看出人们如何"找出"证据.

让我们看看另一个领域,在那里研究类似的问题.

没有类型的组合逻辑

组合逻辑也可以被视为极简主义的函数编程语言.尽管它具有极简主义,但它完全是图灵完整的,但即使在这种看似混淆的语言中,也可以用模块化和可重复使用的方式编写非常直观和复杂的程序,从"正常"函数式编程和一些代数见解中获得一些实践, .

添加输入规则

组合逻辑也有类型变体.语法增加了类型,甚至除了缩减规则之外,还添加了类型规则.

对于基本组合器:

• ķ _α,β被选择为基本组合子,栖息型 α →交通β →交通α
• 小号_α,β,γ被选择为基本组合子,居住型(α → β → γ)→(α → β)→ α → γ.

打字申请规则:

• 如果X居住类型α → β并且Y居住类型α,则 X Y居住类型β.

符号和缩写

• ķ _α,β:α →交通β →交通α
• 小号_α,β,γ:(α → β → γ)→(α → β)*→ α → γ.
• 如果X:α → β和Y:α,则 X Y:β.

库里 - 霍华德的通信

可以看出,"模式"在证明微积分和这种类型的组合逻辑中是同构的.

• 所述活性部的前quolibet证明演算的公理对应于ķ组合逻辑的基础组合子
• 证明微积分的链规则公理对应于组合逻辑的S基组合子
• 在肯定前件推理的证明演算规则对应于组合逻辑操作"应用程序".
• 逻辑的"条件"连接词corresponds对应于类型构造函数→类型理论(和类型组合逻辑)

功能编程

但收益是多少？我们为什么要将问题转化为组合逻辑？我个人认为它有时很有用,因为函数式编程是一个具有大量文献并应用于实际问题的东西.人们可以习惯它,当被迫在日常编程任务和实践中使用它时.并且在组合逻辑简化方面可以很好地利用函数式编程实践的一些技巧和提示.如果一个"转移"的实践在组合逻辑中发展,那么它也可以用于在希尔伯特系统中找到证明.

外部链接

链接函数编程中的类型(lambda演算,组合逻辑)如何转换为逻辑证明和定理:

• Wadler,Philip(1989).定理免费!.

链接(或书籍)如何学习直接在组合逻辑中编程的方法和实践:

• 马多雷,大卫(2003年).Unlambda编程语言.Unlambda:你的功能编程语言梦魇成真.
• Curry,Haskell B.&Feys,Robert&Craig,William(1958).组合逻辑.卷.我.阿姆斯特丹:北荷兰出版公司.
• Tromp,John(1999).二元Lambda微积分与组合逻辑.可从作者John's Lambda微积分和组合逻辑游乐场下载PDF和Postscript .

Answer 2

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

关于希尔伯特系统的一些常见问题解答:问:如何知道使用哪个公理图式,以及要进行哪些替换？由于存在无限多种可能性,因此即使在原理上也无法全部尝试.答:没有算法; 至少没有简单的.相反,一个人必须聪明.在纯数学中,这不被视为一个问题,因为人们最担心的是证据的存在.然而,在计算机科学应用中,人们对自动化演绎过程感兴趣,因此这是一个致命的缺陷.希尔伯特系统通常不用于自动定理证明.问:那么,为什么人们关心希尔伯特系统呢？答:以modus ponens作为其单个演绎规则,它提供了人类如何设计数学证明的可爱模型.正如我们将要看到的,更适合计算机实现的方法产生的证据不那么"像人一样".

Answer 3

在希尔伯特微积分中找到证据是非常困难的.

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

Answer 4

您也可以通过设置¬α=α→approach来解决问题.然后我们可以采用Hilbert风格系统,如其中一个答案的附录所示,并通过添加以下两个公理和常数使其成为经典:

实施例FALSO Quodlibet:电子_α:⊥→α
Consequentia紫茉莉:M _α:(¬α→α)→α

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

1. α⊢α(身份)
2. ⊥⊥β→⊥(Ex Falso Quodlibet)
3. α→⊥,α⊢β→⊥(Impl简介左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))))

这给出了以下Hilbert风格的证明:

引理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))[链]
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 [Mirabilis]
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]

相当长的证据!

再见