Reflection principles, propositional proof systems, and theories

TL;DR

This paper explores reflection principles in propositional proof systems, analyzing their complexity and connections to arithmetical theories, with a focus on lower bounds and proof system conjectures.

Contribution

It revisits reflection principles for propositional proofs using a finer scale and connects proof complexity conjectures with associated proof systems and theories.

Findings

Proving lower bounds on Resolution proofs is hard within Resolution.

Survey of arithmetical theories and their associated proof systems.

Connection established between proof complexity conjectures and theories.

Abstract

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\"uller 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.