后件概括规则 rule of consequent generalization 狭谓词演算HA系统中的初始变形规则。国内一种有影响的表述是:如果个体变项Δ在A中不出现,从├A→B(Δ),可得├A→(Δ)B(Δ)。这是一个引入全称量词的规则。与命题演算的定理“├(p→q)∧(p→r)→(p→q∧r)”相当。是以下图式的推广:  当个体域无穷时,可表示成{1,2,…n,…}用上面图式可得一系列的断定: 这样应该可以得:├A→B(1)∧B(2)∧…∧B(n)∧… 按定义,它不合式。但是它相当于全称式(ᗄx)B(x)。这样就有:├A→(ᗄx)B(x)。 |