中介谓词演算系统ME与ME之间的化归算法及其应用

在经典二值逻辑中，带等词的谓词演算系统Ｆ１与Ｆ１＊的函词系统等价，在互推关系下这两个系统也等价，然而在中介逻辑中，带等词的中介谓词演算系统ＭＥ与ＭＥ＊函词系统不等价，本文定理１指出，在互推关系下，任何ＭＥ＊中的公式均可化为ＭＥ中的标准前束范式，因此在互推意义下两系统等价，在中介逻辑中，ＭＥ是一个较为特殊的子系统，它具有许多与二值逻辑相类似的性质，本文的结果为将这些性质进一步推广到ＭＥ＊上提供了基础

Algorithm and Its Applications of Transformation between Medium Predicate Calculus Systems ME and ME

In classical 2-valued logic,it is known that the connective system of predicate calculus with equality ,FI are equivalent to that of FI , these two systems are also equivalent under the relationship of inference. In medium logic (ML), however, it has been proved that the connective systems of medium predicate calculus ME and ME are not e-quivalent. Theorem 1 in this paper gives an algorithm which transforms a formula of ME into a prenex standard form in ME,and therefore shows that ME is equivalent to ME under the relationship of inference. As a special sub-system of ML, ME has many useful properties similar to those in 2-valued logic. The result shown above provides a foundation for the generalization of these properties onto ME. As two examples, we present the Skolem standard form theorem and the Herbrand theorem of ME. The results in the paper also show that the equivalence between two logic systems under the relationship of inference does not means that they have the same logical properties.