论L中演绎序列的两种搜索方法  

On Two Search Methods for Deductive Sequences in L

作　　者：程和祥 樊毅 CHENG He-xiang;FAN Yi(Postdoctoral Mobile Station of Southwest University of Political Science&Law,Chongqing 401120,China;Postdoctoral Workstation of Guizhou Academy of Social Sciences,Guiyang,Guizhou 550002,China;Beijing Yuandian Mingshi Technology Co.,Ltd.,Beijing 102218,China)

机构地区：[1]西南政法大学博士后流动站,重庆401120 [2]贵州省社会科学院博士后工作站,贵州贵阳550002 [3]北京远点明视科技有限公司,北京102218

出　　处：《贵州工程应用技术学院学报》2021年第6期80-85,共6页Journal of Guizhou University Of Engineering Science

基　　金：2020年地方立法研究规划项目“大数据时代个人信息风险控制立法研究”,项目编号:DFLF2020Y06;教育部人文社会基金项目“可能与必然的概念史研究”,项目编号:19YJC72002。

摘　　要：在经典命题演算公理系统L中,由于演绎定理的运用,演绎序列通常都会较为简单;而证明中只能使用公理和MP规则,导致证明的步骤较为复杂。根据杜国平的方法,只要存在演绎序列,就能找到相应的公理证明。实际上,有一类定理的演绎程序比较容易获得,也有一些定理的演绎程序直观上并不容易发现。因而如何搜索演绎序列,就是一个颇为实际的问题。通过将待证公式拆分成前件和后件,我们可以粗略得到两种寻找演绎序列的方法:若公式形如X_(n)→…(X_(i)→…(Y→Z)…),后件可以层层拆分,则在演绎程序中将多次拆分获得的前件不断作为前提,直到后件为原子公式,以寻找演绎序列(若难以找到,则考虑用L_(3));若公式形如(((X_(n)→Z)→…→X_(i))→…Y)→X_(0),第一次拆分之后,后件是原子公式,则考虑将前件或原待证公式进行相应的"变形",结合归谬法等方法寻找演绎序列。如此,通过获得的演绎序列,我们就可以发现其中公式的相互作用,并以此作为"证明的技巧",最终得到严格的公理证明。In the classical propositional calculus axiom system L,due to the use of the deductive theorem,the deductive sequence is usually relatively simple;and the axiom and MP rules can only be used in the proof,so the proved steps are more complicated.According to Du Guoping’s method,as long as there is a deductive sequence,the corresponding axiom proof can be found.In fact,the deductive procedure of a class of theorems is relatively easy to obtain,and some deductive procedures of theorem are not easy to find intuitively.Therefore,how to search for deductive sequences is a rather practical problem.By splitting the formula to be proved into the front and the back,we can roughly get two ways to find the deductive sequence:if the formula is like X_(n)→…(X_(i)→…(Y→Z)…),the latter can be split layer by layer.The predecessor obtained by multiple splits is constantly used as a premise to find the deductive sequence;if the formula is like(((X_(n)→Z)→…→X_(i))→…Y)→X_(0),after the first split,the latter is an atomic formula,Then consider the corresponding"deformation"of the former or the original formula,and find the deductive sequence by combining the methods of reduction to obsurdity.In this way,through the obtained deductive sequence,we can find out the interaction of the formulas,and use this as a"proofing technique",and finally obtain strict axiom proof.

关 键 词：公式类型 拆分 L_(3) 归谬法 

分 类 号：B81[哲学宗教—逻辑学]