论经典命题逻辑公理系统L中的证明技巧

On proving skills in axiomatic system L of classical propositional logic

在经典命题逻辑的学习中,公理系统L中的定理证明只能使用公理模式和推理规则,对于初学者而言,常常显得强人所难,主要表现为找不到证明的突破口。事实上,可以从两个方向出发:一方面,从公理模式出发,分析每条公理模式的特性,由此可得消件法和换位法两个小技巧;另一方面,通过使用演绎定理,一般我们可得到待证定理的演绎证明序列,而通过对演绎证明序列的"仔细观察",可以获得相应公理证明的"突破口"。这些技巧,可以提高初学者的学习效率,优化数理逻辑的教学,也可以为定理机械化证明的理论和方法提供必要的实践准备,以促进新时代逻辑学教学现代化的实现。

In the study of classical propositional logic,the axioms in the axiomatic system(prove that they can only use axioms and reasoning rules.For beginners,they often find it hard to find a breakthrough that can not be found.In fact,we can proceed from two directions:on the one hand,starting from the axiom model,analyzing the characteristics of each axiom model,we can get two tips,i.e.,the elimination method and the transposition method;on the other hand,by using the deduction theorem,generally,we can obtain the sequence of the deductive proofs of the theorem to be proved,and through the'careful observation'of the sequence of deductive proofs,we can obtain the'break-through'that the corresponding axioms prove.These skills can improve the learning efficiency of beginners,optimize the teaching of mathematical logic,and can also provide the necessary practical preparation for the theory and method of theorem mechanization to promote the modernization of logic teaching in the new era.