Paper detail

Reflection principles, propositional proof systems, and theories

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.