| 命题变元代入规则 rule of substitution for propositional variable 狭谓词演算HA系统中的初始变形规则。国内一种有影响的表述是：在公式A中出现的命题变元π可由一公式B代入，必须在π出现的所有位置上进行，并要求：(1)如Δ在A中均为自由变元，则B不得含有约束变元Δ;(2)如Δ在A中为约束变元，则B不得含有自由变元Δ;(3)B中的约束个体变元Δ，如在A中也是约束的，那么π不能在量词(Δ)和(∃Δ)的辖域中，这样代入后的合式公式能保持普遍有效性。如果┝A，那么┝Aπ/B，违反上面的要求，代入后的公式就可能不合式，或者不能保持普遍有效性。例1：在“p→p∨F(x)”中，用(ᗄx)G(x)代p，则得(ᗄx)G(x)→(ᗄx)G(x)∨F(x)，其中(ᗄx)G(x)∨F(x)不合式。究其原因是违反了规则(2)。例2，下列公式： (ᗄx)(F(x)→p)→((∃x)F(x)→p) 是谓词演算的定理，是普遍有效的。因之 A：(ᗄx)(F(x)→p)→((∃x)F(x)→(ᗄx)(p∧(H(x)∨H(x)))) 也是普遍有效的。设以F(x)代p，则得： (ᗄ(x)(F(x)→F(x))→((∃x)F(x)→(ᗄ(x)(F(x)∧(H(x)∨H(x)))) 销去H(x)∨H(x)可得： (ᗄ(x)(F(x)→F(x))→((∃x)F(x)→(ᗄx)F(x)) 不普遍有效。因为代入时违反了规则(2)。 |