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 V12 and hence,
in particular, polynomially simulates the quantified propositional
calculus G
and the Πb1-consequences of S12 proved with
one use of exponentiation.
Furthermore, the soundness of iEF is not provable in
S12.
An iteration of the construction yields
a proof system corresponding to T2 + Exp and, in principle,
to much stronger theories.