公理系统没有假设规则。

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

自然演绎是指一类系统，具体谁首先使用的不知道。而《讲义》中所介绍的是费奇所使用的系统，属于自然演绎的一种。不同的书上介绍的自然演绎系统都大同小异，基本结构都是一样，差别只是某些规则和符号的使用。其实我觉得自然演绎没必要深究，因为这种系统很难严格化讨论，学好一种的使用就足够。重点还是放在公理系统比较好。

我感觉表列系统好像是多余的，没啥优点。
到是现在书上都没有系统的说下矢列演算系统？

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

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

科庇的《符号逻辑》有严格的讨论。

不是吧。。。怎么严格法？

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

科庇那本书，自然演绎系统中演绎是怎么定义的？

参考23楼。

经网友NPC和无沉的启发，找到一份解答。
陈晓平先生的《自然演绎逻辑导论》2006年，第二版前言，2页-3页，
【假设域的表示】。
1.德国人 甘岑【G. Gentzen,1934】 的树形方法。现在很少人使用。
2.波兰人 雅斯可夫斯基【S.Jaskowski,1934 】的两种方法。
2.1 方框法。假设域圈在方框内；方框外各行不依赖假设。
科庇【I M Copi,1954】，费奇【F Fitch，1952】,伯格曼等人简化成一条竖线，表示假设域。
2.2 标记法。假设域的每一行都作标记，指出它依赖的假设。奎因【W V Qine,1950】,苏佩斯作了改进。
****
不管是方框，是竖线，还是数字符号，
只要能明确地表示出假设域，
改进则进，该退则退，
就好。


2.2 标记法。假设域的每一行都作标记，指出它依赖的假设。奎因【W V Qine,1950】,苏佩斯作了改进。
这个是不是加标系统？

1.只看到陈晓平的这些资料；不知道“标记法”的细节。
不过，其中的三个要点是必备的：
引入假设，退出假设的位置、明确表示出来了，
假设域里的命题也不许可左摇右摆了。
2.类似的，
弗雷格的量词符号非常奇怪，影响了传播；
但是，
现代逻辑已经有非常简洁的符号，大头向下的"A"，脸向后的"E".


斜形形式证明，formal proof of oblique form ,
刘风璞等，逻辑学大全，1991年，195页。