在第五章中，我们给出了可证公式的定义.（当然，自然推理系统FQC的可证公式的定义和公理系统QC中的可证公式的定义是有区别的）这个定义可以被理解为相应于所给规则的“绝对真理”的概念.在这一节里，我们可以把这个概念作进一步推广，定义“相对真理”的概念，也就是要定义一个公式在某些附加假设（或条件）下成立的概念.实际上，我们只要把第四章第一节中的一些基本概念和事实作一些推广即可.

定义 令Φ是一个任意的公式集，α是一个任意的公式.如果α是某个假设性证明的最后一步得出的公式，而该假设性证明的所有未曾消除的、由Hyp规则所引入的公式都属于Φ，那么称公式α是从公式集Φ可演绎的.简称α是从Φ可演绎的.记作Φα.

当Φ中只有一个公式β时，{β}α就简记成βα，并称α是从β可演绎的.

当Φ∪{β}α时，也可简记为Φ，βα.

从上述定义可知，当Φ=∅时，∅α当且仅当α，即α是从空集可演绎的，当且仅当α是可证的.因此，可以得出结论：可演绎性是可证性的推广.

符号具有下面的一些性质.有些性质从形式上看类似于第四章第一节中0的性质，但是，为了完整起见，我们还是给出每条性质的证明.

性质1 如果公式集Φ⊆Φ′，并且Φα，则Φ′α.

证明 由Φα可知，存在一个假设性证明，它的最后一个公式是α，而其未曾消除的假设都属于Φ；又由Φ⊆Φ′，那么这些未曾消除的假设也都属于Φ′.所以，Φ′α.

给定一个公式集Φ，如果用Th（Φ）表示从Φ可演绎的全体公式的集合.从可演绎定义得，{α：α}=Th（∅），即Th（∅）等于由全体可证公式组成的公式集.由性质1可得：Th（∅）⊆Th（Φ）.这说明，所有逻辑定理是任一理论T=Φ的定理.换句话说，一个理论T=Φ的定理集中包含所有逻辑的（或系统的内）定理.

性质2 如果α∈Φ，那么Φα.

证明 下面的仅有一个公式α组成的假设性证明：

就是Φα的一个证明.

性质3 Φα当且仅当有一个有穷子集Φ0，α是从Φ0可演绎的.

证明 如果Φα，那么有一个有穷长的假设性证明，这个证明的最后一步是公式α，并且所有未被消除的假设都属于Φ，这些未被消除的假设的全体就是Φ的一个有穷子集，不妨设为Φ0，则Φ0α.

如果有Φ的一个有穷子集Φ0，使得Φ00α，那么因为Φ0⊆Φ，由性质1可得：Φα.

性质4 如果Φα并且（α→β），那么Φβ.

证明 因为Φα，所以有一个假设性证明π1，而α是π1的最后一步得出的公式，并且所有未被消除的假设都属于Φ，即：

又因α→β，所以有一个证明π2，并且α→β是π2的最后一步得出的公式，并且该证明中，没有未被消除的假设，即：

现在，把π2写在π1的最后一个公式α的下面，并在π2的最后一个公式α→β下面写下β.这样，就得到一个假设性证明π，公式β为π的最后一步得出的公式，并且所有未被消除的假设都属于Φ，即：

根据可演绎定义得：Φβ.

性质5 Φα当且仅当Φ⇁⇁α.

证明 如果Φα并且由FQC的定理：α→⇁⇁α，再利用性质4可得：Φ⇁⇁α.反之，如果Φ⇁⇁α并且由FQC的定理⇁⇁α→α，再利用性质4可得：Φα.

性质6 如果对某个公式β，Φβ并且Φ⇁β，那么对任一公式α，Φα.

证明 因为Φβ，所以存在一个假设性证明π1，并且π1的最后一步是β；又因Φ⇁β，所以存在一个假设性证明π2，并且π2的最后一步是⇁β.π1和π2中所有未被消除的假设都属于Φ.构造证明π如下：把π2写在β的下面，然后在⇁β的下面再接如下的一个子证明，作为π的一个子证明.

这样就得到了一个证明π，如图6-1所示.

图6-1

π的最后一步是α，并且所有未被消除的假设都属于Φ.根据可演绎定义得：Φ

性质7 Φ（α∧β）当且仅当Φα并且Φβ.

证明 如果Φ（α∧β），由FQC定理：α∧β→α和α∧β→β，再由性质4可得：Φα并且Φβ.

如果Φα并且Φβ，那么分别存在假设性证明π1和π2，使得在π1的最后一步得出α，在π2的最后一步得出β.而且所有未被消除的假设都属于Φ.即：

然后，把π2写在α之下，再在β之下接

这样就得到了一个证明π，它的最后一步是α∧β，并且所有未被消除的假设都属于Φ（如图6-2所示）.根据可演绎定义得：Φα∧β.

图6-2

性质8 如果Φα，那么Φ（α∨β）；如果Φβ，那么Φ（α∨β）.

证明 根据可演绎定义得：存在一个假设性证明π，π的最后一步得出的公式是α或β，并且所有未被消除的假设都在Φ中.因此，只要在π之下，按照∨+规则接着写一个公式α∨β，那么该证明π′就是由Φ得到的（α∨β）的一个证明.如图6-3所示.

图6-3

性质9 如果Φ（α→β）并且Φα，那么Φβ.

证明 因为Φ（α→β）并且Φα，根据可演绎定义得：存在假设性证明π1和π2，并且在证明的最后一步分别是公式（α→β）和α.而所有未被消除的假设都属于Φ.即：

现在，构造非假设性证明π如下：

在证明π1的最后一个公式（α→β）之下，紧接着写下π2，再接着π2的最后一个公式α之下，紧接着写如下两个公式：

因为π的最后一步得出公式β，而且π中所有未被消除的假设都属于Φ.根据可演绎定义得：Φβ.

性质10 如果Φα→β，那么Φ，αβ.

证明 因为Φα→β并且Φ⊆Φ∪{α}（即：Φ⊆Φ，α）.由性质1得：Φ∪{α}α→β，即：Φ，αα→β.又α∈Φ∪{α}，由性质2得：Φ∪{α}α.即：Φ，αα.由性质9可得：Φ，αβ.

性质11 如果Φ，αβ，那么Φα→β.

证明 因为Φ，αβ，根据可演绎定义得：存在一个假设性证明π1，π1的最后一个公式是β，并且所有未被消除的假设都属于Φ，α.

在π1中，把形如

而α未被消去的子证明都换成如下的子证明：

在π1的最后一个子证明中，用Hyp规则引入的假设或是α或不是α.如果是α，那么按上面的规定，π1的最后一个子证明被换为

(www.daowen.com)

这样就得到一个证明π2，而π2的最后一个公式就是α→β，并且所有未被消除的假设都属于Φ，根据可演绎定义得：Φα→β.

如果在π1的最后一个子证明中，用Hyp规则引入的假设不是α，不妨设为

由于β→（α→β）是FQC的一个定理，因此存在一个证明π3，它的最后一个公式就是β→（α→β）.把π3接在π1的公式β之下，再在β→（α→β）之下写α→β，即：

于是就得到一个证明π，即：

它的最后一个子证明（γ之前）的部分是将π1中把形如

而α未被消除的子证明换为子证明：

而得.

π的最后一个公式是α→β，并且所有未被消除的假设都属于Φ，根据可演绎定义得：Φα→β.

性质11被称为狭谓词逻辑的演绎定理.

性质12 Φα当且仅当有Φ的有穷多个公式φ0，φ1，…，φn 满足φ0→（φ1 →…→（φn →α）…）.

证明 由性质3得：Φα当且仅当Φ有一个有穷子集Φ0，使得Φ0α.令Φ0={φ0，φ1，…，φn}.由性质10和性质11得：

性质13 如果Φα并且Φ，αβ，那么Φβ.

证明 因为Φ，αβ，由性质11可得：Φα→β.又因为Φα，由性质9得：Φβ.

性质14 如果Φ，αβ并且Φ，⇁αβ，那么Φβ.

证明 因为Φ，αβ并且Φ，⇁αβ，由性质11得：Φα→β并且Φ⇁α→β.因为（α→β）→（⇁α→β）→β是FQC的定理，即：（α→β）→（⇁α→β）→β.由性质4得：Φ（⇁α→β）→β，再由性质9得：Φβ.

性质15 如果Φ，⇁αβ并且Φ，⇁α⇁β，那么Φα.

证明 因为Φ，⇁αβ并且Φ，⇁α⇁β，由性质11可得：Φ⇁α→β并且Φ⇁α→⇁β.又因为：（⇁α→β）→（⇁α→⇁β）→α是FQC的定理，即：（⇁α→β）→（⇁α→⇁β）→α.由性质4和性质9可得：Φα.

性质16 如果Φ，αγ并且Φ，βγ，那么Φ，α∨βγ.

证明 因为Φ，αγ并且Φ，βγ，由性质11得：Φα→γ并且Φβ→γ.又因为：（α→γ）→（（β→γ）→（α∨β→γ））是FQC的定理，即：（α→γ）→（（β→γ）→（α∨β→γ））.再由性质4和性质9得：Φα∨β→γ，再利用性质10得：Φ，α∨βγ.

性质17 Φα↔β当且仅当Φα→β并且Φβ→α.

证明 因为Φα↔β，又因为（α↔β）→（α→β）和（α↔β）→（β→α）是FQC的定理，即（α↔β）→（α→β）和（α↔β）→（β→α）.由性质4得：Φα→β并且Φβ→α.

如果Φα→β并且Φβ→α，又因（α→β）→（（β→α）→（α↔β））是FQC的定理，即：（α→β）→（（β→α）→（α↔β））.由性质4和性质9可得：Φα↔β.

性质18 如果Φα↔β并且Φα，那么Φβ；如果Φα↔β并且Φβ，那么Φα.

证明 因为Φα↔β，又因（α↔β）→（α→β）是FQC的定理，即：（α↔β）→（α→β），由性质4可得：Φα→β，又Φα，由性质9可得：Φβ.

同理可证性质18的另一部分（从略）.

性质19 如果Φ∀xα，那么Φα（t/x）.

证明 利用∀xα→α（t/x）和性质4可得结论.

性质20 如果Φα（t/x），那么Φ∃xα.

证明 利用α（t/x）→∃xα和性质4可得结论.

性质21 如果Φα（y/x）并且y不在Φ，∀xα中自由出现，那么Φ∀xα.

（这里，“y不在Φ中自由出现”是指y不在Φ的任一个公式中自由出现.）

证明 因为Φα（y/x）并且y不在Φ，∀xα中自由出现，那么由性质11得：Φ含有有穷多个公式φ0，φ1，…，φn 满足

由于y不在Φ中自由出现，因此我们可以在φ0→φ1…→（φn→α（y/x））…的一个证明中，继续使用∀+ 规则而得公式

又，∀y（φ0 →φ1 →…→（φn →α（y/x））…）→（φ0 →φ1 →…→（φn →∀yα（y/x））），

由性质4得：

再由性质11得：Φ∀yα（y/x）.

然而 在FQC中，∀yα（y/x）～∀xα（这里，y不 在∀xα中自由出现），即：∀yα（y/x）→∀xα，由性质4得：Φ∀xα.

性质22 如果Φ，α（y/x）β并且y不在Φ，∃xα和β中自由出现，则Φ，∃xαβ.

证明 因为Φ，α（y/x）β并且y不在Φ，∃xα和β中自由出现，那么根据性质11得：Φα（y/x）→β.由性质21又得：Φ∀y（α（y/x）→β）.利用第五章第四节可证公式（60），即

由性质4得：Φ∃yα（y/x）→β.又由在FQC中，∃xα→∃yα（y/x）（这里，y不在∃xα中自由出现），即：

由FQC定理：（∃xα→∃yα（y|x））→（∃yα（y|x）→β）→（∃xα→β），和性质4得：

最后利用性质10得：Φ，∃xαβ.

例 以下三个公式是等价关系理论中的三条公理：

试证明：φ2，φ3，∃z（R（x，z）∧R（y，z））R（x，y）.

证明

本节中的语法概念——可演绎性与第五章第五节中的语义概念——逻辑后承相对应.