联合演算的结构判定方法初探

On Structure Determination Method of Joint Calculus

与命题演算一样,联合演算也有相应的判明一公式是否永真的方法。希尔伯特和阿克曼提出的"审定法"就是这样一种方法,但审定法没有区分联合演算的两个层次,试图在联合演算的第一个层次上解决判定问题,从而暴露出严重的弱点。在本文中,我将对审定法进行改造,深入解读竖号的逻辑意义,厘清联合演算的两个层次,在类逻辑和命题逻辑之间建立完全的类比,提出一种具有普遍意义的更严格的方法,即结构判定方法。该方法能够帮助我们揭示传统推理式的前提和结论之间的联系的必然性,从而判明一联合演算公式是否永真式,并且帮助由任一可满足式(包括永真式)得出永真式。

Similar to the propositional calculus,joint calculus also has the corresponding method to ascertain whether a formula is tautology or not. The determination method proposed by Hilbert and Ackermann is such a method. But this method does not differentiate the two levels of joint calculus, tries to solve the determination problem at the first level in the calculus,thus exposes serious weaknesses. In this paper,I will reform the method of Hilbert and Ackermann,reinterpret in-depth the logical meaning of vertical symbol,clarify the two levels to establishment a complete analogy between the term logic and the propositional logic,propose a universal and more stringent method,i. e. structure determination method. This method can help us reveal the inevitability between the premise and the conclusion of traditional inference,thus ascertain whether a joint calculation formula is tautology or not,and help get a tautology from any satisfiable formula ( including tautology) .