类型一阶逻辑的理论证明探讨

Theoretical Proof of Typed First-order Logic

类型一阶逻辑在传统的一阶逻辑上,引入了类型,它是多态多类逻辑程序设计语言的理论基础,对编译系统设计与实现的进一步发展具有重要意义。论文在类型一阶逻辑的理论层面进行了探讨,引入了基本简单导出的可靠性定理和等值符号的可替换性定理,并予以证明。通过这两个定理,可以简化类型一阶逻辑理论证明中的工作量,使得将来的理论研究更加方便。

Type is introduced into the typed first-order logic,which is based on the traditional first-order logic and the theoretical foundation of polymorphic and polytypic logic programming language. Typed first-order is significant to the further development of the design and implementation of compilation system. This paper is a research at the theoretical level and it introduces reliability theorem of the basic and simple derivation and the exchangeability theorem of the equivalent symbols,and the two theorems are proved in this paper. With the two theorems,the workload of the first-order logic proof can be simplified and the future theoretical research will be easier.