论文标题
反思原则，命题证明系统和理论
Reflection principles, propositional proof systems, and theories
论文作者
论文摘要
反思原则是陈述，如果句子可以证明，那是真的。已经研究了一阶理论的反思原则，但它们在命题证明复杂性中也起着重要作用。在本文中，我们将使用更精细的反思原则来重新审视有关命题证明系统的反思原则的一些结果。我们将使用这样的结果，即在解决方案上证明下限很难解决。这首先出现在最近的Atserias和Müller作为关键引理中，并在某些衍生文件中被广泛化和简化。我们还将调查有关与之相关的算术理论和证明系统的一些结果。我们将展示有关有限一致性声明的证据复杂性的猜想与与理论相关的证明系统的陈述之间的联系。
The reflection principle is the statement that if a sentence is provable then it is true. Reflection principles have been studied for first-order theories, but they also play an important role in propositional proof complexity. In this paper we will revisit some results about the reflection principles for propositional proofs systems using a finer scale of reflection principles. We will use the result that proving lower bounds on Resolution proofs is hard in Resolution. This appeared first in the recent article of Atserias and Müller as a key lemma and was generalized and simplified in some spin-off papers. We will also survey some results about arithmetical theories and proof systems associated with them. We will show a connection between a conjecture about proof complexity of finite consistency statements and a statement about proof systems associated with a theory.
