(4)当a为(x)时 41)若讠=j,则:a中所有x;都是约束出现,从而a(x;/t)=a 由于σ与o对不是x的个体变元符号指派的值相同,由定理3,14 知Ia(x/)兮Ia台Ib (4.2)若i≠j,则:a(x;/t)为(x)f(x;/t.由于t对c;在a 中自由,故x不在α中自由出现或者xj不在t中出现 (4.21)若x;不在α中自由出现,仿(4.1)可证(**)成立 1(1.22)若不在中出现,由定理313得:对任意a∈D j/a)=t.从而 a 当且仅当I(x)3(x:/t) 当且仅当:对任意a∈D,r ai/a (x;/t 当且仅当:对任意a∈D,IHm(x;/t),"=0(x;/a) 当且仅当:对任意a∈D,I (归纳假设) 当且仅当:对任意a∈D,同a1 当且仅当:对任意a∈D,(x/(m/p)B 当且仅当:对任意a∈D,ⅠmnB, (0(x/a)(x;/t)=a(x;/t0)(x/a) 当且仅当Ⅰ (x;/t VxI)B 当且仅当Ⅰ o(I 归纳证完,(**)成立.证毕(4) F α  (∀xj)β / (4.1) V i = j, .α I# xi Q_`DTU α(xi/t) = α. 89 σ ( σ 3 xi $ -%Æ8E> 3.14 : I | σ α(xi/t) ⇔ I | σ α ⇔ I | σ α (4.2) V i = j, . α(xi/t)  (∀xj)β(xi/t). 89 t  xi  α $8] xi 3 α $8D!5 xj 3 t D (4.2.1) V xi 3 α $8Dt (4.1) 4H (∗∗) OP (4.2.2) V xj 3 t D8E> 3.13 [:/ a ∈ D, t σ(xj/a) = t σ. TU I | σ α(xi/t) FMNF I | σ (∀xj)β(xi/t), FMNF:/ a ∈ D, I | σ(xj/a) β(xi/t). FMNF:/ a ∈ D, I | σ β(xi/t), σ = σ(xj/a) FMNF:/ a ∈ D, I | σ(xi/tσ) β, (CD%) FMNF:/ a ∈ D, I | σ(xi/tσ) β, FMNF:/ a ∈ D, I | σ(xj/a)(xi/tσ) β. FMNF:/ a ∈ D, I | σ(xi/tσ)(xj/a) β, (σ(xj/a)(xi/tσ) = σ(xi/tσ)(xj/a)) FMNF I | σ(xi/tσ) (∀xj)β, FMNF I | σ(xi/tσ) α. CDHM (∗∗) OP Hs 13