论直觉主义谓词逻辑的矢列式自然演绎系统与公理化系统

On Axiomatic System and Natural Deduction System in Sequent Calculus Style for Intuitionistic Predicate Logic

在达米特的直觉主义谓词逻辑的矢列式自然演绎系统和公理化系统的基础上,文章详细证明了系统中的演绎定理,指出系统与系统的对应关系并且完整证明了二者的等价关系,分析和比较了二者的证明策略,还探讨了矢列式自然演绎系统与公理化系统之间等价转化的方法论意义及局限性。这些工作有助于从理论和实践上客观地分析和评价这两种证明演算,为同一逻辑的矢列式自然演绎系统与公理化系统之间的等价转化提供方法论上的借鉴意义。

On the bases of Dummett＇ s natural deduction system in sequent calculus style and axiomatic system for intuitionistic predicate logic, the paper proves the deduction theorem detailedly in the system , points out the corresponding relationship between the system and the system and proves the equivalent relationship between the two systems, analyzes and compares the two methods of proof strategies, and also discusses the methodological significance and limitations of the equivalence transformation between natural deduction system in sequent calculus style and axiomatic system. These jobs are helpful to analyze and evaluate the two kinds of proof calculi objectively from theory and practice, provide the methodological lessons for the equivalent transformation of the same logic between natural deduction system in sequent calculus style and axiomatic system.