一阶逻辑的自然推理系统

一阶逻辑的一种形式系统。自然推理系统与一阶逻辑的公理系统的不同之处是，在自然推理系统中没有公理，代替公理的是一组推演规则。自然推理系统的主要特征是，其中的推演规则较之公理系统中用公理和定理来表示演绎推理规律更接近于一般的数学思维。因之，它被称为自然推理系统。自然推理系统在20世纪30年代首次由G．根岑和其它逻辑学家建立，后来又经发展和变化。下面介绍一个与一阶逻辑形式系统F(参见一阶逻辑)相对应的自然推理系统F，F的语言和F相同。在F的规则中，A，B是任意公式，α表示任意个体变元，大写希腊字母Γ，△表示公式集合，语法符号┝F表示前提和结论之间的推理关系，┝F左边的公式(公式集合)是前提，右边的公式是结论。但是，在不引起混淆的情况下，┝简记为┝。F的推演规则有以下15条：

(∈)A，…，A┝A(i=1，…，n)。

(τ)如果Γ┝△，△┝A(△不空)，则Γ┝A。

()如果Γ，A┝B，B，则Γ┝A

(∧)A∧B┝A；A∧B┝B。

(∧)A，B┝A∧B。

(∨)如果Γ，A┝C；Γ，B┝C，则Γ，A∨B┝C。

(∨)A┝A∨B；B┝A∨B。

(→)A→B，A┝B。

(→)如果Γ，A┝B，则Γ┝A→ B。

()AB，A┝B；AB，B┝A。

()如果Γ，A┝B；Γ，B┝A，则Γ┝AB。

()xA(x)┝A(α)。

()如果Γ┝A(α)，α不在Γ中的公式中自由出现，则Γ┝xA(x)。

()如果A(α)┝B，α不在B中出现，则xA(x)┝B。

()A(α)┝xA(x)，其中的A(x)是由A(α)把其中α的某些出现替换为x而得。

规则(∈)称为肯定前提律，凡前提中的公式都可从给定的前提推出。规则(τ)称为演绎推理传递律，表示推理关系是传递的，即从前提Γ可以推出一些结论△，从△又可推出A，则从Γ可推出A。其它13条规则是关于联结词和量词的规则。规则名称中的记号“－”表示消去，如规则(∧－)表示在结论中消去∧；记号“+”表示引入，如规则(∧)表示在结论中引入∧。这13条推演规则可以分成两类，一类直接表示前提和结论之间的推理关系，如规则(→)表示从前提A→B和A可推出结论B。这一类规则称为第一类规则。另一类规则不是直接表示前提和结论之间的推理关系，而是说如果某个推理关系成立，则另一推理关系成立，如规则(→)表示，如果推理关系Γ，A┝B成立，则Γ┝A→B也成立。这后一类规则称为第二类规则。

由F的推演规则可以生成F中的新的推理关系，如可以生成：A┝A；x(A(x)→B(x))┝xA(x)→xB(x)，等等。下面以A┝A为例，说明它怎样由推演规则生成：

其中(1)，(2)由规则(∈)生成，(3)由(1)(2)应用规则()生成。

Γ┝A是F中的推理关系，当且仅当，它能由F的推演规则生成，即它能由F一个第一类规则直接生成，或者能由已生成的推理关系经应用某个第二类规则而得。

在F中生成Γ┝A的过程中，得到一系列推理关系：Γ┝A，…，Γ┝A。其中每一个Γ┝A(i=1，…，n)或者是由第一类推演规则直接生成，或者是由在它们前面的已生成的某些推理关系经应用第二类推演规则而得，并且Γ就是Γ，A就是A。序列Γ┝A，…，Γ┝A称为F中的证明，并称它是关于Γ┝A的一个证明。

┝A表示公式A在F中不用前提可以推出。例如，从上面例子中的(3)A┝A，应用规则(→)就得┝A→A，表示公式A→A在F中不用前提可推出，也说A→ A在F中可证明。

关于自然推理系统F，有如下的结果：如果公式A是常真的，即A，则有┝A；反之，如果┝A。则A。也就是说，系统F具有完全性和可靠性。系统F也是协调的，即不存在一个公式A，使得┝A，A。

自然推理系统F与一阶逻辑的公理系统F，在下述意义上是等价的：凡是F中的可证公式A，即在F中有┝A，则┝A；反之亦然。