PROOF SYSTEMS AND THE REFLECTION PRINCIPLE
Stephen A Cook, Phuong Nguyen · Cambridge University Press eBooks · 2010
An association between V i and the proof system (for i ≥ 1) is shown in Chapter VII by the fact that each bounded theorem of the theory V i translates into a family of tautologies that have polynomial-size proofs. Our theories and their associated proof systems are more deeply connected than as shown by just the propositional translation theorems. In this chapter we will present some more connections between the proof systems, their associated theories and the underlying complexity classes. In general, for each proof system F we study the principle that asserts that the system is sound, i.e, that formulas that have F -proofs are valid. This is known as the Reflection Principle (RFN) for F . We will show in this chapter that the theories V i and TV i prove the RNF for their associated proof systems when the principles are stated for formulas. Together with the Propositional Translation Theorems, these show that the systems and are the strongest systems (for proving formulas) whose RFN are provable in the theories V i and TV i , respectively. A connection between a propositional proof system F and the complexity class C definable in the theory T associated with F will be seen by the fact that the Witnessing Problem for F is complete for C . Recall Theorem VII.4.13 which shows that the Witnessing Problem for (and equivalently for eFrege ) are solvable by a polytime algorithm.