我已经拆解到这个程度了，再看不懂就是智商有缺陷了。//@杨学志_5G创新:对，这就是所有的人都认识不到的地方。 //@高福先生:我原以为您说的sub(y, 19, num(y))中第1，3参数y有二义，原来您以为y和19所代表的y有二义啊？这根本不是问题。第二个参数是19，不是y！subst是基于词法的函数项，语义上编码了”对对应公式中可能的自由变量y进行替换“，subst本身的定义一定是基于词法的，即那个所谓的自由变量根本不会出现。