__
TR03-055 | 20th July 2003 00:00
__

#### Implicit proofs

**Abstract:**

We describe a general method how to construct from

a propositional proof system P a possibly much stronger

proof system iP. The system iP operates with

exponentially long P-proofs described ``implicitly''

by polynomial size circuits.

As an example we prove that proof system iEF, implicit EF,

corresponds to bounded arithmetic theory V^1_2 and hence,

in particular, polynomially simulates the quantified propositional

calculus G and the \Pi^b_1-consequences of S^1_2 proved with

one use of exponentiation.

Furthermore, the soundness of iEF is not provable in S^1_2.

An iteration of the construction yields

a proof system corresponding to T_2 + Exp and, in principle,

to much stronger theories.