证明：∀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.
_________


谢谢！

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

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


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

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

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

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

徐明的《符号逻辑讲义》里，自然演绎称为费奇演绎，确实不了解“费奇”的资料。
好像自然演绎里，甘岑的贡献大？

一块买了两本。另书是陈晓平先生的《自然演绎逻辑导论》2006年。
上乘之作。
第二版前言介绍了自然演绎逻辑系统。
创始人有两个：1934年。
德国甘岑，G. Gentzen
波兰雅斯可夫斯基，S.Jaskowski
核心内容是条件证明规则【蕴涵引入规则】。

其实,表列系统是最简洁的证明方法。
类似于短真值表法、或间接证明法[IP].
但是不漂亮。

条件证明规则和那些推理规则，共同构成“完全的”系统。
而没有条件证明规则，是“不完全的”。

参考23楼。