math - 希尔伯特系统-自动打样

Question

我正在尝试在Hilbert 风格的系统中证明语句〜（a->〜b）=> a。不幸的是，似乎不可能提出通用算法来找到证明，但是我正在寻找一种蛮力型策略。任何有关如何对此进行攻击的想法都值得欢迎。

Answer 1

如果您喜欢combinatory logic中的“编程”，则


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


Curry-Howard correspondence确保此翻译的可能性。

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

¬（α⊃¬β）αα

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



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


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




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





附录

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

希尔伯特系统


Verum exquolibetα，β被假定为一个公理方案，指出句子α⊃β⊃α可以被推导，并针对任何存在的α，β实例化
链规则α，β，γ被假定为一个公理方案，指出句子（α⊃β⊃γ）⊃（α⊃β）⊃α⊃γ可以推导，并针对任何存在的α，β实例化
推论的模态被假定为推理规则：假设α⊃β是可推导的，并且α也可推导，那么我们期望有理由推断出α⊃β也可推导。


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

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

证明演算


VEQα，β：αα⊃β⊃α
CRα，β，γ：（（α⊃β⊃γ）⊃（α⊃β）⊃α⊃γ
MP：如果αα⊃β和αα，则alsoβ


树形图符号：

公理方案-Verum ex quolibet：


━━━━━━━━━━━━━━━━[VEQα，β]
ααβ⊃α


公理方案-链式规则：


━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━[CRα，β，γ]
α（（α⊃β⊃γ）⊃（α⊃β）⊃α⊃γ


推论规则-方法：


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



证明树

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



━━━━━━━━━━━━━━━━━━━━━━━━━━━━[CRα，α⊃α，α]

━━━━━━━━━━━━━━━[VEQα，α⊃α]

⊃[[α⊃（α⊃α）⊃α]⊃（α⊃α⊃α）⊃α⊃α

ααα⊃（α⊃α）⊃α

━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ ━━━━━━[MP]━━━━━━━━━━━━[VEQα，α]

α（（α⊃α⊃α）⊃α⊃α

ααα⊃α⊃α


━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ ━━━━[MP]

αα⊃α

证明公式

让我们看一下证明的一个简洁的（代数？演算？）表示形式：

（CRα，α⊃α，αVEQα，α⊃α）VEQα，α：⊃⊃α⊃α

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


树的分叉（模式）通过简单的串联（括号）呈现，
树的叶子由相应公理名称的缩写表示。


值得保留有关具体实例的记录，在此使用子索引参数进行排版。

从下面的示例系列中可以看出，我们可以开发证明演算，其中公理被标记为基本的组合子，而惯用法被标记为仅使用其“前提”子证明：

例子1

VEQα，β：αα⊃β⊃α

意味着

用α，β实例化的Verex exquolibet公理方案为以下证明提供了证明：α⊃β⊃α是可推导的。

例子2

VEQα，α：ααα⊃α⊃α

用α，α实例化的Verex exquolibet公理方案为以下证明提供了证明：α⊃α⊃α是可推论的。

例子3

VEQα，α⊃α：αα（α⊃α）⊃α

意味着

以α，α⊃α实例化的Verex exquolibet公理方案为以下证明提供了证明：α⊃（α⊃α）⊃α是可推论的。

例子4

CRα，β，γ：（（α⊃β⊃γ）⊃（α⊃β）⊃α⊃γ

意味着

用α，β，γ实例化的链式规则公理方案提供了以下证明：（α⊃β⊃γ）⊃（α⊃β）⊃α⊃γ。

例子5

CRα，α⊃α，α：⊢[[α⊃（α⊃α）⊃α]⊃（α⊃α⊃α）⊃α⊃α

意味着

用α，α⊃α，α实例化的链规则公理方案提供了以下证明：[α⊃（α⊃α）⊃α]⊃（α⊃α⊃α）⊃α⊃α。

例子6

CRα，α⊃α，αVEQα，α⊃α：α⊃（α⊃α⊃α）⊃α⊃α

意味着

如果我们通过惯性方式将CRα，α⊃α，α和VEQα，α⊃α组合在一起，那么我们得到的证明可以证明以下陈述：（ααα⊃α）⊃α⊃α是可推论的。

例子7

（CRα，α⊃α，αVEQα，α⊃α）VEQα，α：⊃⊃α⊃α

如果我们将comund证明（CRα，α⊃α，α）与VEQα，α⊃α（通过模式）结合在一起，那么我们将获得更加复杂的证明。这证明了以下陈述：α⊃α是可推论的。

组合逻辑

尽管以上所有内容的确为期望定理提供了证明，但似乎非常不直观。人们看不到如何“证明”证据。

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

无类型组合逻辑

Combinatory logic也可以被认为是一种极简的函数式编程语言。尽管极简，它完全是图灵完整的，而且，即使以这种看似混淆的语言，也可以以模块化和可重用的方式编写相当直观和复杂的程序，并且可以从“常规”函数式编程中获得一些实践，并获得一些代数见解， 。

添加打字规则

组合逻辑还具有类型化的变体。语法增加了类型，而且，除了减少规则以外，还增加了键入规则。

对于基本组合器：


选择Kα，β作为基本组合器，inhabiting typeα→β→α
选择Sα，β，γ作为基本组合器，居住类型（α→β→γ）→（α→β）→α→γ。


打字申请规则：


如果X居住于类型α→β，而Y居住于类型α，则
X Y居住在类型β中。


表示法和缩写


Kα，β：α→β→α
Sα，β，γ：（α→β→γ）→（α→β）*→α→γ。
如果X：α→β且Y：α，则
X Y：β。


咖喱霍华德对应

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


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


功能编程

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

外部链接

链接如何将函数式编程中的类型（拉姆达微积分，组合逻辑）转换为逻辑证明和定理：


瓦德勒·菲利普（Wadler，Philip）（1989）。 Theorems for free!。


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


戴维·马多尔（2003）。 The Unlambda Programming Language. Unlambda: Your Functional Programming Language Nightmares Come True。
库里（Hurskell B.＆Feys），罗伯特（Robert）和克雷格（Craig），威廉（1958）。组合逻辑。卷I.阿姆斯特丹：北荷兰出版公司。
约翰·特隆普（1999）。二进制Lambda微积分和组合逻辑。可从作者的John's Lambda Calculus and Combinatory Logic Playground下载PDF和Postscript。