We investigate the connection between propositional proof systems and their canonical pairs. It is known that simulations between proof systems translate to reductions between their canonical pairs. We focus on the opposite direction and study the following questions. Q1: Where does the implication [can(f) ≤pp m can(g) ⇒ f ≤s g] hold, and where does it fail? Q2: Where can we find proof systems of different strengths, but equivalent canonical pairs? Q3: What do (non-)equivalent canonical pairs tell about the corresponding proof systems? Q4: Is every NP-pair (A, B), where A is NP-complete, strongly many-one equivalent to the canonical pair of some proof system? In short, we show that Q1 and Q2 can be answered with ‘everywhere’, which generalizes previous results by Pudl´ak and Beyersdorff. Regarding Q3, inequivalent canonical pairs tell that the proof systems are not “very similar”, while equivalent, P-inseparable canonical pairs tell that they are not “very differe...
Christian Glaßer, Alan L. Selman, Liyu Zhang