证明：∀x（Ax→Bx）→(∀xAx→∀xBx)。
-----------
|.1.∀x（Ax→Bx）,                CP.
|.2.Ay→By,                    1,UI.
|.|.3.∀xAx,                    CP
|.|.4.Ay,                         3,UI.
|.|.5.By,                      2,4,MP.
|.|.6.∀xBx,                    5,UG.
|.7.∀xAx→∀xBx,               3-6,CP.
8.∀x（Ax→Bx）→(∀xAx→∀xBx). 1-7,CP.
_________


这不是徐明的符号逻辑里面的吗？

Fitch发明的。
见《符号逻辑讲义》

谢谢！

不知道你说的消除假设是指什么？
如果按照我的理解，在《讲义》这本书里面，假设都可以由联结词规则来消除，譬如假设A（进格），得到B，那么可以得到A->B（退格），这时假设A就消除了。

有竖线的子证明思路很清晰，我好像在哪里看过说不用竖线进退格也可以(忘了，年龄不大记忆力不行了？)_0

我说的是：
1.《讲义》里“结构规则”的"hyp".有引入假设，没有消除假设。比较老的数理逻辑教材里有这样的规则。
2.《讲义》里蕴涵引入规则，有引入，有消除。
我感觉它们应该合二为一。

宋文坚《逻辑学》里，使用“进退格”。
柯匹的逻辑学导论里，使用“弯箭头”。
徐明的《符号逻辑讲义》 ，“丁字头”。
老的数理逻辑，使用“蝌蚪线”。
我觉得“进退格”最好，写着方便。
【只是百度帖子里，见了“进退格”就乱套了。】
“进退格”的子证明，思路很清晰，大有深意。


为什么需要单独消除假设的规则呢

不需要单独消除假设的规则;
也
不需要单独引入假设的规则；
有“蕴涵引入规则”【条件证明规则里[CP]】就够了。
*
《符号逻辑讲义》里“结构规则”的"hyp"，有引入假设，没有消除假设；
它是“半个规则”。
"hyp"不用为好。

这个证明有三列，序号、命题、理由。
序号、命题的两列、挺整齐。
但是，理由那列、不整齐了。
怎么办？

你可能没看完《讲义》中的费奇式推演的那章。
假设规则不仅仅是为了蕴含引入而设的，还有析取消除、双蕴含引入、作为前提等等

《讲义》注解里，徐明老师自己说，不太了解费奇的书；只是转述。

自然演绎法和公理法是等价的，如同汉语和英语，都可以表情达意。
翻译时有个标准：
信达雅。
*
“假设规则”可能是公理法的好规则，
却不见得是自然演绎的好规则。
*