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

On Two Search Methods for Deductive Sequences in L

在经典命题演算公理系统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.