蕴涵命题演算的不可判定问题
Undecidable problems for propositional calculi with implication
摘要：
本文利用肯定前件和替换规则研究了包含经典蕴涵$\to$的签名上的命题演算。对于这些演算，我们考虑一些识别问题，如识别导子，扩展，完备性和公理化。本文的主要结果是证明了对于任何命题演算，扩张的识别问题都是不可判定的;对于包含公式$x \to ( y \to x )$的命题演算，公理化和完备性的识别问题都是不可判定的。作为推论，固定公式$A$的可导性问题对于所有$A$也是不可判定的。此外，我们给出了相关成果的历史回顾。
英文摘要：
In this article, we deal with propositional calculi over a signature containing the classical implication $\to$ with the rules of modus ponens and substitution. For these calculi we consider few recognizing problems such as recognizing derivations, extensions, completeness, and axiomatizations. The main result of this paper is to prove that the problem of recognizing extensions is undecidable for every propositional calculus, and the problems of recognizing axiomatizations and completeness are undecidable for propositional calculi containing the formula $x \to ( y \to x )$. As a corollary, the problem of derivability of a fixed formula $A$ is also undecidable for all $A$. Moreover, we give a historical survey of related results.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
