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.

We identify two new clusters of proof complexity measures equal up to polynomial and log ⁡ n factors. The first cluster contains the logarithm of tree-like resolution size, regularized clause and monomial space, and clause space, ordinary and regularized, in regular and tree-like resolution. Consequently, separating clause or monomial space from the logarithm of tree-like resolution size is equivalent to showing strong trade-offs between clause space and length, and equivalent to showing super-critical trade-offs between clause space and depth. The second cluster contains width, Σ 2 space (a generalization of clause space to depth 2 Frege systems), ordinary and regularized, and the logarithm of tree-like R ( log ⁡ ) size. As an application, we improve a known size-space trade-off for polynomial calculus with resolution. We further show a quadratic lower bound on tree-like resolution size for formulas refutable in clause space 4, and introduce a measure intermediate between depth and the logarithm of tree-like resolution size.