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

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

直觉主义谓词逻辑与经典谓词逻辑的矢列演算系统

在达米特给出的直觉主义谓词逻辑矢列演算系统的基础上,构造一个与等价的系统L^*,这有助于研究直觉主义命题逻辑的可判定性问题。与此同时,还构造经典谓词逻辑的矢列演算系统以及直觉主义谓词逻辑的矢列演算系统LK^*,这有助于探讨直觉主义逻辑与经典逻辑之间关系。

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

达米特系统地给出了直觉主义谓词逻辑的矢列式自然演绎系统N。在此基础上,我们给出一个与之等价的系统NSI,进一步探讨这两个系统的特点和证明策略,比较矢列式自然演绎系统与根岑的自然演绎系统的异同,并评价矢列式自然演绎系统的历史地位和意义。