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

在经典命题演算公理系统L中,由于演绎定理的运用,演绎序列通常都会较为简单;而证明中只能使用公理和MP规则,导致证明的步骤较为复杂。根据杜国平的方法,只要存在演绎序列,就能找到相应的公理证明。实际上,有一类定理的演绎程序比较容易获得,也有一些定理的演绎程序直观上并不容易发现。因而如何搜索演绎序列,就是一个颇为实际的问题。通过将待证公式拆分成前件和后件,我们可以粗略得到两种寻找演绎序列的方法:若公式形如X_(n)→…(X_(i)→…(Y→Z)…),后件可以层层拆分,则在演绎程序中将多次拆分获得的前件不断作为前提,直到后件为原子公式,以寻找演绎序列(若难以找到,则考虑用L_(3));若公式形如(((X_(n)→Z)→…→X_(i))→…Y)→X_(0),第一次拆分之后,后件是原子公式,则考虑将前件或原待证公式进行相应的"变形",结合归谬法等方法寻找演绎序列。如此,通过获得的演绎序列,我们就可以发现其中公式的相互作用,并以此作为"证明的技巧",最终得到严格的公理证明。