| 约束个体变元易字规则 rule of alphabetic change of bound individual variables 狭谓词演算HA系统中的初始变形规则。国内一种有影响的表述是：公式A中的一个约束个体变元Δ1，可由另一个体变元Δ2替换。但是替换必须在一特定量词及其辖域内到处实现。如Δ1在多个量词内出现，替换可以只在一个量词及其辖域内进行。替换时则要求：(1)Δ2在A中不能作自由变元出现。(2)如Δ2在A中约束，则被替换的Δ1不能在Δ2的辖域中出现。这样得到的公式B，如果├A，那么├B。如果违反这些要求，结果就可能不合式，或者不能保持普遍有效。例1：在“(ᗄx)F(x)→F(y)”中，如用y替换x，则得“(ᗄy)F(y)→F(y)”。y既约束，又自由，因此违反规则(1)，所以不合式。例2，在普遍有效公式(ᗄx)(∃y)R(x，y)→(∃v)R(u，v)中，设以u替换v，则得“(ᗄx)(∃y)R(x，y)→(∃u)R(u，u)”，结果不普遍有效。因违反了规则(1)。 |