经典否定蕴涵系统定理的能行证明

The effective proof of classical negation implication system theorem

借鉴亚里士多德的化归方法,通过反复使用双否消去规则、否定内移规则、移动排序规则、合并规则和归约规则,可以将命题逻辑否定蕴涵系统的任一定理等值地化归为一个形如[YY]的公式。再借助相应的证明子程序和嵌入程序可以能行地构建该定理的证明。

Inspired by Aristotle’s reduction method,we can equivalently reduce any theorem of the negation implication system of the propositional logic to a formula in the form of[YY]by repeatedly using the rule of double negation elimination,rule of negation inward movement,rule of moving sorting,rule of merging and rule of reduction.By introducing the corresponding proof subprogram and embedded program,we can effectively construct the proof of the theorem.