《逻辑学导论》第二部分:演绎
现代逻辑 演绎方法
“尽管在有效性的形式证明能够机械地确定一个给定序列是否一个证明的意义上，形式证明是能行的，但构建一个形式证明并没有一个能行的程序”
这里应该说的是命题逻辑吧，我记得命题逻辑形式系统对于任意体系内的陈述是否为定理（可由公理推理出来）是存在机械性的判定方法的，也就是说对于一个证明可以在有效时间内机械判定其是否有效（一个证明等同于前提的合取蕴含结论），那为什么书上又说命题逻辑不存在机械证明呢？求指点