命题证明系统和快速一致性证明器
Propositional proof systems and fast consistency provers
摘要：
快速一致性证明器是一个一致的多时间公理化理论，它具有任何其他多时间公理化理论的有限一致性陈述的简短证明。Kraj 'ıček和Pudlák证明了一个最优命题证明系统的存在等价于一个快速一致性证明器的存在。很容易观察到，${\sf NP}={\sf coNP}$意味着存在一个快速一致性证明器。相反的含义是一个悬而未决的问题。在本文中，我们定义了一个不太可能的快速一致性证明的概念，并证明了它的存在性等价于${\sf NP}={\sf coNP}$。接下来，它被证明，快速一致性证明不存在，如果一个考虑RE公理化理论，而不是理论与公理集是可识别的多项式时间。
英文摘要：
A fast consistency prover is a consistent poly-time axiomatized theory that has short proofs of the finite consistency statements of any other poly-time axiomatized theory. Kraj\'ıček and Pudlák proved that the existence of an optimal propositional proof system is equivalent to the existence of a fast consistency prover. It is an easy observation that ${\sf NP}={\sf coNP}$ implies the existence of a fast consistency prover. The reverse implication is an open question. In this paper we define the notion of an unlikely fast consistency prover and prove that its existence is equivalent to ${\sf NP}={\sf coNP}$. Next it is proved that fast consistency provers do not exist if one considers RE axiomatized theories rather than theories with an axiom set that is recognizable in polynomial time.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
