蕴涵命题演算公理化识别问题的不可判定性
Undecidability of the problem of recognizing axiomatizations for implicative propositional calculi
摘要：
在本文中，我们考虑命题演算，这是可公理化的直觉蕴涵命题演算的扩展连同肯定前件和替换规则。我们证明了下列问题的不可判定性：给定的有限命题公式集是否构成一个固定的命题演算的适当公理系统。此外，我们证明了同样的以下限制这个问题：是否一个给定的有限集定理的一个固定的命题演算推导出所有定理的演算。这些结果的证明是基于减少的不可判定的停机问题的标签系统介绍后。
英文摘要：
In this paper we consider propositional calculi, which are finitely axiomatizable extensions of intuitionistic implicational propositional calculus together with the rules of modus ponens and substitution. We give a proof of undecidability of the following problem for these calculi: whether a given finite set of propositional formulas constitutes an adequate axiom system for a fixed propositional calculus. Moreover, we prove the same for the following restriction of this problem: whether a given finite set of theorems of a fixed propositional calculus derives all theorems of this calculus. The proof of these results is based on a reduction of the undecidable halting problem for the tag systems introduced by Post.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
