论文标题
命题证明系统和快速的一致性抛弃者
Propositional proof systems and fast consistency provers
论文作者
论文摘要
快速一致性供者是一种一致的多时间公理化理论，它具有任何其他多个多时间公理理论的有限一致性说明的简短证明。 Kraj \'ıček和Pudlák证明，最佳命题证明系统的存在等同于存在快速一致性供体的存在。简单的观察是，$ {\ sf np} = {\ sf conp} $意味着存在快速一致性供您的存在。相反的含义是一个悬而未决的问题。 在本文中，我们定义了不太可能的快速一致性示意剂的概念，并证明其存在等效于$ {\ sf np} = {\ sf conp} $。 接下来证明，如果人们认为重新安置理论而不是具有在多项式时间中可以识别的公理集的理论，则不存在快速一致性差异。
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.
