代入

代入(substitution)谓词演算的基本运算之一设沪是一个谓词演算公式，x1}x2}...}x。是沪中的(未必全部)自由变元，tt,tz,""",t，是n个项，则用项t1,tp,"..,t。分别代替xt,xz,""",x，在沪中所有出现的运算，称为用tt ,tp, """ ,t。代人xt}x.z}...,,x .其结果式用符号记之。