假定S是一个固定的符号集.

定义6.1 给定公式α和两两不相同的个体变项x0，x1，…，xn以及任意的项t0，t1，…，tn.由α经t0，t1，…，tn对x0，x1，…，xn的联立代入而得的公式α（t0/x0，t1/x1，…，tn/xn）的归纳定义如下：

当x不在ti0，ti1，…，tis-1之间出现时，这里的y是x；否则y就是v0，v1，…中不在α，ti0，ti1，…，tis-1中出现的下标最小的那个个体变项.

由定义6.1可得：

（β∧γ）（t0/x0，t1/x1，…，tn/xn）

=β（t0/x0，t1/x1，…，tn/xn）∧γ（t0/x0，t1/x1，…，tn/xn），

（β→γ）（t0/x0，t1/x1，…，tn/xn）

=β（t0/x0，t1/x1，…，tn/xn）→γ（t0/x0，t1/x1，…，tn/xn），

（β↔γ）（t0/x0，t1/x1，…，tn/xn）

=β（t0/x0，t1/x1，…，tn/xn）↔γ（t0/x0，t1/x1，…，tn/xn）.

注意：在定义6.1的（5）中，引进变项y是为了保证出现在ti0，ti1，…，tis-1之间的个体变项不会在代入后受到量词的“俘获”.当

free（∀xβ）∩{xi|i∈{0，1，…，n}并且xi≠ti}=∅

时，即没有一个∀xβ的自由变项xi使得xi≠ti时，从（5）可得

（∀xβ）（t0/x0，t1/x1，…，tn/xn）=∀xβ（x/x），

这里的β（x/x）就是β.因此，又有

（∀xβ）（t0/x0，t1/x1，…，tn/xn）=∀xβ.

对于∃xβ，也有同样的结论.

注意，作联立代入时，x0，x1，…，xn之间的顺序无关紧要.当x0，x1，…，xn之间的顺序改变时，t0，t1，…，tn之间的顺序也随之作相应的改变，由此得到的联立代入的结果还是相同的.当n=1时，即联立代入仅发生在一个变项上，此时简称代入.

下面是一些联立代入的例子.

例6.1 求（P（v0）∨R（v1，v2））（v2/v1，v1/v0，v0/v2）.

解 （P（v0）∨R（v1，v2））（v2/v1，v1/v0，v0/v2）

=（P（v0）（v2/v1，v1/v0，v0/v2））∧

（R（v1，v2）（v2/v1，v1/v0，v0/v2））

=P（v1）∨R（v2，v0）.

例6.2 求（∃v0 R（v0，v1，v2））（v4/v0，v1/v2）.

解 因为

free（∃v0 R（v0，v1，v2））∩{v0，v2}={v1，v2}∩{v0，v2}={v2}，

所以

（∃v0 R（v0，v1，v2））（v4/v0，v1/v2）

=∃v0（R（v0，v1，v2）（v1/v2））=∃v0 R（v0，v1，v1）.

例6.3 求（∀v0 R（v0，v1，v2））（v5/v0，v0/v1，v3/v2）.

解 因为

free（∀v0 R（v0，v1，v2））∩{v0，v1，v2}={v1，v2}∩{v0，v1，v2}={v1，v2}，所以，取v4是不在R（v0，v1，v2）和{v0，v3}中出现的下标最小的个体变项.于是，

（∀v0 R（v0，v1，v2））（v5/v0，v0/v1，v3/v2）

=∀v4（R（v0，v1，v2）（v0/v1，v3/v2，v4/v0））=∀v4 R（v4，v0，v3）.

例6.4 求（∃v0 P（v0，v3）∧∀v1 R（v0，v1，v2））（v4/v0，v2/v1，v1/v2，v3/v3）.

解 因为

free（∃v0 P（v0，v3））∩{v0，v1，v2}={v3}∩{v0，v1，v2}=∅，

即v0不在{v4，v2，v1}中出现，v0就是取v0，又因为

free{∀v1 R（v0，v1，v2））∩{v0，v1，v2}={v0，v2}∩{v0，v1，v2}={v0，v2}，

而v1在{v4，v1}中出现，所以取y为v3，它不在∀v1 R（v0，v1，v2），v4，v1中出现，并且是下标最小的.于是，

（∃v0 P（v0，v3）∧∀v1 R（v0，v1，v2））（v4/v0，v2/v1，v1/v2，v3/v3）(www.daowen.com)

=（∃v0 P（v0，v3））（v4/v0，v2/v1，v1/v2，v3/v3）∧

（∀v1 R（v0，v1，v2））（v4/v0，v2/v1，v1/v2，v3/v3）

=∃v0（P（v0，v3）（v0/v0））∧∀v1（R（v0，v1，v2）（v4/v0，v1/v2，v3/v1））

=∃v0 P（v0，v3）∧∀v3 R（v4，v3，v1）.

下面的代入引理表明了按我们规定的代入所具有的语义性质.即：公式α（t0/x0，t1/x1，…，tn/xn）在解释Σ=（A，θ）下成立，当且仅当对x0指派Σ（t0），对x1指派Σ（t1），……，对xn指派Σ（tn）时，α在解释Σ（Σ（t0）/x0，Σ（t1）/x1，…，Σ（tn）/xn）=（A，θ（Σ（t0）/x0，Σ（t1）/x1，…，Σ（tn）/xn））中成立.

引理6.1（代入引理） 令x0，x1，…，xr两两不同，Σ=（A，θ）是一个解释，a0，a1，…，ar∈A，

（1）对于任意的项t，有

Σ（t（t0/x0，t1/x1，…，tn/xn））

=Σ（Σ（t0）/x0，Σ（t1）/x1，…，Σ（tn）/xn）（t）；

（2）对于任意的公式α，有

证明 （1）任一个项t或是一个个体变项x或是一个个体常项c，根据联立代入的定义，我们只须考虑以下三种情况：

（2）施归纳于公式α的结构：

①ΣR（t0′，t1′，…，t′r-1）（t0/x0，t1/x1，…，tn/xn） 当且仅当R A（Σ（t0′（t0/x0，t1/x1，…，tn/xn）），

Σ（t1′（t0/x0，t1/x1，…，tn/xn）），…，

Σ（t′r-1（t0/x0，t1/x1，…，tn/xn））） 当且仅当R A（Σ（Σ（t0）/x0，Σ（t1）/x1，…，Σ（tn）/xn）（t0′），

Σ（Σ（t0）/x0，Σ（t1）/x1，…，Σ（tn）/xn）（t1′），…，

Σ（Σ（t0）/x0，Σ（t1）/x1，…，Σ（tn）/xn）（t′r-1）） （由（1））当且仅当

Σ（Σ（t0）/x0，Σ（t1）/x1，…，Σ（tn）/xn）R（t0′，t1′，…，t′r-1）.

②Σ（⇁β）（t0/x0，t1/x1，…，tn/xn）

当且仅当 Σ⇁β（t0/x0，t1/x1，…，tn/xn）

当且仅当 Σ β（t0/x0，t1/x1，…，tn/xn）

当且仅当 Σ（Σ（t0）/x0，Σ（t1）/x1，…，Σ（tn）/xn）/β （由归纳假设）

当且仅当 Σ（Σ（t0）/x0，Σ（t1）/x1，…，Σ（tn）/xn）⇁β.

③Σ（β∨γ）（t0/x0，t1/x1，…，tn/xn）

当且仅当 Σ（β（t0/x0，t1/x1，…，tn/xn）∨γ（t0/x0，t1/x1，…，tn/xn））

当且仅当 Σβ（t0/x0，t1/x1，…，tn/xn）或者

Σγ（t0/x0，t1/x1，…，tn/xn）

当且仅当 Σ（Σ（t0）/x0，Σ（t1）/x1，…，Σ（tn）/xn）β或者

Σ（Σ（t0）/x0，Σ（t1）/x1，…，Σ（tn）/xn）γ （由归纳假设）

当且仅当 Σ（Σ（t0）/x0，Σ（t1）/x1，…，Σ（tn）/xn）（β∨γ）.

④下面仅证明：当α形如∃xβ时结论成立，α形如∀xβ的证明留给读者完成.

当且仅当有一个a∈A，

当且仅当有一个a∈A，

（这里利用叠合引理而得.因为y根本不在ti0，ti1，…，tis-1之间出现）

当且仅当有一个a∈A，

（因为y既不是x也不在β中出现，利用叠合引理可得）

当且仅当有一个a∈A，

（由于xi0，xi1，…，xis-1∈free（∃xβ），而x≠xi0，x≠xi1，…，x≠xis-1，因此，Σ（Σ（ti0）/xi0，Σ（ti1）/xi1，…，Σ（tis-1）/xis-1，a/x）=Σ（Σ（ti0）/xi0，Σ（ti1）/xi1，…，Σ（tis-1）/xis-1）（a/x）.）

当且仅当

当且仅当

（因为，对于不等于i0，i1，…，is-1的i而言，xifree（∃xβ）或者xi=ti.）