定义 设 是含命题变项 的命题公式, 是 个谓词公式, 用 代替 中的 , 所得公式 称为 的代换实例.