We shall define in this chapter two translations of bounded arithmetic formulas into propositional formulas and, more importantly, we shall also define translations of proofs in various systems of bounded arithmetic into propositional proofs in particular proof systems.

In the first section we shall consider the case when the language of I△0 is augmented by new predicate or function symbols, and the case of the theories and. In the second section we treat formulas in the language L and the theories, and.

In the third section we study the provability of the reflection principles for propositional proof systems in bounded arithmetic and the relation of these reflection principles to the polynomial simulations. In the fourth section we present some model-theoretic proofs for statements obtained earlier. The final section then suggests another relation of arithmetic proofs to Boolean logic, namely the relation between witnessing arguments and test (decision) trees.

Bounded formulas with a predicate

First we shall treat the theory I△0(R) and then generalize the treatment to the theories and. Instead of I△0(R) we could consider the theory but the presentation for the former is simpler. The language LPA(R) of I△0(R) is the language LPA augmented by a new binary predicate symbol R(x, y).